### Nuprl Lemma : no_repeats-concat-iff

`∀[T:Type]. ∀[ll:T List List].`
`  uiff(no_repeats(T;concat(ll));(∀l∈ll.no_repeats(T;l)) ∧ (∀l1,l2∈ll.  l_disjoint(T;l1;l2)))`

Proof

Definitions occuring in Statement :  pairwise: `(∀x,y∈L.  P[x; y])` l_disjoint: `l_disjoint(T;l1;l2)` l_all: `(∀x∈L.P[x])` no_repeats: `no_repeats(T;l)` concat: `concat(ll)` list: `T List` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` and: `P ∧ Q` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` uiff: `uiff(P;Q)` and: `P ∧ Q` prop: `ℙ` uimplies: `b supposing a` all: `∀x:A. B[x]` so_apply: `x[s]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` implies: `P `` Q` concat: `concat(ll)` top: `Top` true: `True` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` l_all: `(∀x∈L.P[x])` int_seg: `{i..j-}` guard: `{T}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` pairwise: `(∀x,y∈L.  P[x; y])` l_disjoint: `l_disjoint(T;l1;l2)` subtype_rel: `A ⊆r B` less_than: `a < b` squash: `↓T` cand: `A c∧ B`
Lemmas referenced :  false_wf int_term_value_add_lemma itermAdd_wf add-is-int-iff length_of_cons_lemma pairwise-cons cons_wf l_all-cons concat-cons no_repeats_append_iff append_wf iff_weakening_uiff l_disjoint-concat uiff_wf l_all_wf_nil length_wf int_seg_wf int_formula_prop_less_lemma intformless_wf decidable__lt 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 itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le int_seg_properties length_of_nil_lemma select_wf pairwise-nil l_all-nil true_wf and_wf no_repeats_witness no_repeats_nil nil_wf reduce_nil_lemma l_disjoint_wf pairwise_wf2 l_member_wf l_all_wf concat_wf no_repeats_wf list_wf list_induction
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin lemma_by_obid sqequalHypSubstitution isectElimination hypothesisEquality hypothesis sqequalRule lambdaEquality productEquality isectEquality cumulativity because_Cache lambdaFormation setElimination rename setEquality independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality independent_pairFormation natural_numberEquality productElimination independent_pairEquality axiomEquality equalityTransitivity equalitySymmetry addLevel independent_isectElimination unionElimination dependent_pairFormation int_eqEquality intEquality computeAll applyEquality universeEquality instantiate imageElimination addEquality pointwiseFunctionality promote_hyp baseApply closedConclusion baseClosed

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

Date html generated: 2016_05_14-PM-02_55_06
Last ObjectModification: 2016_01_15-AM-07_33_09

Theory : list_1

Home Index