---

Step * 1 1 1 1 1 2 of Lemma sub-spread-transitive

.....wf..... 
1. Pos : Type
2. Mv : Pos ⟶ Type
3. a : Spread(Pos;a.Mv[a])
4. b : Spread(Pos;a.Mv[a])
5. n1 : ℕ
6. p1 : ℕn1 ⟶ MoveChoice(Pos;a.Mv[a])
7. subgame(b;p1;n1) = (inl a) ∈ (Spread(Pos;a.Mv[a])?)
8. n : ℤ
9. c : Spread(Pos;a.Mv[a])
10. p : ℕ0 ⟶ MoveChoice(Pos;a.Mv[a])
11. c = b ∈ Spread(Pos;a.Mv[a])
12. z : Spread(Pos;a.Mv[a])
⊢ subgame(z;λi.if (i) < (0)  then p i  else (p1 (i - 0));n1 + 0) = (inl a) ∈ (Spread(Pos;a.Mv[a])?) ∈ ℙ
BY
{ (RepeatFor 2 ((MemCD THEN Try (Complete (Auto)))) THEN Unfold `Play` 0 THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  Pos  :  Type
2.  Mv  :  Pos  {}\mrightarrow{}  Type
3.  a  :  Spread(Pos;a.Mv[a])
4.  b  :  Spread(Pos;a.Mv[a])
5.  n1  :  \mBbbN{}
6.  p1  :  \mBbbN{}n1  {}\mrightarrow{}  MoveChoice(Pos;a.Mv[a])
7.  subgame(b;p1;n1)  =  (inl  a)
8.  n  :  \mBbbZ{}
9.  c  :  Spread(Pos;a.Mv[a])
10.  p  :  \mBbbN{}0  {}\mrightarrow{}  MoveChoice(Pos;a.Mv[a])
11.  c  =  b
12.  z  :  Spread(Pos;a.Mv[a])
\mvdash{}  subgame(z;\mlambda{}i.if  (i)  <  (0)    then  p  i    else  (p1  (i  -  0));n1  +  0)  =  (inl  a)  \mmember{}  \mBbbP{}


By

---

Latex:
(RepeatFor  2  ((MemCD  THEN  Try  (Complete  (Auto))))  THEN  Unfold  `Play`  0  THEN  Auto)

---

Home Index