---

Step * 1 of Lemma strat2play_subtype_le


1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. ∀[s:win2strat(g;n - 1)]. ∀[j:ℕ(n - 1) + 1].  (strat2play(g;n - 1;s) ⊆r strat2play(g;j;s))
5. s : win2strat(g;n)
6. j : ℕn + 1
7. j < n
⊢ strat2play(g;n;s) ⊆r strat2play(g;n - 1;s)
BY
{ ((D 0 THENA Auto)
   THEN Unfold `strat2play` -1
   THEN (SplitOnHypITE -1  THENA Auto)
   THEN ((DepIsectHD (-2) THEN Trivial) ORELSE Auto)) }

---

Latex:

---

Latex:

1.  g  :  SimpleGame
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  \mforall{}[s:win2strat(g;n  -  1)].  \mforall{}[j:\mBbbN{}(n  -  1)  +  1].    (strat2play(g;n  -  1;s)  \msubseteq{}r  strat2play(g;j;s))
5.  s  :  win2strat(g;n)
6.  j  :  \mBbbN{}n  +  1
7.  j  <  n
\mvdash{}  strat2play(g;n;s)  \msubseteq{}r  strat2play(g;n  -  1;s)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  Unfold  `strat2play`  -1
  THEN  (SplitOnHypITE  -1    THENA  Auto)
  THEN  ((DepIsectHD  (-2)  THEN  Trivial)  ORELSE  Auto))

---

Home Index