---

Step * of 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])))))
BY
{ ((UnivCD THENA Auto)
   THEN RWO "no_repeats-concat-iff" 0
   THEN Auto
   THEN Try ((UnfoldTopAb 0 THEN ParallelLast THEN Auto)⋅)) }

1
1. T : Type
2. ll : T List List
3. (∀l∈ll.no_repeats(T;l))
4. (∀l1,l2∈ll.  l_disjoint(T;l1;l2))
5. i : ℕ||ll||
6. j : {j:ℕ||ll||| ¬(i = j ∈ ℤ)} 
7. k : ℕ||ll[i]||
⊢ ¬(ll[i][k] ∈ ll[j])

2
1. T : Type
2. ll : T List List
3. ∀i:ℕ||ll||. (no_repeats(T;ll[i]) ∧ (∀j:{j:ℕ||ll||| ¬(i = j ∈ ℤ)} . ∀k:ℕ||ll[i]||.  (¬(ll[i][k] ∈ ll[j]))))
4. i : ℕ||ll||
5. no_repeats(T;ll[i])
6. ∀j:{j:ℕ||ll||| ¬(i = j ∈ ℤ)} . ∀k:ℕ||ll[i]||.  (¬(ll[i][k] ∈ ll[j]))
7. j : ℕi
⊢ l_disjoint(T;ll[j];ll[i])

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RWO  "no\_repeats-concat-iff"  0
  THEN  Auto
  THEN  Try  ((UnfoldTopAb  0  THEN  ParallelLast  THEN  Auto)\mcdot{}))

---

Home Index