Step
*
1
1
2
2
1
1
of Lemma
isom-preserves-win2
.....falsecase..... 
1. g1 : SimpleGame
2. g2 : SimpleGame
3. f : Pos(g1) ⟶ Pos(g2)
4. g : Pos(g2) ⟶ Pos(g1)
5. ∀x,y:Pos(g1).  (Legal1(x;y) 
⇒ Legal1(f x;f y))
6. ∀x,y:Pos(g1).  (Legal2(x;y) 
⇒ Legal2(f x;f y))
7. ∀x,y:Pos(g2).  (Legal1(x;y) 
⇒ Legal1(g x;g y))
8. ∀x,y:Pos(g2).  (Legal2(x;y) 
⇒ Legal2(g x;g y))
9. ∀x:Pos(g2). ((f (g x)) = x ∈ Pos(g2))
10. ∀x:Pos(g1). ((g (f x)) = x ∈ Pos(g1))
11. (f InitialPos(g1)) = InitialPos(g2) ∈ Pos(g2)
12. (g InitialPos(g2)) = InitialPos(g1) ∈ Pos(g1)
13. ∀[n:ℕ]. win2strat(g1;n)
14. n : ℤ
15. 0 < n
16. 2 ≤ (2 * n)
17. s : s:win2strat(g1;n - 1) ⋂ moves:{f:strat2play(g1;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g1)| Legal2(moves[(2 * \000Cn) - 1];p)} 
18. s ∈ win2strat(g1;n - 1)
19. s ∈ moves:{f:strat2play(g1;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g1)| Legal2(moves[(2 * n) - 1];p)} 
20. ¬(n = 0 ∈ ℤ)
21. (λmoves.(f (s g o moves)) ∈ win2strat(g2;n - 1))
∧ (∀moves:strat2play(g2;n - 1;λmoves.(f (s g o moves))). (g o moves ∈ strat2play(g1;n - 1;s)))
22. λmoves.(f (s g o moves)) ∈ win2strat(g2;n)
23. moves : f@0:strat2play(g2;n - 1;λmoves.(f (s g o moves))) ⋂ {moves:sequence(Pos(g2))| 
                                                                 (((2 * n) + 2) ≤ ||moves||)
                                                                 ∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
                                                                 ∧ (moves[2 * n]
                                                                   = ((λmoves.(f (s g o moves))) 
                                                                      play-truncate(f@0;2 * n))
                                                                   ∈ Pos(g2))} 
24. ¬(n = 0 ∈ ℤ)
25. ¬(n = 0 ∈ ℤ)
⊢ g o moves ∈ f:strat2play(g1;n - 1;s) ⋂ {moves:sequence(Pos(g1))| 
                                          (((2 * n) + 2) ≤ ||moves||)
                                          ∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
                                          ∧ (moves[2 * n] = (s play-truncate(f;2 * n)) ∈ Pos(g1))} 
BY
{ (DepIsectHD (-3) THEN (MemTypeHD (-3) THENA Auto) THEN Fold `member` (-4)) }
1
1. g1 : SimpleGame
2. g2 : SimpleGame
3. f : Pos(g1) ⟶ Pos(g2)
4. g : Pos(g2) ⟶ Pos(g1)
5. ∀x,y:Pos(g1).  (Legal1(x;y) 
⇒ Legal1(f x;f y))
6. ∀x,y:Pos(g1).  (Legal2(x;y) 
⇒ Legal2(f x;f y))
7. ∀x,y:Pos(g2).  (Legal1(x;y) 
⇒ Legal1(g x;g y))
8. ∀x,y:Pos(g2).  (Legal2(x;y) 
⇒ Legal2(g x;g y))
9. ∀x:Pos(g2). ((f (g x)) = x ∈ Pos(g2))
10. ∀x:Pos(g1). ((g (f x)) = x ∈ Pos(g1))
11. (f InitialPos(g1)) = InitialPos(g2) ∈ Pos(g2)
12. (g InitialPos(g2)) = InitialPos(g1) ∈ Pos(g1)
13. ∀[n:ℕ]. win2strat(g1;n)
14. n : ℤ
15. 0 < n
16. 2 ≤ (2 * n)
17. s : s:win2strat(g1;n - 1) ⋂ moves:{f:strat2play(g1;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g1)| Legal2(moves[(2 * \000Cn) - 1];p)} 
18. s ∈ win2strat(g1;n - 1)
19. s ∈ moves:{f:strat2play(g1;n - 1;s)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(g1)| Legal2(moves[(2 * n) - 1];p)} 
20. ¬(n = 0 ∈ ℤ)
21. (λmoves.(f (s g o moves)) ∈ win2strat(g2;n - 1))
∧ (∀moves:strat2play(g2;n - 1;λmoves.(f (s g o moves))). (g o moves ∈ strat2play(g1;n - 1;s)))
22. λmoves.(f (s g o moves)) ∈ win2strat(g2;n)
23. moves : f@0:strat2play(g2;n - 1;λmoves.(f (s g o moves))) ⋂ {moves:sequence(Pos(g2))| 
                                                                 (((2 * n) + 2) ≤ ||moves||)
                                                                 ∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
                                                                 ∧ (moves[2 * n]
                                                                   = ((λmoves.(f (s g o moves))) 
                                                                      play-truncate(f@0;2 * n))
                                                                   ∈ Pos(g2))} 
24. moves ∈ strat2play(g2;n - 1;λmoves.(f (s g o moves)))
25. moves ∈ sequence(Pos(g2))
26. (((2 * n) + 2) ≤ ||moves||)
∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
∧ (moves[2 * n] = ((λmoves.(f (s g o moves))) play-truncate(moves;2 * n)) ∈ Pos(g2))
27. ¬(n = 0 ∈ ℤ)
28. ¬(n = 0 ∈ ℤ)
⊢ g o moves ∈ f:strat2play(g1;n - 1;s) ⋂ {moves:sequence(Pos(g1))| 
                                          (((2 * n) + 2) ≤ ||moves||)
                                          ∧ Legal1(moves[2 * n];moves[(2 * n) + 1])
                                          ∧ (moves[2 * n] = (s play-truncate(f;2 * n)) ∈ Pos(g1))} 
Latex:
Latex:
.....falsecase..... 
1.  g1  :  SimpleGame
2.  g2  :  SimpleGame
3.  f  :  Pos(g1)  {}\mrightarrow{}  Pos(g2)
4.  g  :  Pos(g2)  {}\mrightarrow{}  Pos(g1)
5.  \mforall{}x,y:Pos(g1).    (Legal1(x;y)  {}\mRightarrow{}  Legal1(f  x;f  y))
6.  \mforall{}x,y:Pos(g1).    (Legal2(x;y)  {}\mRightarrow{}  Legal2(f  x;f  y))
7.  \mforall{}x,y:Pos(g2).    (Legal1(x;y)  {}\mRightarrow{}  Legal1(g  x;g  y))
8.  \mforall{}x,y:Pos(g2).    (Legal2(x;y)  {}\mRightarrow{}  Legal2(g  x;g  y))
9.  \mforall{}x:Pos(g2).  ((f  (g  x))  =  x)
10.  \mforall{}x:Pos(g1).  ((g  (f  x))  =  x)
11.  (f  InitialPos(g1))  =  InitialPos(g2)
12.  (g  InitialPos(g2))  =  InitialPos(g1)
13.  \mforall{}[n:\mBbbN{}].  win2strat(g1;n)
14.  n  :  \mBbbZ{}
15.  0  <  n
16.  2  \mleq{}  (2  *  n)
17.  s  :  s:win2strat(g1;n  -  1)  \mcap{}  moves:\{f:strat2play(g1;n  -  1;s)|  ||f||  =  (2  *  n)\}    {}\mrightarrow{}  \{p:Pos(g1)|  Le\000Cgal2(moves[(2  *  n)  -  1];p)\} 
18.  s  \mmember{}  win2strat(g1;n  -  1)
19.  s  \mmember{}  moves:\{f:strat2play(g1;n  -  1;s)|  ||f||  =  (2  *  n)\}    {}\mrightarrow{}  \{p:Pos(g1)|  Legal2(moves[(2  *  n)  -  1];\000Cp)\} 
20.  \mneg{}(n  =  0)
21.  (\mlambda{}moves.(f  (s  g  o  moves))  \mmember{}  win2strat(g2;n  -  1))
\mwedge{}  (\mforall{}moves:strat2play(g2;n  -  1;\mlambda{}moves.(f  (s  g  o  moves))).  (g  o  moves  \mmember{}  strat2play(g1;n  -  1;s)))
22.  \mlambda{}moves.(f  (s  g  o  moves))  \mmember{}  win2strat(g2;n)
23.  moves  :  f@0:strat2play(g2;n  -  1;\mlambda{}moves.(f  (s  g  o  moves)))  \mcap{}  \{moves:sequence(Pos(g2))| 
                                                                                                                                  (((2  *  n)  +  2)  \mleq{}  ||moves||)
                                                                                                                                  \mwedge{}  Legal1(moves[2  *  n];moves[(2  *  n)
                                                                                                                                                    +  1])
                                                                                                                                  \mwedge{}  (moves[2  *  n]
                                                                                                                                      =  ((\mlambda{}moves.(f  (s  g  o  moves))) 
                                                                                                                                            play-truncate(f@0;2  *  n)))\} 
24.  \mneg{}(n  =  0)
25.  \mneg{}(n  =  0)
\mvdash{}  g  o  moves  \mmember{}  f:strat2play(g1;n  -  1;s)  \mcap{}  \{moves:sequence(Pos(g1))| 
                                                                                    (((2  *  n)  +  2)  \mleq{}  ||moves||)
                                                                                    \mwedge{}  Legal1(moves[2  *  n];moves[(2  *  n)  +  1])
                                                                                    \mwedge{}  (moves[2  *  n]  =  (s  play-truncate(f;2  *  n)))\} 
By
Latex:
(DepIsectHD  (-3)  THEN  (MemTypeHD  (-3)  THENA  Auto)  THEN  Fold  `member`  (-4))
Home
Index