---

Step * 2 1 of Lemma win2strat-strat2play-wf


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)))
BY
{ ((Assert win2strat(g;n) ∈ Type BY
          ((Unfold `win2strat` 0 THEN Unfold `play-len` 0)
           THEN AutoSplit
           THEN DepIsectWf
           THEN Try (Trivial)
           THEN MemCD
           THEN Try (Trivial)
           THEN D -2 With ⌜s⌝ 
           THEN Try (Trivial)
           THEN MemCD
           THEN Try ((D -1
                      THEN Unfold `play-item` 0
                      THEN Unfold `strat2play` -2
                      THEN (SplitOnHypITE -2  THENA Auto)
                      THEN (D -3 ORELSE (DepIsectHD (-3) THEN MemTypeHD (-3) THEN All (Fold `member`)))
                      THEN Auto))
           THEN Auto
           THEN Unfold `strat2play` -1
           THEN (SplitOnHypITE -1  THENA Auto)
           THEN ((DepIsectHD (-2) THEN (MemTypeHD (-2) THENA Auto) THEN All (Fold `member`) THEN Auto) ORELSE Auto)))
   THEN (MemCD THENL [Auto;Id⋅])
   ) }

1
.....subterm..... T:t
2:n
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))
8. win2strat(g;n) ∈ Type
⊢ <Ax, Ax, Ax> ∈ (∀[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:

1.  g  :  SimpleGame
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  win2strat(g;n  -  1)  \mmember{}  Type
5.  \mforall{}[s:win2strat(g;n  -  1)].  (strat2play(g;n  -  1;s)  \mmember{}  Type)
6.  \mforall{}[s:win2strat(g;n  -  1)].  \mforall{}[f:strat2play(g;n  -  1;s)].    (||f||  \mmember{}  \mBbbZ{})
7.  \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)  \mmember{}  Type  BY
                ((Unfold  `win2strat`  0  THEN  Unfold  `play-len`  0)
                  THEN  AutoSplit
                  THEN  DepIsectWf
                  THEN  Try  (Trivial)
                  THEN  MemCD
                  THEN  Try  (Trivial)
                  THEN  D  -2  With  \mkleeneopen{}s\mkleeneclose{} 
                  THEN  Try  (Trivial)
                  THEN  MemCD
                  THEN  Try  ((D  -1
                                        THEN  Unfold  `play-item`  0
                                        THEN  Unfold  `strat2play`  -2
                                        THEN  (SplitOnHypITE  -2    THENA  Auto)
                                        THEN  (D  -3
                                        ORELSE  (DepIsectHD  (-3)  THEN  MemTypeHD  (-3)  THEN  All  (Fold  `member`))
                                        )
                                        THEN  Auto))
                  THEN  Auto
                  THEN  Unfold  `strat2play`  -1
                  THEN  (SplitOnHypITE  -1    THENA  Auto)
                  THEN  ((DepIsectHD  (-2)  THEN  (MemTypeHD  (-2)  THENA  Auto)  THEN  All  (Fold  `member`)  THEN  Auto)
                  ORELSE  Auto
                  )))
  THEN  (MemCD  THENL  [Auto;Id\mcdot{}])
  )

---

Home Index