Proof of Nuprl Lemma : coW-trans

Step * 1 1 1 2 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 : 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)}
BY
{ (RepUR ``let`` 0

   THEN (Assert seq-add(seq-add(seq-nil();<(), ()>);<(), z>) ∈ {f:strat2play(coW-game(a.B[a];w2;w3);0;Y)| ||f|| = 2 ∈ ℤ}\000C  BY

               ((Unfold `strat2play` 0 THEN RepUR ``play-len play-item`` 0)
                THEN (MemTypeCD THENA Auto)
                THEN (MemTypeCD THENW Auto)
                THEN SplitAndConcl
                THEN Computation
                THEN Auto

                THEN ((EqCD THEN Auto) ORELSE (RepUR ``sg-legal1 coW-game`` 0 THEN OrRight THEN Auto))))

) }

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)}

27. seq-add(seq-add(seq-nil();<(), ()>);<(), z>) ∈ {f:strat2play(coW-game(a.B[a];w2;w3);0;Y)| ||f|| = 2 ∈ ℤ}

⊢ <seq-add(seq-add(seq-nil();<(), ()>);<(), fst((Y seq-add(seq-add(seq-nil();<(), ()>);<(), z>)))>), seq-add(seq-add(seq\000C-nil();<(), ()>);<(), z>)> ∈ {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 : 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> 24. m1[0] = InitialPos(coW-game(a.B[a];w1;w3)) 25. copath-length(z) = 1 26. copathAgree(a.B[a];w3;();z) \mvdash{} let M2 = seq-add(seq-add(seq-nil();<(), ()>);<(), z>) in let M1 = seq-add(seq-add(seq-nil();<(), ()>);<(), fst((Y M2))>) in <M1, M2> \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: (RepUR ``let`` 0 THEN (Assert seq-add(seq-add(seq-nil();<(), ()>);<(), z>) \mmember{} \{f:strat2play(coW-game(a.B[a];w2;w3);0;\000CY)| ||f|| = 2\} BY ((Unfold `strat2play` 0 THEN RepUR ``play-len play-item`` 0) THEN (MemTypeCD THENA Auto) THEN (MemTypeCD THENW Auto) THEN SplitAndConcl THEN Computation THEN Auto THEN ((EqCD THEN Auto) ORELSE (RepUR ``sg-legal1 coW-game`` 0 THEN OrRight THEN Auto) ))) ) Home Index