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)))


Definitions occuring in Statement :  length: ||as|| append: as bs list: List uimplies: supposing a uall: [x:A]. B[x] guard: {T} or: P ∨ Q and: P ∧ Q 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 prop: or: P ∨ Q guard: {T} and: P ∧ Q so_apply: x[s] implies:  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: c∧ B cons: [a b] false: False ge: i ≥  le: A ≤ B satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] not: ¬A subtype_rel: A ⊆B true: True squash: T iff: ⇐⇒ 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

\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