### Nuprl Lemma : subtype_rel_tuple-type

[As,Bs:Type List].  tuple-type(As) ⊆tuple-type(Bs) supposing (||As|| ||Bs|| ∈ ℤ) ∧ (∀i:ℕ||As||. (As[i] ⊆Bs[i]))

Proof

Definitions occuring in Statement :  tuple-type: tuple-type(L) select: L[n] length: ||as|| list: List int_seg: {i..j-} uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] all: x:A. B[x] and: P ∧ Q natural_number: \$n int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T so_lambda: λ2x.t[x] uimplies: supposing a and: P ∧ Q prop: int_seg: {i..j-} guard: {T} lelt: i ≤ j < k all: x:A. B[x] decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False implies:  Q not: ¬A top: Top so_apply: x[s] subtype_rel: A ⊆B bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  ge: i ≥  le: A ≤ B bfalse: ff sq_type: SQType(T) bnot: ¬bb assert: b less_than': less_than'(a;b) nat_plus: + less_than: a < b squash: T true: True select: L[n] cons: [a b] nil: [] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] cand: c∧ B subtract: m iff: ⇐⇒ Q
Lemmas referenced :  list_induction uall_wf list_wf equal_wf length_wf all_wf int_seg_wf subtype_rel_wf select_wf int_seg_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 intformeq_wf int_formula_prop_eq_lemma tuple-type_wf equal-wf-base-T nil_wf length_of_nil_lemma subtype_rel_self equal-wf-base tupletype_nil_lemma tupletype_cons_lemma subtype_rel-equal unit_wf2 ifthenelse_wf null_wf bool_wf eqtt_to_assert assert_of_null length_of_cons_lemma non_neg_length itermAdd_wf int_term_value_add_lemma eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot equal-wf-T-base cons_wf add-is-int-iff false_wf add_nat_plus length_wf_nat less_than_wf nat_plus_wf nat_plus_properties lelt_wf list-cases stuck-spread base_wf null_nil_lemma product_subtype_list subtype_rel_transitivity null_cons_lemma btrue_wf and_wf bfalse_wf btrue_neq_bfalse subtype_rel_product decidable__equal_int add-member-int_seg2 subtract_wf itermSubtract_wf int_term_value_subtract_lemma add-associates add-swap add-commutes zero-add add-subtract-cancel int_subtype_base squash_wf true_wf select_cons_tl iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin instantiate extract_by_obid sqequalHypSubstitution isectElimination universeEquality sqequalRule lambdaEquality hypothesis isectEquality productEquality intEquality because_Cache hypothesisEquality natural_numberEquality setElimination rename independent_isectElimination equalityTransitivity equalitySymmetry productElimination dependent_functionElimination unionElimination dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll applyEquality cumulativity independent_functionElimination axiomEquality lambdaFormation equalityElimination promote_hyp baseClosed pointwiseFunctionality baseApply closedConclusion dependent_set_memberEquality imageMemberEquality applyLambdaEquality addEquality hypothesis_subsumption hyp_replacement imageElimination

Latex:
\mforall{}[As,Bs:Type  List].
tuple-type(As)  \msubseteq{}r  tuple-type(Bs)  supposing  (||As||  =  ||Bs||)  \mwedge{}  (\mforall{}i:\mBbbN{}||As||.  (As[i]  \msubseteq{}r  Bs[i]))

Date html generated: 2017_04_17-AM-09_29_07
Last ObjectModification: 2017_02_27-PM-05_31_29

Theory : tuples

Home Index