Nuprl Lemma : tuple-type-subtype-n-tuple

[L:Type List]. ∀[n:ℕ].  tuple-type(L) ⊆n-tuple(n) supposing ||L|| n ∈ ℤ


Proof




Definitions occuring in Statement :  n-tuple: n-tuple(n) tuple-type: tuple-type(L) length: ||as|| list: List nat: uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a sq_type: SQType(T) all: x:A. B[x] implies:  Q guard: {T} n-tuple: n-tuple(n) subtype_rel: A ⊆B prop: nat: and: P ∧ Q cand: c∧ B top: Top squash: T true: True iff: ⇐⇒ Q int_seg: {i..j-} lelt: i ≤ j < k le: A ≤ B less_than: a < b ge: i ≥  decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A
Lemmas referenced :  subtype_base_sq int_subtype_base equal_wf length_wf nat_wf list_wf subtype_rel_tuple-type map_wf int_seg_wf top_wf upto_wf map-length length_upto length_wf_nat squash_wf true_wf iff_weakening_equal select-map subtype_rel_list lelt_wf select_wf int_seg_properties nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt intformless_wf int_formula_prop_less_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin instantiate extract_by_obid sqequalHypSubstitution isectElimination cumulativity intEquality independent_isectElimination hypothesis dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination sqequalRule axiomEquality universeEquality hypothesisEquality setElimination rename isect_memberEquality because_Cache natural_numberEquality lambdaEquality voidElimination voidEquality applyEquality imageElimination imageMemberEquality baseClosed productElimination independent_pairFormation lambdaFormation dependent_set_memberEquality unionElimination dependent_pairFormation int_eqEquality computeAll

Latex:
\mforall{}[L:Type  List].  \mforall{}[n:\mBbbN{}].    tuple-type(L)  \msubseteq{}r  n-tuple(n)  supposing  ||L||  =  n



Date html generated: 2017_04_17-AM-09_29_10
Last ObjectModification: 2017_02_27-PM-05_29_21

Theory : tuples


Home Index