### Nuprl Lemma : append-tuple-one-one

[L1,L2:Type List].
∀[x1,x2:tuple-type(L1)]. ∀[y1,y2:tuple-type(L2)].
{(x1 x2 ∈ tuple-type(L1)) ∧ (y1 y2 ∈ tuple-type(L2))}
supposing append-tuple(||L1||;||L2||;x1;y1) append-tuple(||L1||;||L2||;x2;y2) ∈ tuple-type(L1 L2)
supposing 0 < ||L2||

Proof

Definitions occuring in Statement :  append-tuple: append-tuple(n;m;x;y) tuple-type: tuple-type(L) length: ||as|| append: as bs list: List less_than: a < b uimplies: supposing a uall: [x:A]. B[x] guard: {T} and: P ∧ Q natural_number: \$n universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q ge: i ≥  all: x:A. B[x] decidable: Dec(P) or: P ∨ Q false: False le: A ≤ B not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top prop: less_than: a < b squash: T guard: {T} so_lambda: λ2x.t[x] so_apply: x[s] pi1: fst(t) pi2: snd(t) subtype_rel: A ⊆B int_iseg: {i...j} cand: c∧ B
Lemmas referenced :  split-tuple_wf append_wf non_neg_length decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf length-append decidable__lt length_wf intformless_wf itermAdd_wf int_formula_prop_less_lemma int_term_value_add_lemma istype-le istype-less_than tuple-type_wf append-tuple_wf list_wf split-tuple-append-tuple pi1_wf firstn_wf nth_tl_wf pi2_wf subtype_rel_tuple-type nth_tl_append subtype_rel-equal select_wf int_seg_properties length_append subtype_rel_list top_wf istype-universe length_nth_tl intformeq_wf itermSubtract_wf int_formula_prop_eq_lemma int_term_value_subtract_lemma int_seg_wf equal_functionality_wrt_subtype_rel2 firstn_append firstn_length
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut applyLambdaEquality extract_by_obid sqequalHypSubstitution isectElimination thin instantiate closedConclusion universeEquality hypothesisEquality hypothesis Error :dependent_set_memberEquality_alt,  because_Cache independent_pairFormation dependent_functionElimination unionElimination productElimination natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  int_eqEquality Error :isect_memberEquality_alt,  voidElimination sqequalRule Error :universeIsType,  addEquality imageElimination Error :productIsType,  independent_pairEquality axiomEquality Error :equalityIstype,  Error :isectIsTypeImplies,  Error :inhabitedIsType,  Error :lambdaFormation_alt,  setElimination rename applyEquality cumulativity equalityTransitivity equalitySymmetry

Latex:
\mforall{}[L1,L2:Type  List].
\mforall{}[x1,x2:tuple-type(L1)].  \mforall{}[y1,y2:tuple-type(L2)].
\{(x1  =  x2)  \mwedge{}  (y1  =  y2)\}
supposing  append-tuple(||L1||;||L2||;x1;y1)  =  append-tuple(||L1||;||L2||;x2;y2)
supposing  0  <  ||L2||

Date html generated: 2019_06_20-PM-02_03_42
Last ObjectModification: 2018_12_07-PM-06_36_19

Theory : tuples

Home Index