---

Step * 1 1 of Lemma win2strat-strat2play-wf


1. g : SimpleGame
2. n : ℤ
3. win2strat(g;0) ∈ Type
4. ∀[s:win2strat(g;0)]. (strat2play(g;0;s) ∈ Type)
⊢ <Ax, Ax, Ax, Ax> ∈ (win2strat(g;0) ∈ Type)
  ∧ (∀[s:win2strat(g;0)]. (strat2play(g;0;s) ∈ Type))
  ∧ (∀[s:win2strat(g;0)]. ∀[f:strat2play(g;0;s)].  (||f|| ∈ ℤ))
  ∧ (∀[s:win2strat(g;0)]. ∀[f:strat2play(g;0;s)]. ∀[k:{(2 * 0) + 2..||f|| + 1-}].
       (seq-truncate(f;k) ∈ strat2play(g;0;s)))
BY
{ ((Assert ∀[s:win2strat(g;0)]. ∀[f:strat2play(g;0;s)].  (||f|| ∈ ℤ) BY
          (ParallelLast THEN Unfold `strat2play` 0 THEN Reduce 0 THEN RepUR ``play-item`` 0 THEN Auto))
   THEN (Assert ∀[s:win2strat(g;0)]. ∀[f:strat2play(g;0;s)]. ∀[k:{(2 * 0) + 2..||f|| + 1-}].
                  (seq-truncate(f;k) ∈ strat2play(g;0;s)) BY
               (ParallelOp -2
                THEN (D -3 With ⌜s⌝  THENA Auto)
                THEN Unfold `strat2play` 0
                THEN Reduce 0
                THEN Unfold `play-item` 0
                THEN Auto
                THEN D -2
                THEN MemTypeCD
                THEN RWW "seq-len-truncate seq-truncate-item" 0
                THEN Auto))
   THEN (MemCD THENL [Auto; MemCD⋅] THENL [Auto; MemCD⋅])
   THEN (Unfold `uall` 0 THEN MemTypeCD THEN Try (Trivial))
   THEN D -4 With ⌜s⌝ 
   THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  SimpleGame
2.  n  :  \mBbbZ{}
3.  win2strat(g;0)  \mmember{}  Type
4.  \mforall{}[s:win2strat(g;0)].  (strat2play(g;0;s)  \mmember{}  Type)
\mvdash{}  <Ax,  Ax,  Ax,  Ax>  \mmember{}  (win2strat(g;0)  \mmember{}  Type)
    \mwedge{}  (\mforall{}[s:win2strat(g;0)].  (strat2play(g;0;s)  \mmember{}  Type))
    \mwedge{}  (\mforall{}[s:win2strat(g;0)].  \mforall{}[f:strat2play(g;0;s)].    (||f||  \mmember{}  \mBbbZ{}))
    \mwedge{}  (\mforall{}[s:win2strat(g;0)].  \mforall{}[f:strat2play(g;0;s)].  \mforall{}[k:\{(2  *  0)  +  2..||f||  +  1\msupminus{}\}].
              (seq-truncate(f;k)  \mmember{}  strat2play(g;0;s)))


By

---

Latex:
(...
  THEN  (Assert  \mforall{}[s:win2strat(g;0)].  \mforall{}[f:strat2play(g;0;s)].  \mforall{}[k:\{(2  *  0)  +  2..||f||  +  1\msupminus{}\}].
                                (seq-truncate(f;k)  \mmember{}  strat2play(g;0;s))  BY
                          (ParallelOp  -2
                            THEN  (D  -3  With  \mkleeneopen{}s\mkleeneclose{}    THENA  Auto)
                            THEN  Unfold  `strat2play`  0
                            THEN  Reduce  0
                            THEN  Unfold  `play-item`  0
                            THEN  Auto
                            THEN  D  -2
                            THEN  MemTypeCD
                            THEN  RWW  "seq-len-truncate  seq-truncate-item"  0
                            THEN  Auto))
  THEN  (MemCD  THENL  [Auto;  MemCD\mcdot{}]  THENL  [Auto;  MemCD\mcdot{}])
  THEN  (Unfold  `uall`  0  THEN  MemTypeCD  THEN  Try  (Trivial))
  THEN  D  -4  With  \mkleeneopen{}s\mkleeneclose{} 
  THEN  Auto)

---

Home Index