---

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


1. t : ℕ@i
2. A : Id List@i
3. {a:Id| (a ∈ A)}  ~ ℕ(2 * t) + 1@i
4. W : {a:Id| (a ∈ A)}  List List@i
5. ∀ws:{a:Id| (a ∈ A)}  List. ((ws ∈ W) ⇐⇒ (||ws|| = (t + 1) ∈ ℤ) ∧ no_repeats({a:Id| (a ∈ A)} ;ws))@i
6. n-intersecting({a:Id| (a ∈ A)} ;Combination(((2 - 1) * t) + 1;{a:Id| (a ∈ A)} );2)
⊢ two-intersection(A;W)
BY
{ (Subst' t + 1 ~ ((2 - 1) * t) + 1 -2 THEN Auto) }

1
1. t : ℕ@i
2. A : Id List@i
3. {a:Id| (a ∈ A)}  ~ ℕ(2 * t) + 1@i
4. W : {a:Id| (a ∈ A)}  List List@i
5. ∀ws:{a:Id| (a ∈ A)}  List. ((ws ∈ W) ⇐⇒ (||ws|| = (((2 - 1) * t) + 1) ∈ ℤ) ∧ no_repeats({a:Id| (a ∈ A)} ;ws))@i
6. n-intersecting({a:Id| (a ∈ A)} ;Combination(((2 - 1) * t) + 1;{a:Id| (a ∈ A)} );2)
⊢ two-intersection(A;W)

---

Latex:



1.  t  :  \mBbbN{}@i
2.  A  :  Id  List@i
3.  \{a:Id|  (a  \mmember{}  A)\}    \msim{}  \mBbbN{}(2  *  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||  =  (t  +  1))  \mwedge{}  no\_repeats(\{a:Id|  (a  \mmember{}  A)\}  ;ws))@i
6.  n-intersecting(\{a:Id|  (a  \mmember{}  A)\}  ;Combination(((2  -  1)  *  t)  +  1;\{a:Id|  (a  \mmember{}  A)\}  );2)
\mvdash{}  two-intersection(A;W)


By

(Subst'  t  +  1  \msim{}  ((2  -  1)  *  t)  +  1  -2  THEN  Auto)

---

Home Index