Step
*
2
1
1
1
1
2
1
1
1
of Lemma
coW-game-step-isom
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. t : coW-dom(a.B[a];w)
6. b : coW-dom(a.B[a];w')
7. λp.let u,v = p
in <copath-cons(t;u), copath-cons(b;v)> ∈ Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
⟶ Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>)
8. Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>) ⊆r {p:copath(a.B[a];w) × copath(a.B[a];w')|
let p1,p2 = p
in (0 < copath-length(p1) ∧ (copath-hd(p1) = t ∈ coW-dom(a.B[a];w)))
∧ 0 < copath-length(p2)
∧ (copath-hd(p2) = b ∈ coW-dom(a.B[a];w'))}
9. p1 : copath(a.B[a];w)
10. p2 : copath(a.B[a];w')
11. f : sequence(Pos(coW-game(a.B[a];w;w')))
12. 0 < ||f||
13. f[0] = <copath-cons(t;()), copath-cons(b;())> ∈ Pos(coW-game(a.B[a];w;w'))
14. f[||f|| - 1] = <p1, p2> ∈ Pos(coW-game(a.B[a];w;w'))
15. ∀i:ℕ. ((2 * i) + 1 < ||f|| ⇒ (↓Legal1(f[2 * i];f[(2 * i) + 1])))
16. ∀i:ℕ+. (2 * i < ||f|| ⇒ (↓Legal2(f[(2 * i) - 1];f[2 * i])))
17. 0 < copath-length(p1)
18. copath-hd(p1) = t ∈ coW-dom(a.B[a];w)
19. 0 < copath-length(p2)
20. copath-hd(p2) = b ∈ coW-dom(a.B[a];w')
21. ∀q:Pos(coW-game(a.B[a];w;w')). (sg-reachable(coW-game(a.B[a];w;w');<copath-cons(t;()), copath-cons(b;())>;q) ⇒ coW-\000Cpos-agree(a.B[a];w;w';<copath-cons(t;()), copath-cons(b;())>;q))
⊢ sg-reachable(coW-game(a.B[a];coW-item(w;t);coW-item(w';b));<(), ()>;<copath-tl(p1), copath-tl(p2)>)
BY
{ (Assert ∀i:ℕ||f||. coW-pos-agree(a.B[a];w;w';<copath-cons(t;()), copath-cons(b;())>;f[i]) BY
((D 0 THENA Auto)
THEN BackThruSomeHyp
THEN (D 0 With ⌜seq-truncate(f;i + 1)⌝ THENW Auto)
THEN RWW "seq-len-truncate seq-truncate-item" 0
THEN Auto)) }
1
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. t : coW-dom(a.B[a];w)
6. b : coW-dom(a.B[a];w')
7. λp.let u,v = p
in <copath-cons(t;u), copath-cons(b;v)> ∈ Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
⟶ Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>)
8. Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>) ⊆r {p:copath(a.B[a];w) × copath(a.B[a];w')|
let p1,p2 = p
in (0 < copath-length(p1) ∧ (copath-hd(p1) = t ∈ coW-dom(a.B[a];w)))
∧ 0 < copath-length(p2)
∧ (copath-hd(p2) = b ∈ coW-dom(a.B[a];w'))}
9. p1 : copath(a.B[a];w)
10. p2 : copath(a.B[a];w')
11. f : sequence(Pos(coW-game(a.B[a];w;w')))
12. 0 < ||f||
13. f[0] = <copath-cons(t;()), copath-cons(b;())> ∈ Pos(coW-game(a.B[a];w;w'))
14. f[||f|| - 1] = <p1, p2> ∈ Pos(coW-game(a.B[a];w;w'))
15. ∀i:ℕ. ((2 * i) + 1 < ||f|| ⇒ (↓Legal1(f[2 * i];f[(2 * i) + 1])))
16. ∀i:ℕ+. (2 * i < ||f|| ⇒ (↓Legal2(f[(2 * i) - 1];f[2 * i])))
17. 0 < copath-length(p1)
18. copath-hd(p1) = t ∈ coW-dom(a.B[a];w)
19. 0 < copath-length(p2)
20. copath-hd(p2) = b ∈ coW-dom(a.B[a];w')
21. ∀q:Pos(coW-game(a.B[a];w;w')). (sg-reachable(coW-game(a.B[a];w;w');<copath-cons(t;()), copath-cons(b;())>;q) ⇒ coW-\000Cpos-agree(a.B[a];w;w';<copath-cons(t;()), copath-cons(b;())>;q))
22. ∀i:ℕ||f||. coW-pos-agree(a.B[a];w;w';<copath-cons(t;()), copath-cons(b;())>;f[i])
⊢ sg-reachable(coW-game(a.B[a];coW-item(w;t);coW-item(w';b));<(), ()>;<copath-tl(p1), copath-tl(p2)>)
Latex:
Latex:
1. A : \mBbbU{}'
2. B : A {}\mrightarrow{} Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. t : coW-dom(a.B[a];w)
6. b : coW-dom(a.B[a];w')
7. \mlambda{}p.let u,v = p
in <copath-cons(t;u), copath-cons(b;v)>
\mmember{} Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
{}\mrightarrow{} Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>)
8. Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>) \msubseteq{}r \{p:copath(a.B[a];w) \mtimes{} copath\000C(a.B[a];w')|
let p1,p2 = p
in (0 < copath-length(p1) \mwedge{} (copath-hd(p1) = t))
\mwedge{} 0 < copath-length(p2)
\mwedge{} (copath-hd(p2) = b)\}
9. p1 : copath(a.B[a];w)
10. p2 : copath(a.B[a];w')
11. f : sequence(Pos(coW-game(a.B[a];w;w')))
12. 0 < ||f||
13. f[0] = <copath-cons(t;()), copath-cons(b;())>
14. f[||f|| - 1] = <p1, p2>
15. \mforall{}i:\mBbbN{}. ((2 * i) + 1 < ||f|| {}\mRightarrow{} (\mdownarrow{}Legal1(f[2 * i];f[(2 * i) + 1])))
16. \mforall{}i:\mBbbN{}\msupplus{}. (2 * i < ||f|| {}\mRightarrow{} (\mdownarrow{}Legal2(f[(2 * i) - 1];f[2 * i])))
17. 0 < copath-length(p1)
18. copath-hd(p1) = t
19. 0 < copath-length(p2)
20. copath-hd(p2) = b
21. \mforall{}q:Pos(coW-game(a.B[a];w;w'))
(sg-reachable(coW-game(a.B[a];w;w');<copath-cons(t;()), copath-cons(b;())>q)
{}\mRightarrow{} coW-pos-agree(a.B[a];w;w';<copath-cons(t;()), copath-cons(b;())>q))
\mvdash{} sg-reachable(coW-game(a.B[a];coW-item(w;t);coW-item(w';b));<(), ()><copath-tl(p1), copath-tl(p2)>\000C)
By
Latex:
(Assert \mforall{}i:\mBbbN{}||f||. coW-pos-agree(a.B[a];w;w';<copath-cons(t;()), copath-cons(b;())>f[i]) BY
((D 0 THENA Auto)
THEN BackThruSomeHyp
THEN (D 0 With \mkleeneopen{}seq-truncate(f;i + 1)\mkleeneclose{} THENW Auto)
THEN RWW "seq-len-truncate seq-truncate-item" 0
THEN Auto))
Home
Index