### Nuprl Lemma : no_repeats_concat

`∀[T:Type]. ∀[ll:T List List].`
`  uiff(no_repeats(T;concat(ll));∀i:ℕ||ll||`
`                                  (no_repeats(T;ll[i])`
`                                  ∧ (∀j:{j:ℕ||ll||| ¬(i = j ∈ ℤ)} . ∀k:ℕ||ll[i]||.  (¬(ll[i][k] ∈ ll[j])))))`

Proof

Definitions occuring in Statement :  no_repeats: `no_repeats(T;l)` l_member: `(x ∈ l)` select: `L[n]` length: `||as||` concat: `concat(ll)` list: `T List` int_seg: `{i..j-}` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` not: `¬A` and: `P ∧ Q` set: `{x:A| B[x]} ` natural_number: `\$n` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` false: `False` prop: `ℙ` uall: `∀[x:A]. B[x]` int_seg: `{i..j-}` guard: `{T}` sq_stable: `SqStable(P)` squash: `↓T` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` less_than: `a < b` so_lambda: `λ2x.t[x]` so_apply: `x[s]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` l_all: `(∀x∈L.P[x])` pairwise: `(∀x,y∈L.  P[x; y])` l_disjoint: `l_disjoint(T;l1;l2)` iff: `P `⇐⇒` Q` subtype_rel: `A ⊆r B` rev_implies: `P `` Q` le: `A ≤ B` cand: `A c∧ B` l_member: `(x ∈ l)` nat: `ℕ` ge: `i ≥ j ` true: `True`
Lemmas referenced :  l_member_wf select_wf list_wf int_seg_properties length_wf sq_stable__not equal_wf decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt intformless_wf int_formula_prop_less_lemma int_seg_wf set_wf not_wf no_repeats_witness l_all_wf no_repeats_wf pairwise_wf2 l_disjoint_wf all_wf iff_weakening_uiff concat_wf no_repeats-concat-iff uiff_wf lelt_wf select_member intformeq_wf int_formula_prop_eq_lemma subtype_rel_sets equal-wf-T-base set_subtype_base int_subtype_base less_than_transitivity2 le_weakening2 nat_properties squash_wf true_wf
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation isect_memberFormation introduction lambdaFormation sqequalHypSubstitution productElimination thin hypothesis independent_functionElimination voidElimination extract_by_obid isectElimination cumulativity hypothesisEquality because_Cache setElimination rename independent_isectElimination natural_numberEquality intEquality sqequalRule imageMemberEquality baseClosed imageElimination dependent_functionElimination unionElimination dependent_pairFormation lambdaEquality int_eqEquality isect_memberEquality voidEquality computeAll independent_pairEquality setEquality productEquality instantiate addLevel applyEquality universeEquality equalityTransitivity equalitySymmetry dependent_set_memberEquality hyp_replacement

Latex:
\mforall{}[T:Type].  \mforall{}[ll:T  List  List].
uiff(no\_repeats(T;concat(ll));\mforall{}i:\mBbbN{}||ll||
(no\_repeats(T;ll[i])
\mwedge{}  (\mforall{}j:\{j:\mBbbN{}||ll|||  \mneg{}(i  =  j)\}  .  \mforall{}k:\mBbbN{}||ll[i]||.
(\mneg{}(ll[i][k]  \mmember{}  ll[j])))))

Date html generated: 2016_10_21-AM-10_30_22
Last ObjectModification: 2016_07_12-AM-05_44_35

Theory : list_1

Home Index