---

Step * 2 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 : a:Pos × (Mv[a] ⟶ WfdSpread(Pos;a.Mv[a]))
6. x ∈ Spread(Pos;a.Mv[a])
⊢ x ∈ WfdSpread(Pos;a.Mv[a])
BY
{ (MemTypeCD
   THEN Auto
   THEN DVar`x'
   THEN RecUnfold `subgame` 0
   THEN Reduce 0
   THEN (GenConclTerm ⌜p 0 a⌝⋅ THENA Auto)
   THEN D -2
   THEN Reduce 0
   THEN Auto)⋅ }

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. a : Pos
6. x1 : Mv[a] ⟶ WfdSpread(Pos;a.Mv[a])
7. <a, x1> ∈ Spread(Pos;a.Mv[a])
8. p : ℕ ⟶ MoveChoice(Pos;a.Mv[a])
9. x : Mv[a]
10. (p 0 a) = (inl x) ∈ (Mv[a]?)
⊢ ↓∃n:ℕ. resigned(if (n =z 0) then inl <a, x1> else subgame(x1 x;λi.(p (i + 1));n - 1) fi )

2
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. a : Pos
6. x1 : Mv[a] ⟶ WfdSpread(Pos;a.Mv[a])
7. <a, x1> ∈ Spread(Pos;a.Mv[a])
8. p : ℕ ⟶ MoveChoice(Pos;a.Mv[a])
9. y : Unit
10. (p 0 a) = (inr y ) ∈ (Mv[a]?)
⊢ ↓∃n:ℕ. resigned(if (n =z 0) then inl <a, x1> else inr y  fi )

---

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  :  a:Pos  \mtimes{}  (Mv[a]  {}\mrightarrow{}  WfdSpread(Pos;a.Mv[a]))
6.  x  \mmember{}  Spread(Pos;a.Mv[a])
\mvdash{}  x  \mmember{}  WfdSpread(Pos;a.Mv[a])


By

---

Latex:
(MemTypeCD
  THEN  Auto
  THEN  DVar`x'
  THEN  RecUnfold  `subgame`  0
  THEN  Reduce  0
  THEN  (GenConclTerm  \mkleeneopen{}p  0  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto)\mcdot{}

---

Home Index