Step
*
1
2
2
1
1
1
2
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] = <fst(p1[(2 * n) - 1]), snd(p2[(2 * n) - 1])> ∈ Pos(coW-game(a.B[a];w1;w3))
26. (snd((X p1))) = (fst((Y p2))) ∈ copath(a.B[a];w2)
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. v2 : copath(a.B[a];w1)
31. v3 : copath(a.B[a];w2)
32. (X p1) = <v2, v3> ∈ {p:Pos(coW-game(a.B[a];w1;w2))| Legal2(p1[(2 * n) - 1];p)}
33. v4 : copath(a.B[a];w2)
34. v5 : copath(a.B[a];w3)
35. (Y p2) = <v4, v5> ∈ {p:Pos(coW-game(a.B[a];w2;w3))| Legal2(p2[(2 * n) - 1];p)}
36. v9 : copath(a.B[a];w1)
37. v10 : copath(a.B[a];w2)
38. p1[(2 * n) - 1] = <v9, v10> ∈ Pos(coW-game(a.B[a];w1;w2))
39. v7 : copath(a.B[a];w2)
40. v8 : copath(a.B[a];w3)
41. p2[(2 * n) - 1] = <v7, v8> ∈ Pos(coW-game(a.B[a];w2;w3))
42. ((copath-length(v7) = (n - 1) ∈ ℤ) ∧ (copath-length(v8) = n ∈ ℤ))
∨ ((copath-length(v7) = n ∈ ℤ) ∧ (copath-length(v8) = (n - 1) ∈ ℤ))
43. ((copath-length(v9) = (n - 1) ∈ ℤ) ∧ (copath-length(v10) = n ∈ ℤ))
∨ ((copath-length(v9) = n ∈ ℤ) ∧ (copath-length(v10) = (n - 1) ∈ ℤ))
44. (((copath-length(v2) = (copath-length(v9) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w1;v9;v2) ∧ (v10 = v3 ∈ copath(a.B[a];w2)))
∨ ((v9 = v2 ∈ copath(a.B[a];w1)) ∧ (copath-length(v3) = (copath-length(v10) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w2;v10;v3)))
∧ (copath-length(v2) = copath-length(v3) ∈ ℤ)
45. (((copath-length(v4) = (copath-length(v7) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w2;v7;v4) ∧ (v8 = v5 ∈ copath(a.B[a];w3)))
∨ ((v7 = v4 ∈ copath(a.B[a];w2)) ∧ (copath-length(v5) = (copath-length(v8) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w3;v8;v5)))
∧ (copath-length(v4) = copath-length(v5) ∈ ℤ)
46. ((copath-length(v10) = (copath-length(v7) + 1) ∈ ℤ) ∧ (copath-length(v10) = (copath-length(v9) + 1) ∈ ℤ))
∨ ((copath-length(v7) = (copath-length(v10) + 1) ∈ ℤ) ∧ (copath-length(v7) = (copath-length(v8) + 1) ∈ ℤ))
⊢ (((copath-length(v2) = (copath-length(v9) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w1;v9;v2) ∧ (v8 = v5 ∈ copath(a.B[a];w3)))
∨ ((v9 = v2 ∈ copath(a.B[a];w1)) ∧ (copath-length(v5) = (copath-length(v8) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w3;v8;v5)))
∧ (copath-length(v2) = copath-length(v5) ∈ ℤ)
BY
{ (Assert ⌜copath-length(v2) = copath-length(v5) ∈ ℤ⌝⋅ THENM (D 0 THEN Try (Trivial))) }
1
.....assertion.....
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] = <fst(p1[(2 * n) - 1]), snd(p2[(2 * n) - 1])> ∈ Pos(coW-game(a.B[a];w1;w3))
26. (snd((X p1))) = (fst((Y p2))) ∈ copath(a.B[a];w2)
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. v2 : copath(a.B[a];w1)
31. v3 : copath(a.B[a];w2)
32. (X p1) = <v2, v3> ∈ {p:Pos(coW-game(a.B[a];w1;w2))| Legal2(p1[(2 * n) - 1];p)}
33. v4 : copath(a.B[a];w2)
34. v5 : copath(a.B[a];w3)
35. (Y p2) = <v4, v5> ∈ {p:Pos(coW-game(a.B[a];w2;w3))| Legal2(p2[(2 * n) - 1];p)}
36. v9 : copath(a.B[a];w1)
37. v10 : copath(a.B[a];w2)
38. p1[(2 * n) - 1] = <v9, v10> ∈ Pos(coW-game(a.B[a];w1;w2))
39. v7 : copath(a.B[a];w2)
40. v8 : copath(a.B[a];w3)
41. p2[(2 * n) - 1] = <v7, v8> ∈ Pos(coW-game(a.B[a];w2;w3))
42. ((copath-length(v7) = (n - 1) ∈ ℤ) ∧ (copath-length(v8) = n ∈ ℤ))
∨ ((copath-length(v7) = n ∈ ℤ) ∧ (copath-length(v8) = (n - 1) ∈ ℤ))
43. ((copath-length(v9) = (n - 1) ∈ ℤ) ∧ (copath-length(v10) = n ∈ ℤ))
∨ ((copath-length(v9) = n ∈ ℤ) ∧ (copath-length(v10) = (n - 1) ∈ ℤ))
44. (((copath-length(v2) = (copath-length(v9) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w1;v9;v2) ∧ (v10 = v3 ∈ copath(a.B[a];w2)))
∨ ((v9 = v2 ∈ copath(a.B[a];w1)) ∧ (copath-length(v3) = (copath-length(v10) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w2;v10;v3)))
∧ (copath-length(v2) = copath-length(v3) ∈ ℤ)
45. (((copath-length(v4) = (copath-length(v7) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w2;v7;v4) ∧ (v8 = v5 ∈ copath(a.B[a];w3)))
∨ ((v7 = v4 ∈ copath(a.B[a];w2)) ∧ (copath-length(v5) = (copath-length(v8) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w3;v8;v5)))
∧ (copath-length(v4) = copath-length(v5) ∈ ℤ)
46. ((copath-length(v10) = (copath-length(v7) + 1) ∈ ℤ) ∧ (copath-length(v10) = (copath-length(v9) + 1) ∈ ℤ))
∨ ((copath-length(v7) = (copath-length(v10) + 1) ∈ ℤ) ∧ (copath-length(v7) = (copath-length(v8) + 1) ∈ ℤ))
⊢ copath-length(v2) = copath-length(v5) ∈ ℤ
2
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] = <fst(p1[(2 * n) - 1]), snd(p2[(2 * n) - 1])> ∈ Pos(coW-game(a.B[a];w1;w3))
26. (snd((X p1))) = (fst((Y p2))) ∈ copath(a.B[a];w2)
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. v2 : copath(a.B[a];w1)
31. v3 : copath(a.B[a];w2)
32. (X p1) = <v2, v3> ∈ {p:Pos(coW-game(a.B[a];w1;w2))| Legal2(p1[(2 * n) - 1];p)}
33. v4 : copath(a.B[a];w2)
34. v5 : copath(a.B[a];w3)
35. (Y p2) = <v4, v5> ∈ {p:Pos(coW-game(a.B[a];w2;w3))| Legal2(p2[(2 * n) - 1];p)}
36. v9 : copath(a.B[a];w1)
37. v10 : copath(a.B[a];w2)
38. p1[(2 * n) - 1] = <v9, v10> ∈ Pos(coW-game(a.B[a];w1;w2))
39. v7 : copath(a.B[a];w2)
40. v8 : copath(a.B[a];w3)
41. p2[(2 * n) - 1] = <v7, v8> ∈ Pos(coW-game(a.B[a];w2;w3))
42. ((copath-length(v7) = (n - 1) ∈ ℤ) ∧ (copath-length(v8) = n ∈ ℤ))
∨ ((copath-length(v7) = n ∈ ℤ) ∧ (copath-length(v8) = (n - 1) ∈ ℤ))
43. ((copath-length(v9) = (n - 1) ∈ ℤ) ∧ (copath-length(v10) = n ∈ ℤ))
∨ ((copath-length(v9) = n ∈ ℤ) ∧ (copath-length(v10) = (n - 1) ∈ ℤ))
44. (((copath-length(v2) = (copath-length(v9) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w1;v9;v2) ∧ (v10 = v3 ∈ copath(a.B[a];w2)))
∨ ((v9 = v2 ∈ copath(a.B[a];w1)) ∧ (copath-length(v3) = (copath-length(v10) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w2;v10;v3)))
∧ (copath-length(v2) = copath-length(v3) ∈ ℤ)
45. (((copath-length(v4) = (copath-length(v7) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w2;v7;v4) ∧ (v8 = v5 ∈ copath(a.B[a];w3)))
∨ ((v7 = v4 ∈ copath(a.B[a];w2)) ∧ (copath-length(v5) = (copath-length(v8) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w3;v8;v5)))
∧ (copath-length(v4) = copath-length(v5) ∈ ℤ)
46. ((copath-length(v10) = (copath-length(v7) + 1) ∈ ℤ) ∧ (copath-length(v10) = (copath-length(v9) + 1) ∈ ℤ))
∨ ((copath-length(v7) = (copath-length(v10) + 1) ∈ ℤ) ∧ (copath-length(v7) = (copath-length(v8) + 1) ∈ ℤ))
47. copath-length(v2) = copath-length(v5) ∈ ℤ
⊢ ((copath-length(v2) = (copath-length(v9) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w1;v9;v2) ∧ (v8 = v5 ∈ copath(a.B[a];w3)))
∨ ((v9 = v2 ∈ copath(a.B[a];w1)) ∧ (copath-length(v5) = (copath-length(v8) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w3;v8;v5))
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] = <fst(p1[(2 * n) - 1]), snd(p2[(2 * n) - 1])>
26. (snd((X p1))) = (fst((Y p2)))
27. transMoves(X;Y;moves) = <p1, p2>
28. 1 \mleq{} n
29. (2 * 1) \mleq{} (2 * n)
30. v2 : copath(a.B[a];w1)
31. v3 : copath(a.B[a];w2)
32. (X p1) = <v2, v3>
33. v4 : copath(a.B[a];w2)
34. v5 : copath(a.B[a];w3)
35. (Y p2) = <v4, v5>
36. v9 : copath(a.B[a];w1)
37. v10 : copath(a.B[a];w2)
38. p1[(2 * n) - 1] = <v9, v10>
39. v7 : copath(a.B[a];w2)
40. v8 : copath(a.B[a];w3)
41. p2[(2 * n) - 1] = <v7, v8>
42. ((copath-length(v7) = (n - 1)) \mwedge{} (copath-length(v8) = n))
\mvee{} ((copath-length(v7) = n) \mwedge{} (copath-length(v8) = (n - 1)))
43. ((copath-length(v9) = (n - 1)) \mwedge{} (copath-length(v10) = n))
\mvee{} ((copath-length(v9) = n) \mwedge{} (copath-length(v10) = (n - 1)))
44. (((copath-length(v2) = (copath-length(v9) + 1)) \mwedge{} copathAgree(a.B[a];w1;v9;v2) \mwedge{} (v10 = v3))
\mvee{} ((v9 = v2) \mwedge{} (copath-length(v3) = (copath-length(v10) + 1)) \mwedge{} copathAgree(a.B[a];w2;v10;v3)))
\mwedge{} (copath-length(v2) = copath-length(v3))
45. (((copath-length(v4) = (copath-length(v7) + 1)) \mwedge{} copathAgree(a.B[a];w2;v7;v4) \mwedge{} (v8 = v5))
\mvee{} ((v7 = v4) \mwedge{} (copath-length(v5) = (copath-length(v8) + 1)) \mwedge{} copathAgree(a.B[a];w3;v8;v5)))
\mwedge{} (copath-length(v4) = copath-length(v5))
46. ((copath-length(v10) = (copath-length(v7) + 1))
\mwedge{} (copath-length(v10) = (copath-length(v9) + 1)))
\mvee{} ((copath-length(v7) = (copath-length(v10) + 1)) \mwedge{} (copath-length(v7) = (copath-length(v8) + 1)))
\mvdash{} (((copath-length(v2) = (copath-length(v9) + 1)) \mwedge{} copathAgree(a.B[a];w1;v9;v2) \mwedge{} (v8 = v5))
\mvee{} ((v9 = v2) \mwedge{} (copath-length(v5) = (copath-length(v8) + 1)) \mwedge{} copathAgree(a.B[a];w3;v8;v5)))
\mwedge{} (copath-length(v2) = copath-length(v5))
By
Latex:
(Assert \mkleeneopen{}copath-length(v2) = copath-length(v5)\mkleeneclose{}\mcdot{} THENM (D 0 THEN Try (Trivial)))
Home
Index