---

Step * 2 1 1 1 of Lemma WfdSpread-induction


1. Pos : Type
2. eq : EqDecider(Pos)
3. Mv : Pos ⟶ Type
4. n : ℤ
5. w : WfdSpread(Pos;a.Mv[a])@i
6. s : ℕ0 ⟶ MoveChoice(Pos;a.Mv[a])@i
7. a : Pos@i
8. f : Mv[a] ⟶ WfdSpread(Pos;a.Mv[a])@i
9. W_sel(w;0;s) = (inl mkW(a;f)) ∈ (WfdSpread(Pos;a.Mv[a])?)
10. m : Mv[a]@i
⊢ W_sel(w;0 + 1;s++λb.if eq b a then inl m else inr ⋅  fi ) = (inl (f m)) ∈ (WfdSpread(Pos;a.Mv[a])?)
BY
{ (Unfold `W_sel` (-2)
   THEN RecUnfold `subgame` (-2)
   THEN Reduce (-2)
   THEN Auto
   THEN HypSubst (-2) 0
   THEN Auto
   THEN Unfold `W_sel` 0
   THEN RepeatFor 2 ((RecUnfold `subgame` 0 THEN Reduce 0))
   THEN RepUR ``seq-adjoin seq-append`` 0
   THEN AutoSplit)⋅ }

---

Latex:

---

Latex:

1.  Pos  :  Type
2.  eq  :  EqDecider(Pos)
3.  Mv  :  Pos  {}\mrightarrow{}  Type
4.  n  :  \mBbbZ{}
5.  w  :  WfdSpread(Pos;a.Mv[a])@i
6.  s  :  \mBbbN{}0  {}\mrightarrow{}  MoveChoice(Pos;a.Mv[a])@i
7.  a  :  Pos@i
8.  f  :  Mv[a]  {}\mrightarrow{}  WfdSpread(Pos;a.Mv[a])@i
9.  W\_sel(w;0;s)  =  (inl  mkW(a;f))
10.  m  :  Mv[a]@i
\mvdash{}  W\_sel(w;0  +  1;s++\mlambda{}b.if  eq  b  a  then  inl  m  else  inr  \mcdot{}    fi  )  =  (inl  (f  m))


By

---

Latex:
(Unfold  `W\_sel`  (-2)
  THEN  RecUnfold  `subgame`  (-2)
  THEN  Reduce  (-2)
  THEN  Auto
  THEN  HypSubst  (-2)  0
  THEN  Auto
  THEN  Unfold  `W\_sel`  0
  THEN  RepeatFor  2  ((RecUnfold  `subgame`  0  THEN  Reduce  0))
  THEN  RepUR  ``seq-adjoin  seq-append``  0
  THEN  AutoSplit)\mcdot{}

---

Home Index