---

Step * of Lemma sub-spread-transitive

∀[Pos:Type]. ∀[Mv:Pos ⟶ Type].  Trans(Spread(Pos;a.Mv[a]);s',s.s' ≤ s)
BY
{ (Auto THEN D 0 THEN Auto THEN All (Unfold `sub-spread`)⋅ THEN ExRepD) }

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])?)
⊢ ∃n:ℕ. ∃p:ℕn ⟶ MoveChoice(Pos;a.Mv[a]). (subgame(c;p;n) = (inl a) ∈ (Spread(Pos;a.Mv[a])?))

---

Latex:

---

Latex:
\mforall{}[Pos:Type].  \mforall{}[Mv:Pos  {}\mrightarrow{}  Type].    Trans(Spread(Pos;a.Mv[a]);s',s.s'  \mleq{}  s)


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  All  (Unfold  `sub-spread`)\mcdot{}  THEN  ExRepD)

---

Home Index