Step
*
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 : {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 : {f:strat2play(coW-game(a.B[a];w1;w3);0;coW-trans(X; Y))| ||f|| = ((2 * 0) + 2) ∈ ℤ}
⊢ transMoves(X;Y;m1) ∈ {p:strat2play(coW-game(a.B[a];w1;w2);0;X) × strat2play(coW-game(a.B[a];w2;w3);0;Y)|
let a,b = p
in coWtransInvariant(a.B[a];w1;w2;w3;0;X;Y;a;b;m1)}
BY
{ (D -1
THEN Reduce -1
THEN Unfold `transMoves` 0
THEN Unfold `play-len` -1
THEN HypSubst' (-1) 0
THEN Reduce 0
THEN Unfold `transMoves` 0
THEN (Subst' ||seq-truncate(m1;0)|| ~ 0 0
THENA (Computation THEN Unfold `strat2play` -2 THEN Reduce -2 THEN D -2 THEN D -3 THEN Reduce 0 THEN Auto)
)
THEN Reduce 0
THEN Fold `play-item` 0
THEN (GenConclTerm ⌜m1[1]⌝⋅ THENA Auto)
THEN RepUR ``sg-pos coW-game`` -2
THEN D -2
THEN Reduce 0
THEN (OnVar `m1' Strat2PlayInvariant THENA Auto)
THEN D -1
THEN (D -1 With ⌜0⌝ THENA Auto)
THEN D -1
THEN Thin (-1)
THEN D -1
THEN Reduce -1
THEN Fold `play-item` (-2)
THEN (RWO "-2 -3" (-1) THENA Auto)
THEN RepUR ``sg-legal1 sg-init coW-game`` -1
THEN ((D -1 THEN ExRepD)
THENL [(SubstFor ⌜copath-length(v1)⌝ 0⋅
THEN Reduce 0
THEN (SubstFor ⌜v2⌝ (-5)⋅ THENA Auto)
THEN ThinVar `v2'
THEN RenameVar `z' (-5))
; ((Subst' copath-length(v1) ~ 0 0 THENA (Auto THEN SubstFor ⌜v1⌝ 0⋅ THEN Auto))
THEN Reduce 0
THEN (SubstFor ⌜v1⌝ (-5)⋅ THENA Auto)
THEN ThinVar `v1'
THEN RenameVar `z' (-5))]
)) }
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 : ℤ
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)
⊢ let M1 = seq-add(seq-add(seq-nil();<(), ()>);<z, ()>) in
let M2 = seq-add(seq-add(seq-nil();<(), ()>);<snd((X M1)), ()>) in
<M1, M2> ∈ {p:strat2play(coW-game(a.B[a];w1;w2);0;X) × strat2play(coW-game(a.B[a];w2;w3);0;Y)|
let a,b = p
in coWtransInvariant(a.B[a];w1;w2;w3;0;X;Y;a;b;m1)}
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 : {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];w3)
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];w3;();z)
⊢ let M2 = seq-add(seq-add(seq-nil();<(), ()>);<(), z>) in
let M1 = seq-add(seq-add(seq-nil();<(), ()>);<(), fst((Y M2))>) in
<M1, M2> ∈ {p:strat2play(coW-game(a.B[a];w1;w2);0;X) × strat2play(coW-game(a.B[a];w2;w3);0;Y)|
let a,b = p
in coWtransInvariant(a.B[a];w1;w2;w3;0;X;Y;a;b;m1)}
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 : \{f:strat2play(coW-game(a.B[a];w1;w3);0;coW-trans(X; Y))| ||f|| = ((2 * 0) + 2)\}
\mvdash{} transMoves(X;Y;m1) \mmember{} \{p:strat2play(coW-game(a.B[a];w1;w2);0;X)
\mtimes{} strat2play(coW-game(a.B[a];w2;w3);0;Y)|
let a,b = p
in coWtransInvariant(a.B[a];w1;w2;w3;0;X;Y;a;b;m1)\}
By
Latex:
(D -1
THEN Reduce -1
THEN Unfold `transMoves` 0
THEN Unfold `play-len` -1
THEN HypSubst' (-1) 0
THEN Reduce 0
THEN Unfold `transMoves` 0
THEN (Subst' ||seq-truncate(m1;0)|| \msim{} 0 0
THENA (Computation
THEN Unfold `strat2play` -2
THEN Reduce -2
THEN D -2
THEN D -3
THEN Reduce 0
THEN Auto)
)
THEN Reduce 0
THEN Fold `play-item` 0
THEN (GenConclTerm \mkleeneopen{}m1[1]\mkleeneclose{}\mcdot{} THENA Auto)
THEN RepUR ``sg-pos coW-game`` -2
THEN D -2
THEN Reduce 0
THEN (OnVar `m1' Strat2PlayInvariant THENA Auto)
THEN D -1
THEN (D -1 With \mkleeneopen{}0\mkleeneclose{} THENA Auto)
THEN D -1
THEN Thin (-1)
THEN D -1
THEN Reduce -1
THEN Fold `play-item` (-2)
THEN (RWO "-2 -3" (-1) THENA Auto)
THEN RepUR ``sg-legal1 sg-init coW-game`` -1
THEN ((D -1 THEN ExRepD)
THENL [(SubstFor \mkleeneopen{}copath-length(v1)\mkleeneclose{} 0\mcdot{}
THEN Reduce 0
THEN (SubstFor \mkleeneopen{}v2\mkleeneclose{} (-5)\mcdot{} THENA Auto)
THEN ThinVar `v2'
THEN RenameVar `z' (-5))
; ((Subst' copath-length(v1) \msim{} 0 0 THENA (Auto THEN SubstFor \mkleeneopen{}v1\mkleeneclose{} 0\mcdot{} THEN Auto))
THEN Reduce 0
THEN (SubstFor \mkleeneopen{}v1\mkleeneclose{} (-5)\mcdot{} THENA Auto)
THEN ThinVar `v1'
THEN RenameVar `z' (-5))]
))
Home
Index