### Nuprl Lemma : general-append-cancellation

`∀[T:Type]. ∀[as,bs,cs,ds:T List].`
`  ({(as = bs ∈ (T List)) ∧ (cs = ds ∈ (T List))}) supposing `
`     (((||as|| = ||bs|| ∈ ℤ) ∨ (||cs|| = ||ds|| ∈ ℤ)) and `
`     ((as @ cs) = (bs @ ds) ∈ (T List)))`

Proof

Definitions occuring in Statement :  length: `||as||` append: `as @ bs` list: `T List` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` guard: `{T}` or: `P ∨ Q` and: `P ∧ Q` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` uimplies: `b supposing a` prop: `ℙ` or: `P ∨ Q` guard: `{T}` and: `P ∧ Q` so_apply: `x[s]` implies: `P `` Q` append: `as @ bs` all: `∀x:A. B[x]` so_lambda: `so_lambda(x,y,z.t[x; y; z])` top: `Top` so_apply: `x[s1;s2;s3]` cand: `A c∧ B` cons: `[a / b]` false: `False` ge: `i ≥ j ` le: `A ≤ B` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` not: `¬A` subtype_rel: `A ⊆r B` true: `True` squash: `↓T` iff: `P `⇐⇒` Q` decidable: `Dec(P)`
Lemmas referenced :  list_induction uall_wf list_wf isect_wf equal_wf append_wf or_wf length_wf list_ind_nil_lemma length_of_nil_lemma equal-wf-base-T list_ind_cons_lemma length_of_cons_lemma cons_wf list-cases nil_wf product_subtype_list non_neg_length satisfiable-full-omega-tt intformand_wf intformle_wf itermConstant_wf itermVar_wf intformeq_wf itermAdd_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_term_value_add_lemma int_formula_prop_wf subtype_rel_list top_wf squash_wf true_wf add_functionality_wrt_eq length_append iff_weakening_equal reduce_tl_cons_lemma and_wf tl_wf decidable__or decidable__equal_int intformnot_wf intformor_wf int_formula_prop_not_lemma int_formula_prop_or_lemma reduce_hd_cons_lemma hd_wf ge_wf length_cons_ge_one
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality cumulativity hypothesis because_Cache intEquality productEquality applyLambdaEquality independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality productElimination independent_pairEquality axiomEquality baseClosed equalityTransitivity equalitySymmetry lambdaFormation rename addEquality natural_numberEquality universeEquality unionElimination independent_pairFormation promote_hyp hypothesis_subsumption independent_isectElimination dependent_pairFormation int_eqEquality computeAll hyp_replacement applyEquality imageElimination imageMemberEquality dependent_set_memberEquality setElimination

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs,cs,ds:T  List].
(\{(as  =  bs)  \mwedge{}  (cs  =  ds)\})  supposing
(((||as||  =  ||bs||)  \mvee{}  (||cs||  =  ||ds||))  and
((as  @  cs)  =  (bs  @  ds)))

Date html generated: 2017_04_14-AM-09_26_36
Last ObjectModification: 2017_02_27-PM-04_00_50

Theory : list_1

Home Index