Proof of Nuprl Lemma : sg-normalize-win2

Step * 1 2 1 1 1 1 2 of Lemma sg-normalize-win2

1. g : SimpleGame
2. n : ℕ
3. 0 < n
4. win2strat(g;n - 1) ≡ win2strat(sg-normalize(g);n - 1)

5. x : s:win2strat(sg-normalize(g);n - 1) ⋂ moves:{f:strat2play(sg-normalize(g);n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Po\000Cs(sg-normalize(g))|

                                                                        Legal2(moves[(2 * n) - 1];p)}

6. x ∈ win2strat(sg-normalize(g);n - 1)

7. x ∈ moves:{f:strat2play(sg-normalize(g);n - 1;x)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(sg-normalize(g))|

                                                                    Legal2(moves[(2 * n) - 1];p)}

8. ¬(n = 0 ∈ ℤ)
9. ¬(n = 0 ∈ ℤ)
10. moves : strat2play(g;n - 1;x)
11. ||moves|| = (2 * n) ∈ ℤ
12. x ∈ win2strat(g;n - 1)
13. moves ∈ {moves:sequence(Pos(g))| ((2 * (n - 1)) + 2) ≤ ||moves||}
14. sequence(Pos(sg-normalize(g))) ⊆r sequence(Pos(g))
15. (moves[0] = InitialPos(g) ∈ Pos(g))
∧ (∀i:ℕ(n - 1) + 1
     ((↓Legal1(moves[2 * i];moves[(2 * i) + 1]))
     ∧ (i < n - 1
       ⇒ ((↓Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)]))
          ∧ (moves[2 * (i + 1)] = (x play-truncate(moves;2 * (i + 1))) ∈ Pos(g))))))
16. moves ∈ sequence(Pos(sg-normalize(g)))
⊢ moves ∈ strat2play(sg-normalize(g);n - 1;x)
BY
{ (D -2
   THEN DupHyp (-2)
   THEN (D -1 With ⌜0⌝  THENA Auto)
   THEN D -1
   THEN Thin (-1)
   THEN D -1
   THEN RepUR ``play-item`` -1
   THEN Strat2PlayWf
   THEN Try (Trivial)) }

1
.....set predicate.....
1. g : SimpleGame
2. n : ℕ
3. 0 < n
4. win2strat(g;n - 1) ≡ win2strat(sg-normalize(g);n - 1)

5. x : s:win2strat(sg-normalize(g);n - 1) ⋂ moves:{f:strat2play(sg-normalize(g);n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Po\000Cs(sg-normalize(g))|

                                                                        Legal2(moves[(2 * n) - 1];p)}

6. x ∈ win2strat(sg-normalize(g);n - 1)

7. x ∈ moves:{f:strat2play(sg-normalize(g);n - 1;x)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(sg-normalize(g))|

                                                                    Legal2(moves[(2 * n) - 1];p)}

⊢ (2 ≤ ||moves||) ∧ (moves[0] = InitialPos(sg-normalize(g)) ∈ Pos(sg-normalize(g))) ∧ Legal1(moves[0];moves[1])

2
1. g : SimpleGame
2. n : ℕ
3. 0 < n
4. win2strat(g;n - 1) ≡ win2strat(sg-normalize(g);n - 1)

5. x : s:win2strat(sg-normalize(g);n - 1) ⋂ moves:{f:strat2play(sg-normalize(g);n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Po\000Cs(sg-normalize(g))|

                                                                        Legal2(moves[(2 * n) - 1];p)}

6. x ∈ win2strat(sg-normalize(g);n - 1)

7. x ∈ moves:{f:strat2play(sg-normalize(g);n - 1;x)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(sg-normalize(g))|

                                                                    Legal2(moves[(2 * n) - 1];p)}

8. ¬(n = 0 ∈ ℤ)
9. ¬(n = 0 ∈ ℤ)
10. moves : strat2play(g;n - 1;x)
11. ||moves|| = (2 * n) ∈ ℤ
12. x ∈ win2strat(g;n - 1)
13. moves ∈ {moves:sequence(Pos(g))| ((2 * (n - 1)) + 2) ≤ ||moves||}
14. sequence(Pos(sg-normalize(g))) ⊆r sequence(Pos(g))
15. moves[0] = InitialPos(g) ∈ Pos(g)
16. ∀i:ℕ(n - 1) + 1
      ((↓Legal1(moves[2 * i];moves[(2 * i) + 1]))
      ∧ (i < n - 1
        ⇒ ((↓Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)]))
           ∧ (moves[2 * (i + 1)] = (x play-truncate(moves;2 * (i + 1))) ∈ Pos(g)))))
17. moves ∈ sequence(Pos(sg-normalize(g)))
18. Legal1(moves[0];moves[1])
19. k : ℤ
20. 0 < k
21. k ≤ (n - 1)
22. ¬(k = 0 ∈ ℤ)
23. moves ∈ strat2play(sg-normalize(g);k - 1;x)
⊢ moves ∈ {moves@0:sequence(Pos(sg-normalize(g)))|
           (((2 * k) + 2) ≤ ||moves@0||)
           ∧ Legal1(moves@0[2 * k];moves@0[(2 * k) + 1])
           ∧ (moves@0[2 * k] = (x play-truncate(moves;2 * k)) ∈ Pos(sg-normalize(g)))}

Latex:

Latex:
1. g : SimpleGame 2. n : \mBbbN{} 3. 0 < n 4. win2strat(g;n - 1) \mequiv{} win2strat(sg-normalize(g);n - 1) 5. x : s:win2strat(sg-normalize(g);n - 1) \mcap{} moves:\{f:strat2play(sg-normalize(g);n - 1;s)| ||f|| = (2 * n)\} {}\mrightarrow{} \{p:Pos(sg-normalize(g))| Leg\000Cal2(moves[(2 * n) - 1];p)\} 6. x \mmember{} win2strat(sg-normalize(g);n - 1) 7. x \mmember{} moves:\{f:strat2play(sg-normalize(g);n - 1;x)| ||f|| = (2 * n)\} {}\mrightarrow{} \{p:Pos(sg-normalize(g))| Legal2(moves[(2 * n) - 1];p)\} 8. \mneg{}(n = 0) 9. \mneg{}(n = 0) 10. moves : strat2play(g;n - 1;x) 11. ||moves|| = (2 * n) 12. x \mmember{} win2strat(g;n - 1) 13. moves \mmember{} \{moves:sequence(Pos(g))| ((2 * (n - 1)) + 2) \mleq{} ||moves||\} 14. sequence(Pos(sg-normalize(g))) \msubseteq{}r sequence(Pos(g)) 15. (moves[0] = InitialPos(g)) \mwedge{} (\mforall{}i:\mBbbN{}(n - 1) + 1 ((\mdownarrow{}Legal1(moves[2 * i];moves[(2 * i) + 1])) \mwedge{} (i < n - 1 {}\mRightarrow{} ((\mdownarrow{}Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)])) \mwedge{} (moves[2 * (i + 1)] = (x play-truncate(moves;2 * (i + 1)))))))) 16. moves \mmember{} sequence(Pos(sg-normalize(g))) \mvdash{} moves \mmember{} strat2play(sg-normalize(g);n - 1;x) By Latex: (D -2 THEN DupHyp (-2) THEN (D -1 With \mkleeneopen{}0\mkleeneclose{} THENA Auto) THEN D -1 THEN Thin (-1) THEN D -1 THEN RepUR ``play-item`` -1 THEN Strat2PlayWf THEN Try (Trivial)) Home Index