---

Step * of Lemma W_sel_wf

∀[Pos:Type]
  ∀[Mv:Pos ⟶ Type]. ∀[n:ℕ]. ∀[w:WfdSpread(Pos;a.Mv[a])]. ∀[s:ℕn ⟶ MoveChoice(Pos;a.Mv[a])].
    (W_sel(w;n;s) ∈ WfdSpread(Pos;a.Mv[a])?) 
  supposing ∀x,y:Pos.  Dec(x = y ∈ Pos)
BY
{ ((InductionOnNat THEN Auto)
   THEN (InstLemma `WfdSpread-ext` [⌜Pos⌝;⌜Mv⌝]⋅ THENA Auto)
   THEN (GenConcl ⌜w = z ∈ (a:Pos × (Mv[a] ⟶ WfdSpread(Pos;a.Mv[a])))⌝⋅ THENA Auto)
   THEN ThinVar `w'
   THEN D -1
   THEN Unfold `W_sel` 0
   THEN RecUnfold `subgame` 0
   THEN Reduce 0
   THEN Fold `mkW` 0
   THEN AutoSplit
   THEN Fold `shift-play` 0
   THEN (GenConclAtAddr [2;1] THEN D -2 THEN Reduce 0)
   THEN Auto
   THEN Fold `W_sel` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Pos:Type]
    \mforall{}[Mv:Pos  {}\mrightarrow{}  Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[w:WfdSpread(Pos;a.Mv[a])].  \mforall{}[s:\mBbbN{}n  {}\mrightarrow{}  MoveChoice(Pos;a.Mv[a])].
        (W\_sel(w;n;s)  \mmember{}  WfdSpread(Pos;a.Mv[a])?) 
    supposing  \mforall{}x,y:Pos.    Dec(x  =  y)


By

---

Latex:
((InductionOnNat  THEN  Auto)
  THEN  (InstLemma  `WfdSpread-ext`  [\mkleeneopen{}Pos\mkleeneclose{};\mkleeneopen{}Mv\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}w  =  z\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `w'
  THEN  D  -1
  THEN  Unfold  `W\_sel`  0
  THEN  RecUnfold  `subgame`  0
  THEN  Reduce  0
  THEN  Fold  `mkW`  0
  THEN  AutoSplit
  THEN  Fold  `shift-play`  0
  THEN  (GenConclAtAddr  [2;1]  THEN  D  -2  THEN  Reduce  0)
  THEN  Auto
  THEN  Fold  `W\_sel`  0
  THEN  Auto)

---

Home Index