---

Step * of Lemma respond-implies-win2

∀g:SimpleGame. ((∀p:{p:Pos(g)| Legal1(InitialPos(g);p)} . ∃q:{q:Pos(g)| Legal2(p;q)} . win2(g@q)) ⇒ win2(g))
BY
{ (Auto
   THEN (Skolemize (-1) `m' THENA Auto)
   THEN Thin (-3)
   THEN All (Unfold `win2`)
   THEN (D 0 THENA Auto)
   THEN RenameVar `s' (-2)
   THEN UseWitness ⌜λmoves.if (||moves|| =z 2) then m moves[1] else s moves[1] seq-tl(seq-tl(moves)) fi ⌝⋅
   THEN NatInd (-1)
   THEN Unfold `win2strat` 0
   THEN (SplitOnConclITE THENA Auto)
   THEN Try (Trivial)
   THEN Try ((D -1 THEN Fold `member` 0 THEN Auto))
   THEN DepIsectCD
   THEN Try (Trivial)
   THEN (MemCD THENA Auto)) }

1
.....subterm..... T:t
1:n
1. g : SimpleGame
2. m : p:{p:Pos(g)| Legal1(InitialPos(g);p)}  ⟶ {q:Pos(g)| Legal2(p;q)} 
3. s : ∀p:{p:Pos(g)| Legal1(InitialPos(g);p)} . ∀[n:ℕ]. win2strat(g@m p;n)
4. n : ℤ
5. 0 < n
6. λmoves.if (||moves|| =z 2) then m moves[1] else s moves[1] seq-tl(seq-tl(moves)) fi  ∈ win2strat(g;n - 1)
7. ¬(n = 0 ∈ ℤ)
8. moves : {f:strat2play(g;n - 1;λmoves.if (||moves|| =z 2) then m moves[1] else s moves[1] seq-tl(seq-tl(moves)) fi )| 
            ||f|| = (2 * n) ∈ ℤ} 
⊢ if (||moves|| =z 2) then m moves[1] else s moves[1] seq-tl(seq-tl(moves)) fi  ∈ {p:Pos(g)| 
                                                                                   Legal2(moves[(2 * n) - 1];p)} 

---

Latex:

---

Latex:
\mforall{}g:SimpleGame
    ((\mforall{}p:\{p:Pos(g)|  Legal1(InitialPos(g);p)\}  .  \mexists{}q:\{q:Pos(g)|  Legal2(p;q)\}  .  win2(g@q))  {}\mRightarrow{}  win2(g))


By

---

Latex:
(Auto
  THEN  (Skolemize  (-1)  `m'  THENA  Auto)
  THEN  Thin  (-3)
  THEN  All  (Unfold  `win2`)
  THEN  (D  0  THENA  Auto)
  THEN  RenameVar  `s'  (-2)
  THEN  UseWitness  \mkleeneopen{}\mlambda{}moves.if  (||moves||  =\msubz{}  2)
                                                  then  m  moves[1]
                                                  else  s  moves[1]  seq-tl(seq-tl(moves))
                                                  fi  \mkleeneclose{}\mcdot{}
  THEN  NatInd  (-1)
  THEN  Unfold  `win2strat`  0
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Try  (Trivial)
  THEN  Try  ((D  -1  THEN  Fold  `member`  0  THEN  Auto))
  THEN  DepIsectCD
  THEN  Try  (Trivial)
  THEN  (MemCD  THENA  Auto))

---

Home Index