---

Step * 1 of Lemma three-intersecting-wait-set


1. t : ℕ@i
2. A : Id List@i
3. {a:Id| (a ∈ A)}  ~ ℕ(3 * t) + 1@i
4. W : {a:Id| (a ∈ A)}  List List@i
5. ∀ws:{a:Id| (a ∈ A)}  List. ((ws ∈ W) ⇐⇒ (||ws|| = ((2 * t) + 1) ∈ ℤ) ∧ no_repeats({a:Id| (a ∈ A)} ;ws))@i
6. n-intersecting({a:Id| (a ∈ A)} ;Combination(((3 - 1) * t) + 1;{a:Id| (a ∈ A)} );3)
⊢ three-intersection(A;W)
BY
{ (UnfoldTopAb 0 THEN (RWW "l_all_iff" 0 THEN Auto) THEN (With ⌈[ws1; ws2; ws3]⌉ (D 6)⋅ THENM D -1) THEN Auto) }

1
1. t : ℕ@i
2. A : Id List@i
3. {a:Id| (a ∈ A)}  ~ ℕ(3 * t) + 1@i
4. W : {a:Id| (a ∈ A)}  List List@i
5. ∀ws:{a:Id| (a ∈ A)}  List. ((ws ∈ W) ⇐⇒ (||ws|| = ((2 * t) + 1) ∈ ℤ) ∧ no_repeats({a:Id| (a ∈ A)} ;ws))@i
6. ws1 : {a:Id| (a ∈ A)}  List@i
7. (ws1 ∈ W)@i
8. ws2 : {a:Id| (a ∈ A)}  List@i
9. (ws2 ∈ W)@i
10. ws3 : {a:Id| (a ∈ A)}  List@i
11. (ws3 ∈ W)@i
12. ∃a:{a:Id| (a ∈ A)} . (∀L∈[ws1; ws2; ws3].(a ∈ L))
⊢ ∃a:{a:Id| (a ∈ A)} . ((a ∈ ws1) ∧ (a ∈ ws2) ∧ (a ∈ ws3))

---

Latex:



1.  t  :  \mBbbN{}@i
2.  A  :  Id  List@i
3.  \{a:Id|  (a  \mmember{}  A)\}    \msim{}  \mBbbN{}(3  *  t)  +  1@i
4.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
5.  \mforall{}ws:\{a:Id|  (a  \mmember{}  A)\}    List.  ((ws  \mmember{}  W)  \mLeftarrow{}{}\mRightarrow{}  (||ws||  =  ((2  *  t)  +  1))  \mwedge{}  no\_repeats(\{a:Id|  (a  \mmember{}  A)\}  ;w\000Cs))@i
6.  n-intersecting(\{a:Id|  (a  \mmember{}  A)\}  ;Combination(((3  -  1)  *  t)  +  1;\{a:Id|  (a  \mmember{}  A)\}  );3)
\mvdash{}  three-intersection(A;W)


By

(UnfoldTopAb  0
  THEN  (RWW  "l\_all\_iff"  0  THEN  Auto)
  THEN  (With  \mkleeneopen{}[ws1;  ws2;  ws3]\mkleeneclose{}  (D  6)\mcdot{}  THENM  D  -1)
  THEN  Auto)

---

Home Index