---

Step * 2 of Lemma win2strat-strat2play-wf

.....upcase..... 
1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. <Ax, Ax, Ax, Ax> ∈ (win2strat(g;n - 1) ∈ Type)
   ∧ (∀[s:win2strat(g;n - 1)]. (strat2play(g;n - 1;s) ∈ Type))
   ∧ (∀[s:win2strat(g;n - 1)]. ∀[f:strat2play(g;n - 1;s)].  (||f|| ∈ ℤ))
   ∧ (∀[s:win2strat(g;n - 1)]. ∀[f:strat2play(g;n - 1;s)]. ∀[k:{(2 * (n - 1)) + 2..||f|| + 1-}].
        (seq-truncate(f;k) ∈ strat2play(g;n - 1;s)))
⊢ <Ax, Ax, Ax, Ax> ∈ (win2strat(g;n) ∈ Type)
  ∧ (∀[s:win2strat(g;n)]. (strat2play(g;n;s) ∈ Type))
  ∧ (∀[s:win2strat(g;n)]. ∀[f:strat2play(g;n;s)].  (||f|| ∈ ℤ))
  ∧ (∀[s:win2strat(g;n)]. ∀[f:strat2play(g;n;s)]. ∀[k:{(2 * n) + 2..||f|| + 1-}].
       (seq-truncate(f;k) ∈ strat2play(g;n;s)))
BY
{ ((Assert win2strat(g;n - 1) ∈ Type BY
          ((MemHD (-1) THENA Auto) THEN All Reduce THEN UseWitness ⌜Ax⌝⋅ THEN Auto))
   THEN (Assert ∀[s:win2strat(g;n - 1)]. (strat2play(g;n - 1;s) ∈ Type) BY
               (RepeatFor 2 (((MemHD (-2) THENA Auto) THEN All Reduce)) THEN UseWitness ⌜Ax⌝⋅ THEN Auto))
   THEN (Assert ∀[s:win2strat(g;n - 1)]. ∀[f:strat2play(g;n - 1;s)].  (||f|| ∈ ℤ) BY
               (RepeatFor 3 (((MemHD (-3) THENA Auto) THEN All Reduce)) THEN UseWitness ⌜Ax⌝⋅ THEN Auto))
   THEN (Assert ∀[s:win2strat(g;n - 1)]. ∀[f:strat2play(g;n - 1;s)]. ∀[k:{(2 * (n - 1)) + 2..||f|| + 1-}].
                  (seq-truncate(f;k) ∈ strat2play(g;n - 1;s)) BY
               (RepeatFor 3 (((MemHD (-4) THENA Auto) THEN All Reduce)) THEN UseWitness ⌜Ax⌝⋅ THEN Auto))
   THEN Thin 4) }

1
1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. win2strat(g;n - 1) ∈ Type
5. ∀[s:win2strat(g;n - 1)]. (strat2play(g;n - 1;s) ∈ Type)
6. ∀[s:win2strat(g;n - 1)]. ∀[f:strat2play(g;n - 1;s)].  (||f|| ∈ ℤ)
7. ∀[s:win2strat(g;n - 1)]. ∀[f:strat2play(g;n - 1;s)]. ∀[k:{(2 * (n - 1)) + 2..||f|| + 1-}].
     (seq-truncate(f;k) ∈ strat2play(g;n - 1;s))
⊢ <Ax, Ax, Ax, Ax> ∈ (win2strat(g;n) ∈ Type)
  ∧ (∀[s:win2strat(g;n)]. (strat2play(g;n;s) ∈ Type))
  ∧ (∀[s:win2strat(g;n)]. ∀[f:strat2play(g;n;s)].  (||f|| ∈ ℤ))
  ∧ (∀[s:win2strat(g;n)]. ∀[f:strat2play(g;n;s)]. ∀[k:{(2 * n) + 2..||f|| + 1-}].
       (seq-truncate(f;k) ∈ strat2play(g;n;s)))

---

Latex:

---

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


By

---

Latex:
((Assert  win2strat(g;n  -  1)  \mmember{}  Type  BY
                ((MemHD  (-1)  THENA  Auto)  THEN  All  Reduce  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  \mforall{}[s:win2strat(g;n  -  1)].  (strat2play(g;n  -  1;s)  \mmember{}  Type)  BY
                          (RepeatFor  2  (((MemHD  (-2)  THENA  Auto)  THEN  All  Reduce))
                            THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
                            THEN  Auto))
  THEN  (Assert  \mforall{}[s:win2strat(g;n  -  1)].  \mforall{}[f:strat2play(g;n  -  1;s)].    (||f||  \mmember{}  \mBbbZ{})  BY
                          (RepeatFor  3  (((MemHD  (-3)  THENA  Auto)  THEN  All  Reduce))
                            THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
                            THEN  Auto))
  THEN  (Assert  \mforall{}[s:win2strat(g;n  -  1)].  \mforall{}[f:strat2play(g;n  -  1;s)].
                            \mforall{}[k:\{(2  *  (n  -  1))  +  2..||f||  +  1\msupminus{}\}].
                                (seq-truncate(f;k)  \mmember{}  strat2play(g;n  -  1;s))  BY
                          (RepeatFor  3  (((MemHD  (-4)  THENA  Auto)  THEN  All  Reduce))
                            THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
                            THEN  Auto))
  THEN  Thin  4)

---

Home Index