---

Step * 1 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. 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))
BY
{ ((ParallelLast THENA Auto) THEN Reduce (-1) THEN RWW "l_all_cons" (-1) THEN Auto) }

---

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.  ws1  :  \{a:Id|  (a  \mmember{}  A)\}    List@i
7.  (ws1  \mmember{}  W)@i
8.  ws2  :  \{a:Id|  (a  \mmember{}  A)\}    List@i
9.  (ws2  \mmember{}  W)@i
10.  ws3  :  \{a:Id|  (a  \mmember{}  A)\}    List@i
11.  (ws3  \mmember{}  W)@i
12.  \mexists{}a:\{a:Id|  (a  \mmember{}  A)\}  .  (\mforall{}L\mmember{}[ws1;  ws2;  ws3].(a  \mmember{}  L))
\mvdash{}  \mexists{}a:\{a:Id|  (a  \mmember{}  A)\}  .  ((a  \mmember{}  ws1)  \mwedge{}  (a  \mmember{}  ws2)  \mwedge{}  (a  \mmember{}  ws3))


By

((ParallelLast  THENA  Auto)  THEN  Reduce  (-1)  THEN  RWW  "l\_all\_cons"  (-1)  THEN  Auto)

---

Home Index