Step
*
1
2
2
1
1
1
2
of Lemma
coW-trans_wf
.....set predicate.....
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)}
⊢ Legal2(moves[(2 * n) - 1];<v2, v5>)
BY
{ ((Subst' (2 * (n - 1)) + 1 ~ (2 * n) - 1 -14 THENA Auto)
THEN Unfold `play-item` 0
THEN (RWO "-14" 0 THENA Auto)
THEN (Subst' (2 * (n - 1)) + 1 ~ (2 * n) - 1 -12 THENA Auto)
THEN MoveToConcl (-12)
THEN MoveToConcl (-2)
THEN MoveToConcl (-5)
THEN (((Assert coW-pos-lens(p1[(2 * n) - 1];n - 1;n) ∨ coW-pos-lens(p1[(2 * n) - 1];n;n - 1) BY
((InstLemma `coW-play-invariant` [⌜A⌝;⌜B⌝;⌜w1⌝;⌜w2⌝;⌜n - 1⌝;⌜X⌝;⌜p1⌝;⌜n - 1⌝]⋅ THENA Auto)
THEN (D -1 THEN (D -2 THENA Auto))
THEN D -1
THEN Subst' (n - 1) + 1 ~ n -1
THEN Auto
THEN Subst' (2 * (n - 1)) + 1 ~ (2 * n) - 1 -1
THEN Auto))
THEN MoveToConcl (-1)
)
THEN (Assert coW-pos-lens(p2[(2 * n) - 1];n - 1;n) ∨ coW-pos-lens(p2[(2 * n) - 1];n;n - 1) BY
((InstLemma `coW-play-invariant` [⌜A⌝;⌜B⌝;⌜w2⌝;⌜w3⌝;⌜n - 1⌝;⌜Y⌝;⌜p2⌝;⌜n - 1⌝]⋅ THENA Auto)
THEN (D -1 THEN (D -2 THENA Auto))
THEN D -1
THEN Subst' (n - 1) + 1 ~ n -1
THEN Auto
THEN Subst' (2 * (n - 1)) + 1 ~ (2 * n) - 1 -1
THEN Auto))
THEN MoveToConcl (-1))
THEN GenConclTerms Auto [⌜p1[(2 * n) - 1]⌝;⌜p2[(2 * n) - 1]⌝]⋅
THEN (RepUR ``sg-pos coW-game`` -4 THEN RepUR ``sg-pos coW-game`` -2 THEN DProds)
THEN RepUR ``coW-pos-lens sg-legal2 coW-game`` 0
THEN RepeatFor 5 ((D 0 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 : 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) ∈ ℤ)
Latex:
Latex:
.....set predicate.....
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{} Legal2(moves[(2 * n) - 1];<v2, v5>)
By
Latex:
((Subst' (2 * (n - 1)) + 1 \msim{} (2 * n) - 1 -14 THENA Auto)
THEN Unfold `play-item` 0
THEN (RWO "-14" 0 THENA Auto)
THEN (Subst' (2 * (n - 1)) + 1 \msim{} (2 * n) - 1 -12 THENA Auto)
THEN MoveToConcl (-12)
THEN MoveToConcl (-2)
THEN MoveToConcl (-5)
THEN (((Assert coW-pos-lens(p1[(2 * n) - 1];n - 1;n) \mvee{} coW-pos-lens(p1[(2 * n) - 1];n;n - 1) BY
((InstLemma `coW-play-invariant` [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}w1\mkleeneclose{};\mkleeneopen{}w2\mkleeneclose{};\mkleeneopen{}n - 1\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}p1\mkleeneclose{};\mkleeneopen{}n - 1\mkleeneclose{}]\mcdot{}
THENA Auto
)
THEN (D -1 THEN (D -2 THENA Auto))
THEN D -1
THEN Subst' (n - 1) + 1 \msim{} n -1
THEN Auto
THEN Subst' (2 * (n - 1)) + 1 \msim{} (2 * n) - 1 -1
THEN Auto))
THEN MoveToConcl (-1)
)
THEN (Assert coW-pos-lens(p2[(2 * n) - 1];n - 1;n) \mvee{} coW-pos-lens(p2[(2 * n) - 1];n;n - 1) BY
((InstLemma `coW-play-invariant` [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}w2\mkleeneclose{};\mkleeneopen{}w3\mkleeneclose{};\mkleeneopen{}n - 1\mkleeneclose{};\mkleeneopen{}Y\mkleeneclose{};\mkleeneopen{}p2\mkleeneclose{};\mkleeneopen{}n - 1\mkleeneclose{}]\mcdot{}
THENA Auto
)
THEN (D -1 THEN (D -2 THENA Auto))
THEN D -1
THEN Subst' (n - 1) + 1 \msim{} n -1
THEN Auto
THEN Subst' (2 * (n - 1)) + 1 \msim{} (2 * n) - 1 -1
THEN Auto))
THEN MoveToConcl (-1))
THEN GenConclTerms Auto [\mkleeneopen{}p1[(2 * n) - 1]\mkleeneclose{};\mkleeneopen{}p2[(2 * n) - 1]\mkleeneclose{}]\mcdot{}
THEN (RepUR ``sg-pos coW-game`` -4 THEN RepUR ``sg-pos coW-game`` -2 THEN DProds)
THEN RepUR ``coW-pos-lens sg-legal2 coW-game`` 0
THEN RepeatFor 5 ((D 0 THENA Auto)))
Home
Index