---

Step * 1 1 1 1 of Lemma isom-preserves-win2


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. s : Top
16. λmoves.(f (s g o moves)) ∈ Top
17. moves : {moves:sequence(Pos(g2))| 
             (2 ≤ ||moves||) ∧ (moves[0] = InitialPos(g2) ∈ Pos(g2)) ∧ Legal1(moves[0];moves[1])} 
⊢ g o moves ∈ {moves:sequence(Pos(g1))| 
               (2 ≤ ||moves||) ∧ (moves[0] = InitialPos(g1) ∈ Pos(g1)) ∧ Legal1(moves[0];moves[1])} 
BY
{ (D -1
   THEN MemTypeCD
   THEN Auto
   THEN (Unfold `play-item` 0 THEN Auto)
   THEN (RWO "seq-comp-item" 0 THENA Auto)
   THEN BackThruSomeHyp
   THEN Auto) }

---

Latex:

---

Latex:

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.  s  :  Top
16.  \mlambda{}moves.(f  (s  g  o  moves))  \mmember{}  Top
17.  moves  :  \{moves:sequence(Pos(g2))| 
                          (2  \mleq{}  ||moves||)  \mwedge{}  (moves[0]  =  InitialPos(g2))  \mwedge{}  Legal1(moves[0];moves[1])\} 
\mvdash{}  g  o  moves  \mmember{}  \{moves:sequence(Pos(g1))| 
                              (2  \mleq{}  ||moves||)  \mwedge{}  (moves[0]  =  InitialPos(g1))  \mwedge{}  Legal1(moves[0];moves[1])\} 


By

---

Latex:
(D  -1
  THEN  MemTypeCD
  THEN  Auto
  THEN  (Unfold  `play-item`  0  THEN  Auto)
  THEN  (RWO  "seq-comp-item"  0  THENA  Auto)
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index