---

Step * 1 of Lemma two-intersecting-wait-set-exists


1. t : ℕ@i
2. A : Id List@i
3. ||A|| = ((2 * t) + 1) ∈ ℤ
4. no_repeats(Id;A)
5. {a:Id| (a ∈ A)}  ~ ℕ(2 * t) + 1
6. C : {a:Id| (a ∈ A)}  List List
7. ∀L:{a:Id| (a ∈ A)}  List. ((L ∈ C) ⇐⇒ (||L|| = (t + 1) ∈ ℤ) ∧ no_repeats({a:Id| (a ∈ A)} ;L))
⊢ two-intersection(A;C)
BY
{ (UsingVars [`t'] (BLemma `two-intersecting-wait-set`) THEN Auto) }

---

Latex:



1.  t  :  \mBbbN{}@i
2.  A  :  Id  List@i
3.  ||A||  =  ((2  *  t)  +  1)
4.  no\_repeats(Id;A)
5.  \{a:Id|  (a  \mmember{}  A)\}    \msim{}  \mBbbN{}(2  *  t)  +  1
6.  C  :  \{a:Id|  (a  \mmember{}  A)\}    List  List
7.  \mforall{}L:\{a:Id|  (a  \mmember{}  A)\}    List.  ((L  \mmember{}  C)  \mLeftarrow{}{}\mRightarrow{}  (||L||  =  (t  +  1))  \mwedge{}  no\_repeats(\{a:Id|  (a  \mmember{}  A)\}  ;L))
\mvdash{}  two-intersection(A;C)


By

(UsingVars  [`t']  (BLemma  `two-intersecting-wait-set`)  THEN  Auto)

---

Home Index