---

Step * 1 1 1 1 1 2 2 of Lemma coW-trans_wf


1. A : 𝕌'
2. B : A ⟶ Type
3. w1 : coW(A;a.B[a])
4. w2 : coW(A;a.B[a])
5. w3 : coW(A;a.B[a])
6. n : ℤ
7. 0 < n
8. ∀[X:win2strat(coW-game(a.B[a];w1;w2);n - 1)]. ∀[Y:win2strat(coW-game(a.B[a];w2;w3);n - 1)].
     (coW-trans(X; Y) ∈ win2strat(coW-game(a.B[a];w1;w3);n - 1))
9. X : s:win2strat(coW-game(a.B[a];w1;w2);n - 1) ⋂ moves:{f:strat2play(coW-game(a.B[a];w1;w2);n - 1;s)| 
                                                          ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(coW-game(a.B[a];w1;w2))| Legal\000C2(moves[(2 * n) - 1];p)} 
10. X ∈ win2strat(coW-game(a.B[a];w1;w2);n - 1)
11. X ∈ moves:{f:strat2play(coW-game(a.B[a];w1;w2);n - 1;X)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(coW-game(a.B[a];w1;w2))| 
                                                                            Legal2(moves[(2 * n) - 1];p)} 
12. Y : s:win2strat(coW-game(a.B[a];w2;w3);n - 1) ⋂ moves:{f:strat2play(coW-game(a.B[a];w2;w3);n - 1;s)| 
                                                           ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(coW-game(a.B[a];w2;w3))| Lega\000Cl2(moves[(2 * n) - 1];p)} 
13. Y ∈ win2strat(coW-game(a.B[a];w2;w3);n - 1)
14. Y ∈ moves:{f:strat2play(coW-game(a.B[a];w2;w3);n - 1;Y)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(coW-game(a.B[a];w2;w3))| 
                                                                            Legal2(moves[(2 * n) - 1];p)} 
15. ∀k:ℕ. ((k ≤ n) ⇒ (X ∈ win2strat(coW-game(a.B[a];w1;w2);k)))
16. ∀k:ℕ. ((k ≤ n) ⇒ (Y ∈ win2strat(coW-game(a.B[a];w2;w3);k)))
17. moves : {f:strat2play(coW-game(a.B[a];w1;w3);n - 1;coW-trans(X; Y))| ||f|| = (2 * n) ∈ ℤ} 
18. k : ℤ
19. 0 ≤ (n - 1)
20. m1 : strat2play(coW-game(a.B[a];w1;w3);0;coW-trans(X; Y))
21. ||m1|| = 2 ∈ ℤ
22. z : copath(a.B[a];w1)
23. m1[1] = <z, ()> ∈ Pos(coW-game(a.B[a];w1;w3))
24. m1[0] = InitialPos(coW-game(a.B[a];w1;w3)) ∈ Pos(coW-game(a.B[a];w1;w3))
25. copath-length(z) = 1 ∈ ℤ
26. copathAgree(a.B[a];w1;();z)
27. seq-add(seq-add(seq-nil();<(), ()>);<z, ()>) ∈ {f:strat2play(coW-game(a.B[a];w1;w2);0;X)| ||f|| = 2 ∈ ℤ} 
28. mm : strat2play(coW-game(a.B[a];w1;w2);0;X)
29. ||mm|| = 2 ∈ ℤ
30. seq-add(seq-add(seq-nil();<(), ()>);<z, ()>) = mm ∈ {f:strat2play(coW-game(a.B[a];w1;w2);0;X)| ||f|| = 2 ∈ ℤ} 
31. X ∈ win2strat(coW-game(a.B[a];w1;w2);0)
32. X ∈ moves:{f:strat2play(coW-game(a.B[a];w1;w2);0;X)| ||f|| = 2 ∈ ℤ}  ⟶ {p:Pos(coW-game(a.B[a];w1;w2))| Legal2(moves\000C[1];p)} 
33. v1 : copath(a.B[a];w1)
34. v2 : copath(a.B[a];w2)
35. Legal2(mm[1];<v1, v2>)
36. (X mm) = <v1, v2> ∈ {p:Pos(coW-game(a.B[a];w1;w2))| Legal2(mm[1];p)} 
37. seq-add(seq-add(seq-nil();<(), ()>);<v2, ()>) ∈ strat2play(coW-game(a.B[a];w2;w3);0;Y)
38. p1 : strat2play(coW-game(a.B[a];w1;w2);0;X)
39. p2 : strat2play(coW-game(a.B[a];w2;w3);0;Y)
⊢ m1 ∈ sequence(Pos(coW-game(a.B[a];w1;w3)))
BY
{ (OnVar `m1' Strat2PlaySubtype THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type
3.  w1  :  coW(A;a.B[a])
4.  w2  :  coW(A;a.B[a])
5.  w3  :  coW(A;a.B[a])
6.  n  :  \mBbbZ{}
7.  0  <  n
8.  \mforall{}[X:win2strat(coW-game(a.B[a];w1;w2);n  -  1)].  \mforall{}[Y:win2strat(coW-game(a.B[a];w2;w3);n  -  1)].
          (coW-trans(X;  Y)  \mmember{}  win2strat(coW-game(a.B[a];w1;w3);n  -  1))
9.  X  :  s:win2strat(coW-game(a.B[a];w1;w2);n  -  1)
              \mcap{}  moves:\{f:strat2play(coW-game(a.B[a];w1;w2);n  -  1;s)|  ||f||  =  (2  *  n)\} 
              {}\mrightarrow{}  \{p:Pos(coW-game(a.B[a];w1;w2))|  Legal2(moves[(2  *  n)  -  1];p)\} 
10.  X  \mmember{}  win2strat(coW-game(a.B[a];w1;w2);n  -  1)
11.  X  \mmember{}  moves:\{f:strat2play(coW-game(a.B[a];w1;w2);n  -  1;X)|  ||f||  =  (2  *  n)\} 
        {}\mrightarrow{}  \{p:Pos(coW-game(a.B[a];w1;w2))|  Legal2(moves[(2  *  n)  -  1];p)\} 
12.  Y  :  s:win2strat(coW-game(a.B[a];w2;w3);n  -  1)
                \mcap{}  moves:\{f:strat2play(coW-game(a.B[a];w2;w3);n  -  1;s)|  ||f||  =  (2  *  n)\} 
                {}\mrightarrow{}  \{p:Pos(coW-game(a.B[a];w2;w3))|  Legal2(moves[(2  *  n)  -  1];p)\} 
13.  Y  \mmember{}  win2strat(coW-game(a.B[a];w2;w3);n  -  1)
14.  Y  \mmember{}  moves:\{f:strat2play(coW-game(a.B[a];w2;w3);n  -  1;Y)|  ||f||  =  (2  *  n)\} 
        {}\mrightarrow{}  \{p:Pos(coW-game(a.B[a];w2;w3))|  Legal2(moves[(2  *  n)  -  1];p)\} 
15.  \mforall{}k:\mBbbN{}.  ((k  \mleq{}  n)  {}\mRightarrow{}  (X  \mmember{}  win2strat(coW-game(a.B[a];w1;w2);k)))
16.  \mforall{}k:\mBbbN{}.  ((k  \mleq{}  n)  {}\mRightarrow{}  (Y  \mmember{}  win2strat(coW-game(a.B[a];w2;w3);k)))
17.  moves  :  \{f:strat2play(coW-game(a.B[a];w1;w3);n  -  1;coW-trans(X;  Y))|  ||f||  =  (2  *  n)\} 
18.  k  :  \mBbbZ{}
19.  0  \mleq{}  (n  -  1)
20.  m1  :  strat2play(coW-game(a.B[a];w1;w3);0;coW-trans(X;  Y))
21.  ||m1||  =  2
22.  z  :  copath(a.B[a];w1)
23.  m1[1]  =  <z,  ()>
24.  m1[0]  =  InitialPos(coW-game(a.B[a];w1;w3))
25.  copath-length(z)  =  1
26.  copathAgree(a.B[a];w1;();z)
27.  seq-add(seq-add(seq-nil();<(),  ()>);<z,  ()>)  \mmember{}  \{f:strat2play(coW-game(a.B[a];w1;w2);0;X)|  ||f||  \000C=  2\} 
28.  mm  :  strat2play(coW-game(a.B[a];w1;w2);0;X)
29.  ||mm||  =  2
30.  seq-add(seq-add(seq-nil();<(),  ()>);<z,  ()>)  =  mm
31.  X  \mmember{}  win2strat(coW-game(a.B[a];w1;w2);0)
32.  X  \mmember{}  moves:\{f:strat2play(coW-game(a.B[a];w1;w2);0;X)|  ||f||  =  2\}    {}\mrightarrow{}  \{p:Pos(coW-game(a.B[a];w1;w2\000C))| 
                                                                                                                            Legal2(moves[1];p)\} 
33.  v1  :  copath(a.B[a];w1)
34.  v2  :  copath(a.B[a];w2)
35.  Legal2(mm[1];<v1,  v2>)
36.  (X  mm)  =  <v1,  v2>
37.  seq-add(seq-add(seq-nil();<(),  ()>);<v2,  ()>)  \mmember{}  strat2play(coW-game(a.B[a];w2;w3);0;Y)
38.  p1  :  strat2play(coW-game(a.B[a];w1;w2);0;X)
39.  p2  :  strat2play(coW-game(a.B[a];w2;w3);0;Y)
\mvdash{}  m1  \mmember{}  sequence(Pos(coW-game(a.B[a];w1;w3)))


By

---

Latex:
(OnVar  `m1'  Strat2PlaySubtype  THEN  Auto)

---

Home Index