---

Step * of Lemma ts-stable-star

∀ts:transition-system{i:l}
  ∀[P:ts-type(ts) ⟶ ℙ]. (ts-stable(ts;x.P[x]) ⇒ (∀x,y:ts-type(ts).  (P[x] ⇒ (x (ts-rel(ts)^*) y) ⇒ P[y])))
BY
{ xxx(Auto
      THEN RepUR ``rel_star infix_ap`` -1
      THEN D -1
      THEN Fold `infix_ap` (-1)
      THEN MoveToConcl (-1)
      THEN RepeatFor 3 (MoveToConcl (-2))
      THEN NatInd (-1)
      THEN RecUnfold `rel_exp` 0
      THEN (SplitOnConclITE THENM Reduce 0)
      THEN Auto
      THEN ExRepD)xxx }

1
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]

---

Latex:

---

Latex:
\mforall{}ts:transition-system\{i:l\}
    \mforall{}[P:ts-type(ts)  {}\mrightarrow{}  \mBbbP{}]
        (ts-stable(ts;x.P[x])  {}\mRightarrow{}  (\mforall{}x,y:ts-type(ts).    (P[x]  {}\mRightarrow{}  (x  (ts-rel(ts)\^{}*)  y)  {}\mRightarrow{}  P[y])))


By

---

Latex:
xxx(Auto
        THEN  RepUR  ``rel\_star  infix\_ap``  -1
        THEN  D  -1
        THEN  Fold  `infix\_ap`  (-1)
        THEN  MoveToConcl  (-1)
        THEN  RepeatFor  3  (MoveToConcl  (-2))
        THEN  NatInd  (-1)
        THEN  RecUnfold  `rel\_exp`  0
        THEN  (SplitOnConclITE  THENM  Reduce  0)
        THEN  Auto
        THEN  ExRepD)xxx

---

Home Index