Step
*
2
3
1
1
1
1
1
1
of Lemma
coW-play-invariant
1. i : ℤ
2. [A] : 𝕌'
3. B : A ⟶ Type
4. w : coW(A;a.B[a])
5. w' : coW(A;a.B[a])
6. n : ℕ
7. s : win2strat(coW-game(a.B[a];w;w');n)
8. moves : strat2play(coW-game(a.B[a];w;w');n;s)
9. moves[0] = InitialPos(coW-game(a.B[a];w;w')) ∈ Pos(coW-game(a.B[a];w;w'))
10. [%4] : 0 < i
11. ((i - 1) ≤ n)
⇒ (coW-pos-lens(moves[2 * (i - 1)];i - 1;i - 1)
∧ (coW-pos-lens(moves[(2 * (i - 1)) + 1];i - 1;(i - 1) + 1)
∨ coW-pos-lens(moves[(2 * (i - 1)) + 1];(i - 1) + 1;i - 1)))
12. ((i - 1) ≤ ((2 * n) + 1)) ⇒ (∀j:ℕ(i - 1) + 1. coW-pos-agree(a.B[a];w;w';moves[j];moves[i - 1]))
13. (i ≤ n)
⇒ (coW-pos-lens(moves[2 * i];i;i)
∧ (coW-pos-lens(moves[(2 * i) + 1];i;i + 1) ∨ coW-pos-lens(moves[(2 * i) + 1];i + 1;i)))
14. 1 ≤ i
15. i ≤ ((2 * n) + 1)
16. (i - 1) = ((((i - 1) ÷ 2) * 2) + 0) ∈ ℤ
17. 0 ≤ ((i - 1) ÷ 2)
18. (0 ≤ 0) ∧ 0 < 2
19. ↓Legal1(moves[i - 1];moves[i])
⊢ coW-pos-agree(a.B[a];w;w';moves[i - 1];moves[i])
BY
{ (MoveToConcl (-1)
THEN (GenConclTerm ⌜moves[i - 1]⌝⋅ THENA Auto)
THEN Thin (-1)
THEN RepUR ``sg-pos coW-game`` -1
THEN D -1
THEN (GenConclTerm ⌜moves[i]⌝⋅ THENA Auto)
THEN Thin (-1)
THEN RepUR ``sg-pos coW-game`` -1
THEN D -1
THEN RepUR ``sg-legal1 coW-game coW-pos-agree`` 0
THEN Auto) }
1
1. i : ℤ
2. [A] : 𝕌'
3. B : A ⟶ Type
4. w : coW(A;a.B[a])
5. w' : coW(A;a.B[a])
6. n : ℕ
7. s : win2strat(coW-game(a.B[a];w;w');n)
8. moves : strat2play(coW-game(a.B[a];w;w');n;s)
9. moves[0] = InitialPos(coW-game(a.B[a];w;w')) ∈ Pos(coW-game(a.B[a];w;w'))
10. [%4] : 0 < i
11. ((i - 1) ≤ n)
⇒ (coW-pos-lens(moves[2 * (i - 1)];i - 1;i - 1)
∧ (coW-pos-lens(moves[(2 * (i - 1)) + 1];i - 1;(i - 1) + 1)
∨ coW-pos-lens(moves[(2 * (i - 1)) + 1];(i - 1) + 1;i - 1)))
12. ((i - 1) ≤ ((2 * n) + 1)) ⇒ (∀j:ℕ(i - 1) + 1. coW-pos-agree(a.B[a];w;w';moves[j];moves[i - 1]))
13. (i ≤ n)
⇒ (coW-pos-lens(moves[2 * i];i;i)
∧ (coW-pos-lens(moves[(2 * i) + 1];i;i + 1) ∨ coW-pos-lens(moves[(2 * i) + 1];i + 1;i)))
14. 1 ≤ i
15. i ≤ ((2 * n) + 1)
16. (i - 1) = ((((i - 1) ÷ 2) * 2) + 0) ∈ ℤ
17. 0 ≤ ((i - 1) ÷ 2)
18. 0 ≤ 0
19. 0 < 2
20. v1 : copath(a.B[a];w)
21. v2 : copath(a.B[a];w')
22. v3 : copath(a.B[a];w)
23. v4 : copath(a.B[a];w')
24. [%21] : ((copath-length(v3) = (copath-length(v1) + 1) ∈ ℤ)
∧ copathAgree(a.B[a];w;v1;v3)
∧ (v2 = v4 ∈ copath(a.B[a];w')))
∨ ((v1 = v3 ∈ copath(a.B[a];w)) ∧ (copath-length(v4) = (copath-length(v2) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w';v2;v4))
⊢ copath-length(v1) ≤ copath-length(v3)
2
1. i : ℤ
2. [A] : 𝕌'
3. B : A ⟶ Type
4. w : coW(A;a.B[a])
5. w' : coW(A;a.B[a])
6. n : ℕ
7. s : win2strat(coW-game(a.B[a];w;w');n)
8. moves : strat2play(coW-game(a.B[a];w;w');n;s)
9. moves[0] = InitialPos(coW-game(a.B[a];w;w')) ∈ Pos(coW-game(a.B[a];w;w'))
10. [%4] : 0 < i
11. ((i - 1) ≤ n)
⇒ (coW-pos-lens(moves[2 * (i - 1)];i - 1;i - 1)
∧ (coW-pos-lens(moves[(2 * (i - 1)) + 1];i - 1;(i - 1) + 1)
∨ coW-pos-lens(moves[(2 * (i - 1)) + 1];(i - 1) + 1;i - 1)))
12. ((i - 1) ≤ ((2 * n) + 1)) ⇒ (∀j:ℕ(i - 1) + 1. coW-pos-agree(a.B[a];w;w';moves[j];moves[i - 1]))
13. (i ≤ n)
⇒ (coW-pos-lens(moves[2 * i];i;i)
∧ (coW-pos-lens(moves[(2 * i) + 1];i;i + 1) ∨ coW-pos-lens(moves[(2 * i) + 1];i + 1;i)))
14. 1 ≤ i
15. i ≤ ((2 * n) + 1)
16. (i - 1) = ((((i - 1) ÷ 2) * 2) + 0) ∈ ℤ
17. 0 ≤ ((i - 1) ÷ 2)
18. 0 ≤ 0
19. 0 < 2
20. v1 : copath(a.B[a];w)
21. v2 : copath(a.B[a];w')
22. v3 : copath(a.B[a];w)
23. v4 : copath(a.B[a];w')
24. ↓((copath-length(v3) = (copath-length(v1) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w;v1;v3) ∧ (v2 = v4 ∈ copath(a.B[a];w')))
∨ ((v1 = v3 ∈ copath(a.B[a];w)) ∧ (copath-length(v4) = (copath-length(v2) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w';v2;v4))
25. copath-length(v1) ≤ copath-length(v3)
⊢ copathAgree(a.B[a];w;v1;v3)
3
1. i : ℤ
2. [A] : 𝕌'
3. B : A ⟶ Type
4. w : coW(A;a.B[a])
5. w' : coW(A;a.B[a])
6. n : ℕ
7. s : win2strat(coW-game(a.B[a];w;w');n)
8. moves : strat2play(coW-game(a.B[a];w;w');n;s)
9. moves[0] = InitialPos(coW-game(a.B[a];w;w')) ∈ Pos(coW-game(a.B[a];w;w'))
10. [%4] : 0 < i
11. ((i - 1) ≤ n)
⇒ (coW-pos-lens(moves[2 * (i - 1)];i - 1;i - 1)
∧ (coW-pos-lens(moves[(2 * (i - 1)) + 1];i - 1;(i - 1) + 1)
∨ coW-pos-lens(moves[(2 * (i - 1)) + 1];(i - 1) + 1;i - 1)))
12. ((i - 1) ≤ ((2 * n) + 1)) ⇒ (∀j:ℕ(i - 1) + 1. coW-pos-agree(a.B[a];w;w';moves[j];moves[i - 1]))
13. (i ≤ n)
⇒ (coW-pos-lens(moves[2 * i];i;i)
∧ (coW-pos-lens(moves[(2 * i) + 1];i;i + 1) ∨ coW-pos-lens(moves[(2 * i) + 1];i + 1;i)))
14. 1 ≤ i
15. i ≤ ((2 * n) + 1)
16. (i - 1) = ((((i - 1) ÷ 2) * 2) + 0) ∈ ℤ
17. 0 ≤ ((i - 1) ÷ 2)
18. 0 ≤ 0
19. 0 < 2
20. v1 : copath(a.B[a];w)
21. v2 : copath(a.B[a];w')
22. v3 : copath(a.B[a];w)
23. v4 : copath(a.B[a];w')
24. [%24] : ((copath-length(v3) = (copath-length(v1) + 1) ∈ ℤ)
∧ copathAgree(a.B[a];w;v1;v3)
∧ (v2 = v4 ∈ copath(a.B[a];w')))
∨ ((v1 = v3 ∈ copath(a.B[a];w)) ∧ (copath-length(v4) = (copath-length(v2) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w';v2;v4))
25. copath-length(v1) ≤ copath-length(v3)
26. copathAgree(a.B[a];w;v1;v3)
⊢ copath-length(v2) ≤ copath-length(v4)
4
1. i : ℤ
2. [A] : 𝕌'
3. B : A ⟶ Type
4. w : coW(A;a.B[a])
5. w' : coW(A;a.B[a])
6. n : ℕ
7. s : win2strat(coW-game(a.B[a];w;w');n)
8. moves : strat2play(coW-game(a.B[a];w;w');n;s)
9. moves[0] = InitialPos(coW-game(a.B[a];w;w')) ∈ Pos(coW-game(a.B[a];w;w'))
10. [%4] : 0 < i
11. ((i - 1) ≤ n)
⇒ (coW-pos-lens(moves[2 * (i - 1)];i - 1;i - 1)
∧ (coW-pos-lens(moves[(2 * (i - 1)) + 1];i - 1;(i - 1) + 1)
∨ coW-pos-lens(moves[(2 * (i - 1)) + 1];(i - 1) + 1;i - 1)))
12. ((i - 1) ≤ ((2 * n) + 1)) ⇒ (∀j:ℕ(i - 1) + 1. coW-pos-agree(a.B[a];w;w';moves[j];moves[i - 1]))
13. (i ≤ n)
⇒ (coW-pos-lens(moves[2 * i];i;i)
∧ (coW-pos-lens(moves[(2 * i) + 1];i;i + 1) ∨ coW-pos-lens(moves[(2 * i) + 1];i + 1;i)))
14. 1 ≤ i
15. i ≤ ((2 * n) + 1)
16. (i - 1) = ((((i - 1) ÷ 2) * 2) + 0) ∈ ℤ
17. 0 ≤ ((i - 1) ÷ 2)
18. 0 ≤ 0
19. 0 < 2
20. v1 : copath(a.B[a];w)
21. v2 : copath(a.B[a];w')
22. v3 : copath(a.B[a];w)
23. v4 : copath(a.B[a];w')
24. ↓((copath-length(v3) = (copath-length(v1) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w;v1;v3) ∧ (v2 = v4 ∈ copath(a.B[a];w')))
∨ ((v1 = v3 ∈ copath(a.B[a];w)) ∧ (copath-length(v4) = (copath-length(v2) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w';v2;v4))
25. copath-length(v1) ≤ copath-length(v3)
26. copathAgree(a.B[a];w;v1;v3)
27. copath-length(v2) ≤ copath-length(v4)
⊢ copathAgree(a.B[a];w';v2;v4)
Latex:
Latex:
1. i : \mBbbZ{}
2. [A] : \mBbbU{}'
3. B : A {}\mrightarrow{} Type
4. w : coW(A;a.B[a])
5. w' : coW(A;a.B[a])
6. n : \mBbbN{}
7. s : win2strat(coW-game(a.B[a];w;w');n)
8. moves : strat2play(coW-game(a.B[a];w;w');n;s)
9. moves[0] = InitialPos(coW-game(a.B[a];w;w'))
10. [\%4] : 0 < i
11. ((i - 1) \mleq{} n)
{}\mRightarrow{} (coW-pos-lens(moves[2 * (i - 1)];i - 1;i - 1)
\mwedge{} (coW-pos-lens(moves[(2 * (i - 1)) + 1];i - 1;(i - 1) + 1)
\mvee{} coW-pos-lens(moves[(2 * (i - 1)) + 1];(i - 1) + 1;i - 1)))
12. ((i - 1) \mleq{} ((2 * n) + 1)) {}\mRightarrow{} (\mforall{}j:\mBbbN{}(i - 1) + 1. coW-pos-agree(a.B[a];w;w';moves[j];moves[i - 1]))
13. (i \mleq{} n)
{}\mRightarrow{} (coW-pos-lens(moves[2 * i];i;i)
\mwedge{} (coW-pos-lens(moves[(2 * i) + 1];i;i + 1) \mvee{} coW-pos-lens(moves[(2 * i) + 1];i + 1;i)))
14. 1 \mleq{} i
15. i \mleq{} ((2 * n) + 1)
16. (i - 1) = ((((i - 1) \mdiv{} 2) * 2) + 0)
17. 0 \mleq{} ((i - 1) \mdiv{} 2)
18. (0 \mleq{} 0) \mwedge{} 0 < 2
19. \mdownarrow{}Legal1(moves[i - 1];moves[i])
\mvdash{} coW-pos-agree(a.B[a];w;w';moves[i - 1];moves[i])
By
Latex:
(MoveToConcl (-1)
THEN (GenConclTerm \mkleeneopen{}moves[i - 1]\mkleeneclose{}\mcdot{} THENA Auto)
THEN Thin (-1)
THEN RepUR ``sg-pos coW-game`` -1
THEN D -1
THEN (GenConclTerm \mkleeneopen{}moves[i]\mkleeneclose{}\mcdot{} THENA Auto)
THEN Thin (-1)
THEN RepUR ``sg-pos coW-game`` -1
THEN D -1
THEN RepUR ``sg-legal1 coW-game coW-pos-agree`` 0
THEN Auto)
Home
Index