---

Step * 2 1 1 of Lemma WfdSpread-induction


1. Pos : Type
2. eq : EqDecider(Pos)
3. ∀a,b:Pos.  Dec(a = b ∈ Pos)
4. Mv : Pos ⟶ Type
5. P : WfdSpread(Pos;a.Mv[a]) ⟶ ℙ
6. ∀a:Pos. ∀f:Mv[a] ⟶ WfdSpread(Pos;a.Mv[a]).  ((∀m:Mv[a]. P[f m]) ⇒ P[mkW(a;f)])
7. w : WfdSpread(Pos;a.Mv[a])@i
8. n : ℕ@i
9. s : ℕn ⟶ MoveChoice(Pos;a.Mv[a])@i
10. ∀t:MoveChoice(Pos;a.Mv[a]). case W_sel(w;n + 1;s++t) of inl(w) => P[w] | inr(z) => True
11. WfdSpread(Pos;a.Mv[a]) ≡ a:Pos × (Mv[a] ⟶ WfdSpread(Pos;a.Mv[a]))
12. a : Pos@i
13. f : Mv[a] ⟶ WfdSpread(Pos;a.Mv[a])@i
14. W_sel(w;n;s) = (inl mkW(a;f)) ∈ (WfdSpread(Pos;a.Mv[a])?)
15. m : Mv[a]@i
⊢ W_sel(w;n + 1;s++λb.if eq b a then inl m else inr ⋅  fi ) = (inl (f m)) ∈ (WfdSpread(Pos;a.Mv[a])?)
BY
{ (RepeatFor 2 (MoveToConcl (-1))
   THEN All Thin
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN MoveToConcl (-2)
   THEN NatInd (-1)
   THEN Auto) }

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

2
1. Pos : Type
2. eq : EqDecider(Pos)
3. Mv : Pos ⟶ Type
4. n : ℤ
5. 0 < n
6. ∀w:WfdSpread(Pos;a.Mv[a]). ∀s:ℕn - 1 ⟶ MoveChoice(Pos;a.Mv[a]). ∀a:Pos. ∀f:Mv[a] ⟶ WfdSpread(Pos;a.Mv[a]).
     ((W_sel(w;n - 1;s) = (inl mkW(a;f)) ∈ (WfdSpread(Pos;a.Mv[a])?))
     ⇒ (∀m:Mv[a]
           (W_sel(w;(n - 1) + 1;s++λb.if eq b a then inl m else inr ⋅  fi ) = (inl (f m)) ∈ (WfdSpread(Pos;a.Mv[a])?))))
7. w : WfdSpread(Pos;a.Mv[a])@i
8. s : ℕn ⟶ MoveChoice(Pos;a.Mv[a])@i
9. a : Pos@i
10. f : Mv[a] ⟶ WfdSpread(Pos;a.Mv[a])@i
11. W_sel(w;n;s) = (inl mkW(a;f)) ∈ (WfdSpread(Pos;a.Mv[a])?)
12. m : Mv[a]@i
⊢ W_sel(w;n + 1;s++λb.if eq b a then inl m else inr ⋅  fi ) = (inl (f m)) ∈ (WfdSpread(Pos;a.Mv[a])?)

---

Latex:

---

Latex:

1.  Pos  :  Type
2.  eq  :  EqDecider(Pos)
3.  \mforall{}a,b:Pos.    Dec(a  =  b)
4.  Mv  :  Pos  {}\mrightarrow{}  Type
5.  P  :  WfdSpread(Pos;a.Mv[a])  {}\mrightarrow{}  \mBbbP{}
6.  \mforall{}a:Pos.  \mforall{}f:Mv[a]  {}\mrightarrow{}  WfdSpread(Pos;a.Mv[a]).    ((\mforall{}m:Mv[a].  P[f  m])  {}\mRightarrow{}  P[mkW(a;f)])
7.  w  :  WfdSpread(Pos;a.Mv[a])@i
8.  n  :  \mBbbN{}@i
9.  s  :  \mBbbN{}n  {}\mrightarrow{}  MoveChoice(Pos;a.Mv[a])@i
10.  \mforall{}t:MoveChoice(Pos;a.Mv[a]).  case  W\_sel(w;n  +  1;s++t)  of  inl(w)  =>  P[w]  |  inr(z)  =>  True
11.  WfdSpread(Pos;a.Mv[a])  \mequiv{}  a:Pos  \mtimes{}  (Mv[a]  {}\mrightarrow{}  WfdSpread(Pos;a.Mv[a]))
12.  a  :  Pos@i
13.  f  :  Mv[a]  {}\mrightarrow{}  WfdSpread(Pos;a.Mv[a])@i
14.  W\_sel(w;n;s)  =  (inl  mkW(a;f))
15.  m  :  Mv[a]@i
\mvdash{}  W\_sel(w;n  +  1;s++\mlambda{}b.if  eq  b  a  then  inl  m  else  inr  \mcdot{}    fi  )  =  (inl  (f  m))


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-1))
  THEN  All  Thin
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  MoveToConcl  (-2)
  THEN  NatInd  (-1)
  THEN  Auto)

---

Home Index