---

Step * 1 of Lemma ts-stable-star


1. ts : transition-system{i:l}
2. [P] : ts-type(ts) ⟶ ℙ
3. ts-stable(ts;x.P[x])
4. n : ℤ
5. [%2] : 0 < n
6. ∀x,y:ts-type(ts).  (P[x] ⇒ (x ts-rel(ts)^n - 1 y) ⇒ P[y])
7. ¬(n = 0 ∈ ℤ)
8. x : ts-type(ts)
9. y@0 : ts-type(ts)
10. P[x]
11. z : ts-type(ts)
12. x ts-rel(ts) z
13. z ts-rel(ts)^n - 1 y@0
⊢ P[y@0]
BY
{ xxxOnMaybeHyp 6 (\h. (InstHyp [⌜z⌝;⌜y@0⌝] h⋅ THEN Auto))xxx }

---

Latex:

---

Latex:

1.  ts  :  transition-system\{i:l\}
2.  [P]  :  ts-type(ts)  {}\mrightarrow{}  \mBbbP{}
3.  ts-stable(ts;x.P[x])
4.  n  :  \mBbbZ{}
5.  [\%2]  :  0  <  n
6.  \mforall{}x,y:ts-type(ts).    (P[x]  {}\mRightarrow{}  (x  rel\_exp(ts-type(ts);  ts-rel(ts);  n  -  1)  y)  {}\mRightarrow{}  P[y])
7.  \mneg{}(n  =  0)
8.  x  :  ts-type(ts)
9.  y@0  :  ts-type(ts)
10.  P[x]
11.  z  :  ts-type(ts)
12.  x  ts-rel(ts)  z
13.  z  rel\_exp(ts-type(ts);  ts-rel(ts);  n  -  1)  y@0
\mvdash{}  P[y@0]


By

---

Latex:
xxxOnMaybeHyp  6  (\mbackslash{}h.  (InstHyp  [\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}y@0\mkleeneclose{}]  h\mcdot{}  THEN  Auto))xxx

---

Home Index