---

Step * of Lemma win2strat_subtype

∀[g:SimpleGame]. ∀[n,m:ℕ].  win2strat(g;n) ⊆r win2strat(g;m) supposing m ≤ n
BY
{ ((InductionOnNat THEN Auto) THEN (Decide ⌜m < n⌝⋅ THENA Auto)) }

1
1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. ∀[m:ℕ]. win2strat(g;n - 1) ⊆r win2strat(g;m) supposing m ≤ (n - 1)
5. m : ℕ
6. m ≤ n
7. m < n
⊢ win2strat(g;n) ⊆r win2strat(g;m)

2
1. g : SimpleGame
2. n : ℤ
3. 0 < n
4. ∀[m:ℕ]. win2strat(g;n - 1) ⊆r win2strat(g;m) supposing m ≤ (n - 1)
5. m : ℕ
6. m ≤ n
7. ¬m < n
⊢ win2strat(g;n) ⊆r win2strat(g;m)

---

Latex:

---

Latex:
\mforall{}[g:SimpleGame].  \mforall{}[n,m:\mBbbN{}].    win2strat(g;n)  \msubseteq{}r  win2strat(g;m)  supposing  m  \mleq{}  n


By

---

Latex:
((InductionOnNat  THEN  Auto)  THEN  (Decide  \mkleeneopen{}m  <  n\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index