---

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


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. n1 + n ≠ 0
10. 0 < n
11. ∀c:Spread(Pos;a.Mv[a]). ∀p:ℕn - 1 ⟶ MoveChoice(Pos;a.Mv[a]).
      ((subgame(c;p;n - 1) = (inl b) ∈ (Spread(Pos;a.Mv[a])?))
      ⇒ (subgame(c;λi.if (i) < (n - 1)  then p i  else (p1 (i - n - 1));n1 + (n - 1))
         = (inl a)
         ∈ (Spread(Pos;a.Mv[a])?)))
12. c : Spread(Pos;a.Mv[a])
13. p : ℕn ⟶ MoveChoice(Pos;a.Mv[a])
14. ¬(n = 0 ∈ ℤ)
15. a1 : Pos
16. g1 : Mv[a1] ⟶ Spread(Pos;a.Mv[a])
17. c = <a1, g1> ∈ (a:Pos × (Mv[a] ⟶ Spread(Pos;a.Mv[a])))
⊢ (case p 0 a1 of inl(m) => subgame(g1 m;λi.(p (i + 1));n - 1) | inr(z) => inr z  = (inl b) ∈ (Spread(Pos;a.Mv[a])?))
⇒ (case p 0 a1
    of inl(m) =>
    subgame(g1 m;λi.if (i + 1) < (n)  then p (i + 1)  else (p1 ((i + 1) - n));(n1 + n) - 1)
    | inr(z) =>
    inr z 
   = (inl a)
   ∈ (Spread(Pos;a.Mv[a])?))
BY
{ (GenConclAtAddr [1;2;1] THEN D -2 THEN Reduce 0) }

1
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. n1 + n ≠ 0
10. 0 < n
11. ∀c:Spread(Pos;a.Mv[a]). ∀p:ℕn - 1 ⟶ MoveChoice(Pos;a.Mv[a]).
      ((subgame(c;p;n - 1) = (inl b) ∈ (Spread(Pos;a.Mv[a])?))
      ⇒ (subgame(c;λi.if (i) < (n - 1)  then p i  else (p1 (i - n - 1));n1 + (n - 1))
         = (inl a)
         ∈ (Spread(Pos;a.Mv[a])?)))
12. c : Spread(Pos;a.Mv[a])
13. p : ℕn ⟶ MoveChoice(Pos;a.Mv[a])
14. ¬(n = 0 ∈ ℤ)
15. a1 : Pos
16. g1 : Mv[a1] ⟶ Spread(Pos;a.Mv[a])
17. c = <a1, g1> ∈ (a:Pos × (Mv[a] ⟶ Spread(Pos;a.Mv[a])))
18. x : Mv[a1]
19. (p 0 a1) = (inl x) ∈ (Mv[a1]?)
⊢ (subgame(g1 x;λi.(p (i + 1));n - 1) = (inl b) ∈ (Spread(Pos;a.Mv[a])?))
⇒ (subgame(g1 x;λi.if (i + 1) < (n)  then p (i + 1)  else (p1 ((i + 1) - n));(n1 + n) - 1)
   = (inl a)
   ∈ (Spread(Pos;a.Mv[a])?))

2
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. n1 + n ≠ 0
10. 0 < n
11. ∀c:Spread(Pos;a.Mv[a]). ∀p:ℕn - 1 ⟶ MoveChoice(Pos;a.Mv[a]).
      ((subgame(c;p;n - 1) = (inl b) ∈ (Spread(Pos;a.Mv[a])?))
      ⇒ (subgame(c;λi.if (i) < (n - 1)  then p i  else (p1 (i - n - 1));n1 + (n - 1))
         = (inl a)
         ∈ (Spread(Pos;a.Mv[a])?)))
12. c : Spread(Pos;a.Mv[a])
13. p : ℕn ⟶ MoveChoice(Pos;a.Mv[a])
14. ¬(n = 0 ∈ ℤ)
15. a1 : Pos
16. g1 : Mv[a1] ⟶ Spread(Pos;a.Mv[a])
17. c = <a1, g1> ∈ (a:Pos × (Mv[a] ⟶ Spread(Pos;a.Mv[a])))
18. y : Unit
19. (p 0 a1) = (inr y ) ∈ (Mv[a1]?)
⊢ ((inr y ) = (inl b) ∈ (Spread(Pos;a.Mv[a])?)) ⇒ ((inr y ) = (inl a) ∈ (Spread(Pos;a.Mv[a])?))

---

Latex:

---

Latex:

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.  n1  +  n  \mneq{}  0
10.  0  <  n
11.  \mforall{}c:Spread(Pos;a.Mv[a]).  \mforall{}p:\mBbbN{}n  -  1  {}\mrightarrow{}  MoveChoice(Pos;a.Mv[a]).
            ((subgame(c;p;n  -  1)  =  (inl  b))
            {}\mRightarrow{}  (subgame(c;\mlambda{}i.if  (i)  <  (n  -  1)    then  p  i    else  (p1  (i  -  n  -  1));n1  +  (n  -  1))  =  (inl  a)))
12.  c  :  Spread(Pos;a.Mv[a])
13.  p  :  \mBbbN{}n  {}\mrightarrow{}  MoveChoice(Pos;a.Mv[a])
14.  \mneg{}(n  =  0)
15.  a1  :  Pos
16.  g1  :  Mv[a1]  {}\mrightarrow{}  Spread(Pos;a.Mv[a])
17.  c  =  <a1,  g1>
\mvdash{}  (case  p  0  a1  of  inl(m)  =>  subgame(g1  m;\mlambda{}i.(p  (i  +  1));n  -  1)  |  inr(z)  =>  inr  z    =  (inl  b))
{}\mRightarrow{}  (case  p  0  a1
        of  inl(m)  =>
        subgame(g1  m;\mlambda{}i.if  (i  +  1)  <  (n)    then  p  (i  +  1)    else  (p1  ((i  +  1)  -  n));(n1  +  n)  -  1)
        |  inr(z)  =>
        inr  z 
      =  (inl  a))


By

---

Latex:
(GenConclAtAddr  [1;2;1]  THEN  D  -2  THEN  Reduce  0)

---

Home Index