---

Step * 1 1 of Lemma WfdSpread-ext


1. Pos : Type
2. ∀a,b:Pos.  Dec(a = b ∈ Pos)
3. Mv : Pos ⟶ Type
4. Spread(Pos;a.Mv[a]) ≡ a:Pos × (Mv[a] ⟶ Spread(Pos;a.Mv[a]))
5. x : Spread(Pos;a.Mv[a])
6. ∀p:ℕ ⟶ MoveChoice(Pos;a.Mv[a]). (↓∃n:ℕ. resigned(subgame(x;p;n)))
⊢ x ∈ a:Pos × (Mv[a] ⟶ WfdSpread(Pos;a.Mv[a]))
BY
{ (MoveToConcl (-1)
   THEN (GenConcl ⌜x = g ∈ (a:Pos × (Mv[a] ⟶ Spread(Pos;a.Mv[a])))⌝⋅ THENA Auto)
   THEN D -2
   THEN Reduce 0
   THEN Auto
   THEN Try ((D 4 THEN SubsumeC ⌜a:Pos × (Mv[a] ⟶ Spread(Pos;a.Mv[a]))⌝⋅ THEN CompleteAuto))) }

1
1. Pos : Type
2. ∀a,b:Pos.  Dec(a = b ∈ Pos)
3. Mv : Pos ⟶ Type
4. Spread(Pos;a.Mv[a]) ≡ a:Pos × (Mv[a] ⟶ Spread(Pos;a.Mv[a]))
5. x : Spread(Pos;a.Mv[a])
6. a : Pos
7. g1 : Mv[a] ⟶ Spread(Pos;a.Mv[a])
8. x = <a, g1> ∈ (a:Pos × (Mv[a] ⟶ Spread(Pos;a.Mv[a])))
9. ∀p:ℕ ⟶ MoveChoice(Pos;a.Mv[a]). (↓∃n:ℕ. resigned(subgame(<a, g1>;p;n)))
⊢ g1 ∈ Mv[a] ⟶ WfdSpread(Pos;a.Mv[a])

---

Latex:

---

Latex:

1.  Pos  :  Type
2.  \mforall{}a,b:Pos.    Dec(a  =  b)
3.  Mv  :  Pos  {}\mrightarrow{}  Type
4.  Spread(Pos;a.Mv[a])  \mequiv{}  a:Pos  \mtimes{}  (Mv[a]  {}\mrightarrow{}  Spread(Pos;a.Mv[a]))
5.  x  :  Spread(Pos;a.Mv[a])
6.  \mforall{}p:\mBbbN{}  {}\mrightarrow{}  MoveChoice(Pos;a.Mv[a]).  (\mdownarrow{}\mexists{}n:\mBbbN{}.  resigned(subgame(x;p;n)))
\mvdash{}  x  \mmember{}  a:Pos  \mtimes{}  (Mv[a]  {}\mrightarrow{}  WfdSpread(Pos;a.Mv[a]))


By

---

Latex:
(MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}x  =  g\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((D  4  THEN  SubsumeC  \mkleeneopen{}a:Pos  \mtimes{}  (Mv[a]  {}\mrightarrow{}  Spread(Pos;a.Mv[a]))\mkleeneclose{}\mcdot{}  THEN  CompleteAuto)))

---

Home Index