Step
*
2
1
2
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. λp.let u,v = p
in <copath-tl(u), copath-tl(v)> ∈ Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>) ⟶ Pos(sg-norm\000Calize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
⊢ sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))) ≅ coW-game(a.B[a];w;w')@<copath-cons(t;())
, copath-cons(b;())
>
BY
{ ((D 0 With ⌜λp.let u,v = p in <copath-cons(t;u), copath-cons(b;v)>⌝ THENA Auto)
THEN D 0 With ⌜λp.let u,v = p
in <copath-tl(u), copath-tl(v)>⌝
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. λp.let u,v = p
in <copath-tl(u), copath-tl(v)> ∈ Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>) ⟶ Pos(sg-norm\000Calize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
10. x : Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
11. y : Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
12. Legal1(x;y)
⊢ Legal1((λp.let u,v = p in <copath-cons(t;u), copath-cons(b;v)>) x;(λp.let u,v = p
in <copath-cons(t;u), copath-cons(b;v)>)
y)
2
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. λp.let u,v = p
in <copath-tl(u), copath-tl(v)> ∈ Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>) ⟶ Pos(sg-norm\000Calize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
10. ∀x,y:Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b)))).
(Legal1(x;y)
⇒ Legal1((λp.let u,v = p in <copath-cons(t;u), copath-cons(b;v)>) x;(λp.let u,v = p
in <copath-cons(t;u), copath-cons(b;v)>)
y))
11. x : Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
12. y : Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
13. Legal2(x;y)
⊢ Legal2((λp.let u,v = p in <copath-cons(t;u), copath-cons(b;v)>) x;(λp.let u,v = p
in <copath-cons(t;u), copath-cons(b;v)>)
y)
3
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. λp.let u,v = p
in <copath-tl(u), copath-tl(v)> ∈ Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>) ⟶ Pos(sg-norm\000Calize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
10. ∀x,y:Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b)))).
(Legal1(x;y)
⇒ Legal1((λp.let u,v = p in <copath-cons(t;u), copath-cons(b;v)>) x;(λp.let u,v = p
in <copath-cons(t;u), copath-cons(b;v)>)
y))
11. ∀x,y:Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b)))).
(Legal2(x;y)
⇒ Legal2((λp.let u,v = p in <copath-cons(t;u), copath-cons(b;v)>) x;(λp.let u,v = p
in <copath-cons(t;u), copath-cons(b;v)>)
y))
12. x : Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>)
13. y : Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>)
14. Legal1(x;y)
⊢ Legal1((λp.let u,v = p in <copath-tl(u), copath-tl(v)>) x;(λp.let u,v = p in <copath-tl(u), copath-tl(v)>) y)
4
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. λp.let u,v = p
in <copath-tl(u), copath-tl(v)> ∈ Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>) ⟶ Pos(sg-norm\000Calize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
10. ∀x,y:Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b)))).
(Legal1(x;y)
⇒ Legal1((λp.let u,v = p in <copath-cons(t;u), copath-cons(b;v)>) x;(λp.let u,v = p
in <copath-cons(t;u), copath-cons(b;v)>)
y))
11. ∀x,y:Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b)))).
(Legal2(x;y)
⇒ Legal2((λp.let u,v = p in <copath-cons(t;u), copath-cons(b;v)>) x;(λp.let u,v = p
in <copath-cons(t;u), copath-cons(b;v)>)
y))
12. ∀x,y:Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>).
(Legal1(x;y)
⇒ Legal1((λp.let u,v = p in <copath-tl(u), copath-tl(v)>) x;(λp.let u,v = p in <copath-tl(u), copath-tl(v)>) y))
13. x : Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>)
14. y : Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>)
15. Legal2(x;y)
⊢ Legal2((λp.let u,v = p in <copath-tl(u), copath-tl(v)>) x;(λp.let u,v = p in <copath-tl(u), copath-tl(v)>) y)
5
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. λp.let u,v = p
in <copath-tl(u), copath-tl(v)> ∈ Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>) ⟶ Pos(sg-norm\000Calize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
10. ∀x,y:Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b)))).
(Legal1(x;y)
⇒ Legal1((λp.let u,v = p in <copath-cons(t;u), copath-cons(b;v)>) x;(λp.let u,v = p
in <copath-cons(t;u), copath-cons(b;v)>)
y))
11. ∀x,y:Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b)))).
(Legal2(x;y)
⇒ Legal2((λp.let u,v = p in <copath-cons(t;u), copath-cons(b;v)>) x;(λp.let u,v = p
in <copath-cons(t;u), copath-cons(b;v)>)
y))
12. ∀x,y:Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>).
(Legal1(x;y)
⇒ Legal1((λp.let u,v = p in <copath-tl(u), copath-tl(v)>) x;(λp.let u,v = p in <copath-tl(u), copath-tl(v)>) y))
13. ∀x,y:Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>).
(Legal2(x;y)
⇒ Legal2((λp.let u,v = p in <copath-tl(u), copath-tl(v)>) x;(λp.let u,v = p in <copath-tl(u), copath-tl(v)>) y))
14. x : Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>)
⊢ ((λp.let u,v = p in <copath-cons(t;u), copath-cons(b;v)>) ((λp.let u,v = p in <copath-tl(u), copath-tl(v)>) x))
= x
∈ Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>)
6
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. λp.let u,v = p
in <copath-tl(u), copath-tl(v)> ∈ Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>) ⟶ Pos(sg-norm\000Calize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
10. ∀x,y:Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b)))).
(Legal1(x;y)
⇒ Legal1((λp.let u,v = p in <copath-cons(t;u), copath-cons(b;v)>) x;(λp.let u,v = p
in <copath-cons(t;u), copath-cons(b;v)>)
y))
11. ∀x,y:Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b)))).
(Legal2(x;y)
⇒ Legal2((λp.let u,v = p in <copath-cons(t;u), copath-cons(b;v)>) x;(λp.let u,v = p
in <copath-cons(t;u), copath-cons(b;v)>)
y))
12. ∀x,y:Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>).
(Legal1(x;y)
⇒ Legal1((λp.let u,v = p in <copath-tl(u), copath-tl(v)>) x;(λp.let u,v = p in <copath-tl(u), copath-tl(v)>) y))
13. ∀x,y:Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>).
(Legal2(x;y)
⇒ Legal2((λp.let u,v = p in <copath-tl(u), copath-tl(v)>) x;(λp.let u,v = p in <copath-tl(u), copath-tl(v)>) y))
14. ∀x:Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>)
(((λp.let u,v = p in <copath-cons(t;u), copath-cons(b;v)>) ((λp.let u,v = p in <copath-tl(u), copath-tl(v)>) x))
= x
∈ Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>))
15. x : Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
⊢ ((λp.let u,v = p in <copath-tl(u), copath-tl(v)>) ((λp.let u,v = p in <copath-cons(t;u), copath-cons(b;v)>) x))
= x
∈ Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
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. \mlambda{}p.let u,v = p
in <copath-tl(u), copath-tl(v)> \mmember{} Pos(coW-game(a.B[a];w;w')@<copath-cons(t;())
, copath-cons(b;())
>) {}\mrightarrow{} Pos(sg-normalize(coW-game(a.\000CB[a];coW-item(w;t);coW-item(w';b))))
\mvdash{} sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))) \mcong{}
coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>
By
Latex:
((D 0 With \mkleeneopen{}\mlambda{}p.let u,v = p in <copath-cons(t;u), copath-cons(b;v)>\mkleeneclose{} THENA Auto)
THEN D 0 With \mkleeneopen{}\mlambda{}p.let u,v = p
in <copath-tl(u), copath-tl(v)>\mkleeneclose{}
THEN Auto)
Home
Index