---

Step * 2 1 1 2 of Lemma WfdSpread-induction


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])?)
BY
{ ((Unfold `W_sel` 0 THEN RecUnfold `subgame` 0 THEN AutoSplit)
   THEN Unfold `W_sel` (-2)
   THEN RecUnfold `subgame` (-2)
   THEN SplitOnHypITE -2 
   THEN Auto
   THEN RepUR ``seq-adjoin seq-append`` 0
   THEN MoveToConcl (-3)
   THEN (InstLemma `WfdSpread-ext` [⌜Pos⌝;⌜Mv⌝]⋅ THENA Auto)
   THEN ((GenConcl ⌜w = z ∈ (a:Pos × (Mv[a] ⟶ WfdSpread(Pos;a.Mv[a])))⌝⋅ THENA Auto)
         THEN (D -2 THEN Reduce 0)
         THEN GenConclAtAddr [1;2;1]
         THEN D -2
         THEN Reduce 0
         THEN Try (Fold `W_sel` 0))⋅)⋅ }

1
1. Pos : Type
2. eq : EqDecider(Pos)
3. Mv : Pos ⟶ Type
4. n : ℤ
5. n + 1 ≠ 0
6. 0 < n
7. ∀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])?))))
8. w : WfdSpread(Pos;a.Mv[a])@i
9. s : ℕn ⟶ MoveChoice(Pos;a.Mv[a])@i
10. a : Pos@i
11. f : Mv[a] ⟶ WfdSpread(Pos;a.Mv[a])@i
12. m : Mv[a]@i
13. ¬(n = 0 ∈ ℤ)
14. WfdSpread(Pos;a.Mv[a]) ≡ a:Pos × (Mv[a] ⟶ WfdSpread(Pos;a.Mv[a]))
15. a1 : Pos@i
16. z1 : Mv[a1] ⟶ WfdSpread(Pos;a.Mv[a])@i
17. w = <a1, z1> ∈ (a:Pos × (Mv[a] ⟶ WfdSpread(Pos;a.Mv[a])))
18. x : Mv[a1]@i
19. (s 0 a1) = (inl x) ∈ (Mv[a1]?)
⊢ (W_sel(z1 x;n - 1;λi.(s (i + 1))) = (inl mkW(a;f)) ∈ (WfdSpread(Pos;a.Mv[a])?))
⇒ (W_sel(z1 x;(n + 1) - 1;λi.if (i + 1) < (n)
                                 then s (i + 1)
                                 else if (i + 1) < (n + 1)  then λb.if eq b a then inl m else inr ⋅  fi   else ⊥)
   = (inl (f m))
   ∈ (WfdSpread(Pos;a.Mv[a])?))

2
1. Pos : Type
2. eq : EqDecider(Pos)
3. Mv : Pos ⟶ Type
4. n : ℤ
5. n + 1 ≠ 0
6. 0 < n
7. ∀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])?))))
8. w : WfdSpread(Pos;a.Mv[a])@i
9. s : ℕn ⟶ MoveChoice(Pos;a.Mv[a])@i
10. a : Pos@i
11. f : Mv[a] ⟶ WfdSpread(Pos;a.Mv[a])@i
12. m : Mv[a]@i
13. ¬(n = 0 ∈ ℤ)
14. WfdSpread(Pos;a.Mv[a]) ≡ a:Pos × (Mv[a] ⟶ WfdSpread(Pos;a.Mv[a]))
15. a1 : Pos@i
16. z1 : Mv[a1] ⟶ WfdSpread(Pos;a.Mv[a])@i
17. w = <a1, z1> ∈ (a:Pos × (Mv[a] ⟶ WfdSpread(Pos;a.Mv[a])))
18. y : Unit@i
19. (s 0 a1) = (inr y ) ∈ (Mv[a1]?)
⊢ ((inr y ) = (inl mkW(a;f)) ∈ (WfdSpread(Pos;a.Mv[a])?)) ⇒ ((inr y ) = (inl (f m)) ∈ (WfdSpread(Pos;a.Mv[a])?))

---

Latex:

---

Latex:

1.  Pos  :  Type
2.  eq  :  EqDecider(Pos)
3.  Mv  :  Pos  {}\mrightarrow{}  Type
4.  n  :  \mBbbZ{}
5.  0  <  n
6.  \mforall{}w:WfdSpread(Pos;a.Mv[a]).  \mforall{}s:\mBbbN{}n  -  1  {}\mrightarrow{}  MoveChoice(Pos;a.Mv[a]).  \mforall{}a:Pos.
      \mforall{}f:Mv[a]  {}\mrightarrow{}  WfdSpread(Pos;a.Mv[a]).
          ((W\_sel(w;n  -  1;s)  =  (inl  mkW(a;f)))
          {}\mRightarrow{}  (\mforall{}m:Mv[a].  (W\_sel(w;(n  -  1)  +  1;s++\mlambda{}b.if  eq  b  a  then  inl  m  else  inr  \mcdot{}    fi  )  =  (inl  (f  m)))))
7.  w  :  WfdSpread(Pos;a.Mv[a])@i
8.  s  :  \mBbbN{}n  {}\mrightarrow{}  MoveChoice(Pos;a.Mv[a])@i
9.  a  :  Pos@i
10.  f  :  Mv[a]  {}\mrightarrow{}  WfdSpread(Pos;a.Mv[a])@i
11.  W\_sel(w;n;s)  =  (inl  mkW(a;f))
12.  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:
((Unfold  `W\_sel`  0  THEN  RecUnfold  `subgame`  0  THEN  AutoSplit)
  THEN  Unfold  `W\_sel`  (-2)
  THEN  RecUnfold  `subgame`  (-2)
  THEN  SplitOnHypITE  -2 
  THEN  Auto
  THEN  RepUR  ``seq-adjoin  seq-append``  0
  THEN  MoveToConcl  (-3)
  THEN  (InstLemma  `WfdSpread-ext`  [\mkleeneopen{}Pos\mkleeneclose{};\mkleeneopen{}Mv\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ((GenConcl  \mkleeneopen{}w  =  z\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  (D  -2  THEN  Reduce  0)
              THEN  GenConclAtAddr  [1;2;1]
              THEN  D  -2
              THEN  Reduce  0
              THEN  Try  (Fold  `W\_sel`  0))\mcdot{})\mcdot{}

---

Home Index