### Nuprl Lemma : no_repeats_append_iff

`∀[T:Type]. ∀[l1,l2:T List].  uiff(no_repeats(T;l1 @ l2);l_disjoint(T;l1;l2) ∧ no_repeats(T;l1) ∧ no_repeats(T;l2))`

Proof

Definitions occuring in Statement :  l_disjoint: `l_disjoint(T;l1;l2)` no_repeats: `no_repeats(T;l)` append: `as @ bs` list: `T List` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` and: `P ∧ Q` universe: `Type`
Definitions unfolded in proof :  prop: `ℙ` false: `False` implies: `P `` Q` not: `¬A` all: `∀x:A. B[x]` l_disjoint: `l_disjoint(T;l1;l2)` uimplies: `b supposing a` and: `P ∧ Q` uiff: `uiff(P;Q)` member: `t ∈ T` uall: `∀[x:A]. B[x]` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` ge: `i ≥ j ` top: `Top` nat: `ℕ` or: `P ∨ Q` decidable: `Dec(P)` no_repeats: `no_repeats(T;l)` true: `True` lelt: `i ≤ j < k` int_seg: `{i..j-}` guard: `{T}` squash: `↓T` subtype_rel: `A ⊆r B` iff: `P `⇐⇒` Q` less_than: `a < b` cand: `A c∧ B` l_member: `(x ∈ l)` le: `A ≤ B` sq_type: `SQType(T)`
Lemmas referenced :  istype-universe list_wf l_disjoint_wf append_wf no_repeats_wf no_repeats_witness no_repeats_append sublist_append1 no_repeats-sublist sublist_append2 istype-nat istype-less_than int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma istype-int itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf full-omega-unsat decidable__le nat_properties istype-void length-append select_wf length_wf decidable__lt istype-le equal_wf squash_wf true_wf select_append_front subtype_rel_self iff_weakening_equal subtract_wf itermSubtract_wf intformless_wf int_term_value_subtract_lemma int_formula_prop_less_lemma add-is-int-iff itermAdd_wf int_term_value_add_lemma false_wf select_append_back select_member top_wf subtype_rel_list length_append non_neg_length decidable__equal_int int_subtype_base subtype_base_sq int_formula_prop_eq_lemma intformeq_wf
Rules used in proof :  universeEquality instantiate productIsType universeIsType because_Cache independent_functionElimination inhabitedIsType functionIsTypeImplies voidElimination dependent_functionElimination lambdaEquality_alt independent_pairEquality productElimination sqequalRule independent_isectElimination independent_pairFormation hypothesisEquality thin isectElimination sqequalHypSubstitution hypothesis isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution extract_by_obid introduction cut cumulativity isectIsTypeImplies functionIsType int_eqEquality dependent_pairFormation_alt approximateComputation natural_numberEquality isect_memberEquality_alt rename setElimination equalityIstype unionElimination lambdaFormation_alt dependent_set_memberEquality_alt applyEquality imageElimination equalityTransitivity equalitySymmetry imageMemberEquality baseClosed pointwiseFunctionality promote_hyp baseApply closedConclusion addEquality sqequalBase intEquality applyLambdaEquality

Latex:
\mforall{}[T:Type].  \mforall{}[l1,l2:T  List].
uiff(no\_repeats(T;l1  @  l2);l\_disjoint(T;l1;l2)  \mwedge{}  no\_repeats(T;l1)  \mwedge{}  no\_repeats(T;l2))

Date html generated: 2019_10_15-AM-10_22_15
Last ObjectModification: 2019_08_05-PM-01_59_05

Theory : list_1

Home Index