---

Step * of Lemma two-intersecting-wait-set

∀t:ℕ. ∀A:Id List.
  ({a:Id| (a ∈ A)}  ~ ℕ(2 * t) + 1
  ⇒ (∀W:{a:Id| (a ∈ A)}  List List
        ((∀ws:{a:Id| (a ∈ A)}  List. ((ws ∈ W) ⇐⇒ (||ws|| = (t + 1) ∈ ℤ) ∧ no_repeats({a:Id| (a ∈ A)} ;ws)))
        ⇒ two-intersection(A;W))))
BY
{ (Auto THEN (InstLemma `combinations-n-intersecting` [⌈2⌉;⌈t⌉;⌈{a:Id| (a ∈ A)} ⌉]⋅ THENA 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|| = (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:


\mforall{}t:\mBbbN{}.  \mforall{}A:Id  List.
    (\{a:Id|  (a  \mmember{}  A)\}    \msim{}  \mBbbN{}(2  *  t)  +  1
    {}\mRightarrow{}  (\mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List
                ((\mforall{}ws:\{a:Id|  (a  \mmember{}  A)\}    List.  ((ws  \mmember{}  W)  \mLeftarrow{}{}\mRightarrow{}  (||ws||  =  (t  +  1))  \mwedge{}  no\_repeats(\{a:Id|  (a  \mmember{}  A)\}  ;\000Cws)))
                {}\mRightarrow{}  two-intersection(A;W))))


By

(Auto  THEN  (InstLemma  `combinations-n-intersecting`  [\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}\{a:Id|  (a  \mmember{}  A)\}  \mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index