Step
*
1
2
2
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 : {f:strat2play(coW-game(a.B[a];w1;w3);n - 1;coW-trans(X; Y))| ||f|| = (2 * n) ∈ ℤ}
18. ∀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)
19. 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)}
20. p1 : strat2play(coW-game(a.B[a];w1;w2);n - 1;X)
21. p2 : strat2play(coW-game(a.B[a];w2;w3);n - 1;Y)
22. ||p1|| = ((2 * (n - 1)) + 2) ∈ ℤ
23. ||p2|| = ((2 * (n - 1)) + 2) ∈ ℤ
24. 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))
25. (snd((X p1))) = (fst((Y p2))) ∈ copath(a.B[a];w2)
26. ((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) ∈ ℤ))
27. 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)}
⊢ let u,x = X p1
in let x,v = Y p2
in <u, v> ∈ {p:Pos(coW-game(a.B[a];w1;w3))| Legal2(moves[(2 * n) - 1];p)}
BY
{ ((Assert 1 ≤ n BY
Auto)
THEN (Mul ⌜2⌝ (-1)⋅ THENA Auto)
THEN (GenConclTerm ⌜X p1⌝⋅ THENA Auto)
THEN (GenConclTerm ⌜Y p2⌝⋅ THENA Auto)) }
1
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:ℕ
∀[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)
19. 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)}
20. p1 : strat2play(coW-game(a.B[a];w1;w2);n - 1;X)
21. p2 : strat2play(coW-game(a.B[a];w2;w3);n - 1;Y)
22. ||p1|| = ((2 * (n - 1)) + 2) ∈ ℤ
23. ||p2|| = ((2 * (n - 1)) + 2) ∈ ℤ
24. 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))
25. (snd((X p1))) = (fst((Y p2))) ∈ copath(a.B[a];w2)
26. ((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) ∈ ℤ))
27. 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)}
28. 1 ≤ n
29. (2 * 1) ≤ (2 * n)
30. v : {p:Pos(coW-game(a.B[a];w1;w2))| Legal2(p1[(2 * n) - 1];p)}
31. (X p1) = v ∈ {p:Pos(coW-game(a.B[a];w1;w2))| Legal2(p1[(2 * n) - 1];p)}
32. v1 : {p:Pos(coW-game(a.B[a];w2;w3))| Legal2(p2[(2 * n) - 1];p)}
33. (Y p2) = v1 ∈ {p:Pos(coW-game(a.B[a];w2;w3))| Legal2(p2[(2 * n) - 1];p)}
⊢ let u,x = v
in let x,v = v1
in <u, v> ∈ {p:Pos(coW-game(a.B[a];w1;w3))| Legal2(moves[(2 * n) - 1];p)}
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. \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)
19. 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)\}
20. p1 : strat2play(coW-game(a.B[a];w1;w2);n - 1;X)
21. p2 : strat2play(coW-game(a.B[a];w2;w3);n - 1;Y)
22. ||p1|| = ((2 * (n - 1)) + 2)
23. ||p2|| = ((2 * (n - 1)) + 2)
24. moves[(2 * (n - 1)) + 1] = <fst(p1[(2 * (n - 1)) + 1]), snd(p2[(2 * (n - 1)) + 1])>
25. (snd((X p1))) = (fst((Y p2)))
26. ((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)))
27. transMoves(X;Y;moves) = <p1, p2>
\mvdash{} let u,x = X p1
in let x,v = Y p2
in <u, v> \mmember{} \{p:Pos(coW-game(a.B[a];w1;w3))| Legal2(moves[(2 * n) - 1];p)\}
By
Latex:
((Assert 1 \mleq{} n BY
Auto)
THEN (Mul \mkleeneopen{}2\mkleeneclose{} (-1)\mcdot{} THENA Auto)
THEN (GenConclTerm \mkleeneopen{}X p1\mkleeneclose{}\mcdot{} THENA Auto)
THEN (GenConclTerm \mkleeneopen{}Y p2\mkleeneclose{}\mcdot{} THENA Auto))
Home
Index