---

Step * 1 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. c : Spread(Pos;a.Mv[a])
6. n1 : ℕ
7. p1 : ℕn1 ⟶ MoveChoice(Pos;a.Mv[a])
8. subgame(b;p1;n1) = (inl a) ∈ (Spread(Pos;a.Mv[a])?)
9. n : ℕ
10. p : ℕn ⟶ MoveChoice(Pos;a.Mv[a])
11. subgame(c;p;n) = (inl b) ∈ (Spread(Pos;a.Mv[a])?)
⊢ ∃n:ℕ. ∃p:ℕn ⟶ MoveChoice(Pos;a.Mv[a]). (subgame(c;p;n) = (inl a) ∈ (Spread(Pos;a.Mv[a])?))
BY
{ TACTIC:(InstConcl [ ⌜n1 + n⌝;⌜λi.if (i) < (n)  then p i  else (p1 (i - n))⌝]⋅ THEN Try (Complete (Auto))) }

1
1. Pos : Type
2. Mv : Pos ⟶ Type
3. a : Spread(Pos;a.Mv[a])
4. b : Spread(Pos;a.Mv[a])
5. c : Spread(Pos;a.Mv[a])
6. n1 : ℕ
7. p1 : ℕn1 ⟶ MoveChoice(Pos;a.Mv[a])
8. subgame(b;p1;n1) = (inl a) ∈ (Spread(Pos;a.Mv[a])?)
9. n : ℕ
10. p : ℕn ⟶ MoveChoice(Pos;a.Mv[a])
11. subgame(c;p;n) = (inl b) ∈ (Spread(Pos;a.Mv[a])?)
⊢ subgame(c;λi.if (i) < (n)  then p i  else (p1 (i - n));n1 + n) = (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.  c  :  Spread(Pos;a.Mv[a])
6.  n1  :  \mBbbN{}
7.  p1  :  \mBbbN{}n1  {}\mrightarrow{}  MoveChoice(Pos;a.Mv[a])
8.  subgame(b;p1;n1)  =  (inl  a)
9.  n  :  \mBbbN{}
10.  p  :  \mBbbN{}n  {}\mrightarrow{}  MoveChoice(Pos;a.Mv[a])
11.  subgame(c;p;n)  =  (inl  b)
\mvdash{}  \mexists{}n:\mBbbN{}.  \mexists{}p:\mBbbN{}n  {}\mrightarrow{}  MoveChoice(Pos;a.Mv[a]).  (subgame(c;p;n)  =  (inl  a))


By

---

Latex:
TACTIC:(InstConcl  [  \mkleeneopen{}n1  +  n\mkleeneclose{};\mkleeneopen{}\mlambda{}i.if  (i)  <  (n)    then  p  i    else  (p1  (i  -  n))\mkleeneclose{}]\mcdot{}
                THEN  Try  (Complete  (Auto))
                )

---

Home Index