---

Step * of Lemma isom-preserves-win2

∀g1,g2:SimpleGame.  (g1 ≅ g2 ⇒ win2(g1) ⇒ win2(g2))
BY
{ (Auto
   THEN RepeatFor 2 (ParallelLast)
   THEN RenameVar `s' (-1)
   THEN D 3
   THEN ExRepD
   THEN UseWitness ⌜λmoves.(f (s g o moves))⌝⋅) }

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. s : win2strat(g1;n)
⊢ λmoves.(f (s g o moves)) ∈ win2strat(g2;n)

---

Latex:

---

Latex:
\mforall{}g1,g2:SimpleGame.    (g1  \mcong{}  g2  {}\mRightarrow{}  win2(g1)  {}\mRightarrow{}  win2(g2))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (ParallelLast)
  THEN  RenameVar  `s'  (-1)
  THEN  D  3
  THEN  ExRepD
  THEN  UseWitness  \mkleeneopen{}\mlambda{}moves.(f  (s  g  o  moves))\mkleeneclose{}\mcdot{})

---

Home Index