Nuprl Lemma : list-decomp-no

Nuprl Lemma : list-decomp-no_repeats

∀[T:Type]. ∀[l1,l2,l3,l4:T List]. ∀[x:T].
  ((l1 = l3 ∈ (T List)) ∧ (l2 = l4 ∈ (T List))) supposing
     ((((l1 @ [x]) @ l2) = ((l3 @ [x]) @ l4) ∈ (T List)) and
     no_repeats(T;(l1 @ [x]) @ l2))

Proof

Definitions occuring in Statement : no_repeats: no_repeats(T;l), append: as @ bs, cons: [a / b], nil: [], list: T List, uimplies: b supposing a, uall: ∀[x:A]. B[x], and: P ∧ Q, universe: Type, equal: s = t ∈ T
Definitions unfolded in proof : uall: ∀[x:A]. B[x], member: t ∈ T, uimplies: b supposing a, and: P ∧ Q, cand: A c∧ B, prop: ℙ, iff: P ⇐⇒ Q, implies: P ⇒ Q, rev_implies: P ⇐ Q, all: ∀x:A. B[x], subtype_rel: A ⊆r B, le: A ≤ B, less_than': less_than'(a;b), false: False, not: ¬A, squash: ↓T, top: Top, true: True, guard: {T}, int_seg: {i..j^-}, lelt: i ≤ j < k, decidable: Dec(P), or: P ∨ Q, uiff: uiff(P;Q), satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], ge: i ≥ j , sq_type: SQType(T), select: L[n], cons: [a / b], less_than: a < b, no_repeats: no_repeats(T;l), nat: ℕ, subtract: n - m
Lemmas referenced : equal_wf, list_wf, append_wf, cons_wf, nil_wf, no_repeats_wf, list_extensionality_iff, int_seg_subtype, length_wf, false_wf, le_wf, squash_wf, true_wf, add_functionality_wrt_eq, length_append, subtype_rel_list, top_wf, iff_weakening_equal, length-singleton, length-append, length_of_cons_lemma, length_of_nil_lemma, int_seg_properties, decidable__le, add-is-int-iff, satisfiable-full-omega-tt, intformnot_wf, intformle_wf, itermAdd_wf, itermVar_wf, itermConstant_wf, int_formula_prop_not_lemma, int_formula_prop_le_lemma, int_term_value_add_lemma, int_term_value_var_lemma, int_term_value_constant_lemma, int_formula_prop_wf, int_seg_wf, decidable__equal_int, non_neg_length, intformand_wf, int_formula_prop_and_lemma, decidable__lt, intformless_wf, int_formula_prop_less_lemma, lelt_wf, select_append_front, select_append_back, subtype_base_sq, int_subtype_base, intformeq_wf, itermSubtract_wf, int_formula_prop_eq_lemma, int_term_value_subtract_lemma, decidable__or, less_than_wf, intformor_wf, int_formula_prop_or_lemma, length_wf_nat, nat_properties, nat_wf, le_weakening2, select_wf, not_wf, add-member-int_seg1, subtract_wf, and_wf, add-associates, minus-add, minus-one-mul, add-swap, add-mul-special, add-commutes, zero-add, zero-mul, add-zero
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, isect_memberFormation, introduction, cut, independent_pairFormation, hypothesis, sqequalRule, sqequalHypSubstitution, productElimination, thin, independent_pairEquality, axiomEquality, extract_by_obid, isectElimination, cumulativity, hypothesisEquality, isect_memberEquality, because_Cache, equalityTransitivity, equalitySymmetry, universeEquality, independent_functionElimination, lambdaFormation, dependent_functionElimination, applyEquality, natural_numberEquality, addEquality, independent_isectElimination, lambdaEquality, imageElimination, intEquality, voidElimination, voidEquality, imageMemberEquality, baseClosed, applyLambdaEquality, setElimination, rename, unionElimination, pointwiseFunctionality, promote_hyp, baseApply, closedConclusion, dependent_pairFormation, int_eqEquality, computeAll, dependent_set_memberEquality, instantiate, hyp_replacement, multiplyEquality, productEquality

Latex:
\mforall{}[T:Type]. \mforall{}[l1,l2,l3,l4:T List]. \mforall{}[x:T]. ((l1 = l3) \mwedge{} (l2 = l4)) supposing ((((l1 @ [x]) @ l2) = ((l3 @ [x]) @ l4)) and no\_repeats(T;(l1 @ [x]) @ l2)) Date html generated: 2017_10_01-AM-08_39_11 Last ObjectModification: 2017_07_26-PM-04_27_23 Theory : list! Home Index