---

Step * of Lemma strat2play_subtype_le

∀[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n)]. ∀[j:ℕn + 1].  (strat2play(g;n;s) ⊆r strat2play(g;j;s))
BY
{ ((InductionOnNat THEN Auto)
   THEN (Decide ⌜j < n⌝⋅ THEN Auto)
   THEN Using [`B',⌜strat2play(g;n - 1;s)⌝] (BLemma `subtype_rel_transitivity`)⋅
   THEN Auto) }

1
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)

---

Latex:

---

Latex:
\mforall{}[g:SimpleGame].  \mforall{}[n:\mBbbN{}].  \mforall{}[s:win2strat(g;n)].  \mforall{}[j:\mBbbN{}n  +  1].    (strat2play(g;n;s)  \msubseteq{}r  strat2play(g;j;s))


By

---

Latex:
((InductionOnNat  THEN  Auto)
  THEN  (Decide  \mkleeneopen{}j  <  n\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  Using  [`B',\mkleeneopen{}strat2play(g;n  -  1;s)\mkleeneclose{}]  (BLemma  `subtype\_rel\_transitivity`)\mcdot{}
  THEN  Auto)

---

Home Index