---

Step * 1 2 2 1 1 1 1 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 : strat2play(coW-game(a.B[a];w1;w3);n - 1;coW-trans(X; Y))
18. ||moves|| = (2 * n) ∈ ℤ
19. ∀k:ℕ
      ∀[moves:{f:strat2play(coW-game(a.B[a];w1;w3);k;coW-trans(X; Y))| ||f|| = ((2 * k) + 2) ∈ ℤ} ]
        (transMoves(X;Y;moves) ∈ {p:strat2play(coW-game(a.B[a];w1;w2);k;X) × strat2play(coW-game(a.B[a];w2;w3);k;Y)| 
                                  let a,b = p 
                                  in coWtransInvariant(a.B[a];w1;w2;w3;k;X;Y;a;b;moves)} ) 
      supposing k ≤ (n - 1)
20. transMoves(X;Y;moves) ∈ {p:strat2play(coW-game(a.B[a];w1;w2);n - 1;X) × strat2play(coW-game(a.B[a];w2;w3);n - 1;Y)| 
                             let a,b = p 
                             in coWtransInvariant(a.B[a];w1;w2;w3;n - 1;X;Y;a;b;moves)} 
21. p1 : strat2play(coW-game(a.B[a];w1;w2);n - 1;X)
22. p2 : strat2play(coW-game(a.B[a];w2;w3);n - 1;Y)
23. ||p1|| = ((2 * (n - 1)) + 2) ∈ ℤ
24. ||p2|| = ((2 * (n - 1)) + 2) ∈ ℤ
25. moves[(2 * (n - 1)) + 1] = <fst(p1[(2 * (n - 1)) + 1]), snd(p2[(2 * (n - 1)) + 1])> ∈ Pos(coW-game(a.B[a];w1;w3))
26. (snd((X p1))) = (fst((Y p2))) ∈ copath(a.B[a];w2)
27. ((copath-length(snd(p1[(2 * (n - 1)) + 1])) = (copath-length(fst(p2[(2 * (n - 1)) + 1])) + 1) ∈ ℤ)
∧ (copath-length(snd(p1[(2 * (n - 1)) + 1])) = (copath-length(fst(p1[(2 * (n - 1)) + 1])) + 1) ∈ ℤ))
∨ ((copath-length(fst(p2[(2 * (n - 1)) + 1])) = (copath-length(snd(p1[(2 * (n - 1)) + 1])) + 1) ∈ ℤ)
  ∧ (copath-length(fst(p2[(2 * (n - 1)) + 1])) = (copath-length(snd(p2[(2 * (n - 1)) + 1])) + 1) ∈ ℤ))
28. transMoves(X;Y;moves)
= <p1, p2>
∈ {p:strat2play(coW-game(a.B[a];w1;w2);n - 1;X) × strat2play(coW-game(a.B[a];w2;w3);n - 1;Y)| 
   let a,b = p 
   in coWtransInvariant(a.B[a];w1;w2;w3;n - 1;X;Y;a;b;moves)} 
29. 1 ≤ n
30. (2 * 1) ≤ (2 * n)
31. v2 : copath(a.B[a];w1)
32. v3 : copath(a.B[a];w2)
33. Legal2(p1[(2 * n) - 1];<v2, v3>)
34. (X p1) = <v2, v3> ∈ {p:Pos(coW-game(a.B[a];w1;w2))| Legal2(p1[(2 * n) - 1];p)} 
35. v4 : copath(a.B[a];w2)
36. v5 : copath(a.B[a];w3)
37. Legal2(p2[(2 * n) - 1];<v4, v5>)
38. (Y p2) = <v4, v5> ∈ {p:Pos(coW-game(a.B[a];w2;w3))| Legal2(p2[(2 * n) - 1];p)} 
⊢ <v2, v5> ∈ Pos(coW-game(a.B[a];w1;w3))
BY
{ (RepUR ``sg-pos coW-game`` 0 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  :  strat2play(coW-game(a.B[a];w1;w3);n  -  1;coW-trans(X;  Y))
18.  ||moves||  =  (2  *  n)
19.  \mforall{}k:\mBbbN{}
            \mforall{}[moves:\{f:strat2play(coW-game(a.B[a];w1;w3);k;coW-trans(X;  Y))|  ||f||  =  ((2  *  k)  +  2)\}  ]
                (transMoves(X;Y;moves)  \mmember{}  \{p:strat2play(coW-game(a.B[a];w1;w2);k;X)
                                                                    \mtimes{}  strat2play(coW-game(a.B[a];w2;w3);k;Y)| 
                                                                    let  a,b  =  p 
                                                                    in  coWtransInvariant(a.B[a];w1;w2;w3;k;X;Y;a;b;moves)\}  ) 
            supposing  k  \mleq{}  (n  -  1)
20.  transMoves(X;Y;moves)  \mmember{}  \{p:strat2play(coW-game(a.B[a];w1;w2);n  -  1;X)
                                                          \mtimes{}  strat2play(coW-game(a.B[a];w2;w3);n  -  1;Y)| 
                                                          let  a,b  =  p 
                                                          in  coWtransInvariant(a.B[a];w1;w2;w3;n  -  1;X;Y;a;b;moves)\} 
21.  p1  :  strat2play(coW-game(a.B[a];w1;w2);n  -  1;X)
22.  p2  :  strat2play(coW-game(a.B[a];w2;w3);n  -  1;Y)
23.  ||p1||  =  ((2  *  (n  -  1))  +  2)
24.  ||p2||  =  ((2  *  (n  -  1))  +  2)
25.  moves[(2  *  (n  -  1))  +  1]  =  <fst(p1[(2  *  (n  -  1))  +  1]),  snd(p2[(2  *  (n  -  1))  +  1])>
26.  (snd((X  p1)))  =  (fst((Y  p2)))
27.  ((copath-length(snd(p1[(2  *  (n  -  1))  +  1]))  =  (copath-length(fst(p2[(2  *  (n  -  1))  +  1]))  +  1))
\mwedge{}  (copath-length(snd(p1[(2  *  (n  -  1))  +  1]))  =  (copath-length(fst(p1[(2  *  (n  -  1))  +  1]))  +  1)))
\mvee{}  ((copath-length(fst(p2[(2  *  (n  -  1))  +  1]))  =  (copath-length(snd(p1[(2  *  (n  -  1))  +  1]))  +  1))
    \mwedge{}  (copath-length(fst(p2[(2  *  (n  -  1))  +  1]))  =  (copath-length(snd(p2[(2  *  (n  -  1))  +  1]))  +  1)))
28.  transMoves(X;Y;moves)  =  <p1,  p2>
29.  1  \mleq{}  n
30.  (2  *  1)  \mleq{}  (2  *  n)
31.  v2  :  copath(a.B[a];w1)
32.  v3  :  copath(a.B[a];w2)
33.  Legal2(p1[(2  *  n)  -  1];<v2,  v3>)
34.  (X  p1)  =  <v2,  v3>
35.  v4  :  copath(a.B[a];w2)
36.  v5  :  copath(a.B[a];w3)
37.  Legal2(p2[(2  *  n)  -  1];<v4,  v5>)
38.  (Y  p2)  =  <v4,  v5>
\mvdash{}  <v2,  v5>  \mmember{}  Pos(coW-game(a.B[a];w1;w3))


By

---

Latex:
(RepUR  ``sg-pos  coW-game``  0  THEN  Auto)

---

Home Index