---

Step * 1 1 1 1 1 2 1 2 of Lemma WfdSpread-ext

.....falsecase..... 
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)))
10. m : Mv[a]
11. p : ℕ ⟶ MoveChoice(Pos;a.Mv[a])
12. eq : EqDecider(Pos)
13. n : ℕ
14. resigned(case if eq a a then inl m else inr ⋅  fi 
 of inl(m1) =>
 subgame(g1 m1;λi.if (i + 1 =z 0) then λb.if eq b a then inl m else inr ⋅  fi  else p ((i + 1) - 1) fi ;n - 1)
 | inr(z) =>
 inr z )
15. ¬(n = 0 ∈ ℤ)
⊢ ↓∃n:ℕ. resigned(subgame(g1 m;p;n))
BY
{ (SplitOnHypITE -2  THENA Auto)⋅ }

1
.....truecase..... 
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)))
10. m : Mv[a]
11. p : ℕ ⟶ MoveChoice(Pos;a.Mv[a])
12. eq : EqDecider(Pos)
13. n : ℕ
14. resigned(case inl m
 of inl(m1) =>
 subgame(g1 m1;λi.if (i + 1 =z 0) then λb.if eq b a then inl m else inr ⋅  fi  else p ((i + 1) - 1) fi ;n - 1)
 | inr(z) =>
 inr z )
15. ¬(n = 0 ∈ ℤ)
16. a = a ∈ Pos
⊢ ↓∃n:ℕ. resigned(subgame(g1 m;p;n))

2
.....falsecase..... 
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)))
10. m : Mv[a]
11. p : ℕ ⟶ MoveChoice(Pos;a.Mv[a])
12. eq : EqDecider(Pos)
13. n : ℕ
14. resigned(case inr ⋅ 
 of inl(m1) =>
 subgame(g1 m1;λi.if (i + 1 =z 0) then λb.if eq b a then inl m else inr ⋅  fi  else p ((i + 1) - 1) fi ;n - 1)
 | inr(z) =>
 inr z )
15. ¬(n = 0 ∈ ℤ)
16. ¬(a = a ∈ Pos)
⊢ ↓∃n:ℕ. resigned(subgame(g1 m;p;n))

---

Latex:

---

Latex:
.....falsecase..... 
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.  a  :  Pos
7.  g1  :  Mv[a]  {}\mrightarrow{}  Spread(Pos;a.Mv[a])
8.  x  =  <a,  g1>
9.  \mforall{}p:\mBbbN{}  {}\mrightarrow{}  MoveChoice(Pos;a.Mv[a]).  (\mdownarrow{}\mexists{}n:\mBbbN{}.  resigned(subgame(<a,  g1>p;n)))
10.  m  :  Mv[a]
11.  p  :  \mBbbN{}  {}\mrightarrow{}  MoveChoice(Pos;a.Mv[a])
12.  eq  :  EqDecider(Pos)
13.  n  :  \mBbbN{}
14.  resigned(case  if  eq  a  a  then  inl  m  else  inr  \mcdot{}    fi 
  of  inl(m1)  =>
  subgame(g1  m1;\mlambda{}i.if  (i  +  1  =\msubz{}  0)
                                    then  \mlambda{}b.if  eq  b  a  then  inl  m  else  inr  \mcdot{}    fi 
                                    else  p  ((i  +  1)  -  1)
                                    fi  ;n  -  1)
  |  inr(z)  =>
  inr  z  )
15.  \mneg{}(n  =  0)
\mvdash{}  \mdownarrow{}\mexists{}n:\mBbbN{}.  resigned(subgame(g1  m;p;n))


By

---

Latex:
(SplitOnHypITE  -2    THENA  Auto)\mcdot{}

---

Home Index