---

Step * 2 1 1 of Lemma coW-equiv-iff


1. [A] : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. ∀z:coW(A;a.B[a]). (coWmem(a.B[a];z;w) ⇐⇒ coWmem(a.B[a];z;w'))
6. p1 : copath(a.B[a];w)
7. p2 : copath(a.B[a];w')
8. ((copath-length(p1) = 1 ∈ ℤ) ∧ (p2 = () ∈ copath(a.B[a];w')))
∨ ((copath-length(p2) = 1 ∈ ℤ) ∧ (p1 = () ∈ copath(a.B[a];w)))
⊢ ∃q:{q:Pos(coW-game(a.B[a];w;w'))| Legal2(<p1, p2>;q)} . win2(coW-game(a.B[a];w;w')@q)
BY
{ (D -3 THEN D -2 THEN RepUR ``copath-length copath-nil copath`` -1) }

1
1. [A] : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. ∀z:coW(A;a.B[a]). (coWmem(a.B[a];z;w) ⇐⇒ coWmem(a.B[a];z;w'))
6. n : ℕ
7. p3 : coPath(a.B[a];w;n)
8. n1 : ℕ
9. p4 : coPath(a.B[a];w';n1)
10. ((n = 1 ∈ ℤ) ∧ (<n1, p4> = <0, ⋅> ∈ (n:ℕ × coPath(a.B[a];w';n))))
∨ ((n1 = 1 ∈ ℤ) ∧ (<n, p3> = <0, ⋅> ∈ (n:ℕ × coPath(a.B[a];w;n))))
⊢ ∃q:{q:Pos(coW-game(a.B[a];w;w'))| Legal2(<<n, p3>, n1, p4>;q)} . win2(coW-game(a.B[a];w;w')@q)

---

Latex:

---

Latex:

1.  [A]  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type
3.  w  :  coW(A;a.B[a])
4.  w'  :  coW(A;a.B[a])
5.  \mforall{}z:coW(A;a.B[a]).  (coWmem(a.B[a];z;w)  \mLeftarrow{}{}\mRightarrow{}  coWmem(a.B[a];z;w'))
6.  p1  :  copath(a.B[a];w)
7.  p2  :  copath(a.B[a];w')
8.  ((copath-length(p1)  =  1)  \mwedge{}  (p2  =  ()))  \mvee{}  ((copath-length(p2)  =  1)  \mwedge{}  (p1  =  ()))
\mvdash{}  \mexists{}q:\{q:Pos(coW-game(a.B[a];w;w'))|  Legal2(<p1,  p2>q)\}  .  win2(coW-game(a.B[a];w;w')@q)


By

---

Latex:
(D  -3  THEN  D  -2  THEN  RepUR  ``copath-length  copath-nil  copath``  -1)

---

Home Index