---

Step * of Lemma subgame_wf

∀[Pos:Type]. ∀[Mv:Pos ⟶ Type]. ∀[n:ℕ]. ∀[g:Spread(Pos;a.Mv[a])]. ∀[p:ℕn ⟶ MoveChoice(Pos;a.Mv[a])].
  (subgame(g;p;n) ∈ Spread(Pos;a.Mv[a])?)
BY
{ (InductionOnNat
   THEN Auto
   THEN RecUnfold `subgame` 0
   THEN AutoSplit
   THEN (InstLemma `spread-ext` [⌜Pos⌝;⌜Mv⌝]⋅ THEN Auto)
   THEN (GenConclAtAddrType ⌜a:Pos × (Mv[a] ⟶ Spread(Pos;a.Mv[a]))⌝ [2;1]⋅ THENM (D -2 THEN Reduce 0 THEN Auto))
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Pos:Type].  \mforall{}[Mv:Pos  {}\mrightarrow{}  Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[g:Spread(Pos;a.Mv[a])].
\mforall{}[p:\mBbbN{}n  {}\mrightarrow{}  MoveChoice(Pos;a.Mv[a])].
    (subgame(g;p;n)  \mmember{}  Spread(Pos;a.Mv[a])?)


By

---

Latex:
(InductionOnNat
  THEN  Auto
  THEN  RecUnfold  `subgame`  0
  THEN  AutoSplit
  THEN  (InstLemma  `spread-ext`  [\mkleeneopen{}Pos\mkleeneclose{};\mkleeneopen{}Mv\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (GenConclAtAddrType  \mkleeneopen{}a:Pos  \mtimes{}  (Mv[a]  {}\mrightarrow{}  Spread(Pos;a.Mv[a]))\mkleeneclose{}  [2;1]\mcdot{}
  THENM  (D  -2  THEN  Reduce  0  THEN  Auto)
  )
  THEN  Auto)

---

Home Index