Proof of Nuprl Lemma : coW-game-step-isom

Step * 2 1 2 7 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))))

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))))
BY
{ (Symmetry
   THEN (RWO "sg-pos-normalize" (-1) THENA Auto)
   THEN D -1
   THEN (RWO "sg-pos-normalize" 0 THENA Auto)
   THEN EqTypeCD
   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,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(coW-game(a.B[a];coW-item(w;t);coW-item(w';b)))
16. sg-reachable(coW-game(a.B[a];coW-item(w;t);coW-item(w';b));InitialPos(coW-game(a.B[a];coW-item(w;t);...));x)
⊢ x

= ((λ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))

∈ Pos(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)))) 10. \mforall{}x,y:Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b)))). (Legal1(x;y) {}\mRightarrow{} Legal1((\mlambda{}p.let u,v = p in <copath-cons(t;u), copath-cons(b;v)>) x;(\mlambda{}p.let u,v = p in <copath-cons(t;u) , copath-cons(b;v) >) y)) 11. \mforall{}x,y:Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b)))). (Legal2(x;y) {}\mRightarrow{} Legal2((\mlambda{}p.let u,v = p in <copath-cons(t;u), copath-cons(b;v)>) x;(\mlambda{}p.let u,v = p in <copath-cons(t;u) , copath-cons(b;v) >) y)) 12. \mforall{}x,y:Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>). (Legal1(x;y) {}\mRightarrow{} Legal1((\mlambda{}p.let u,v = p in <copath-tl(u), copath-tl(v)>) x;(\mlambda{}p.let u,v = p in <copath-tl(u) , copath-tl(v) >) y)) 13. \mforall{}x,y:Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>). (Legal2(x;y) {}\mRightarrow{} Legal2((\mlambda{}p.let u,v = p in <copath-tl(u), copath-tl(v)>) x;(\mlambda{}p.let u,v = p in <copath-tl(u) , copath-tl(v) >) y)) 14. \mforall{}x:Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>) (((\mlambda{}p.let u,v = p in <copath-cons(t;u), copath-cons(b;v)>) ((\mlambda{}p.let u,v = p in <copath-tl(u), copath-tl(v)>) x)) = x) 15. x : Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b)))) \mvdash{} ((\mlambda{}p.let u,v = p in <copath-tl(u), copath-tl(v)>) ((\mlambda{}p.let u,v = p in <copath-cons(t;u), copath-cons(b;v)>) x)) = x By Latex: (Symmetry THEN (RWO "sg-pos-normalize" (-1) THENA Auto) THEN D -1 THEN (RWO "sg-pos-normalize" 0 THENA Auto) THEN EqTypeCD THEN Auto) Home Index