---

Step * of Lemma ts-reachable-induction

∀[ts:transition-system{i:l}]. ∀[P:ts-reachable(ts) ⟶ ℙ].
  ((∀x:ts-reachable(ts). SqStable(P[x]))
  ⇒ (∀x,y:ts-reachable(ts).  (P[x] ⇒ (x ts-rel(ts) y) ⇒ P[y])) ⇒ {∀x:ts-reachable(ts). P[x]} 
     supposing P[ts-init(ts)])
BY
{ xxx(Unfold `guard` 0
      THEN xxx(Auto
               THEN (Assert x ∈ ts-reachable(ts) BY
                           Trivial)
               THEN D -2
               THEN Unhide
               THEN Auto
               THEN RepUR ``rel_star infix_ap`` -2
               THEN ExRepD)xxx
      )xxx }

1
1. ts : transition-system{i:l}
2. P : ts-reachable(ts) ⟶ ℙ
3. ∀x:ts-reachable(ts). SqStable(P[x])
4. P[ts-init(ts)]
5. ∀x,y:ts-reachable(ts).  (P[x] ⇒ (x ts-rel(ts) y) ⇒ P[y])
6. x : ts-type(ts)
7. n : ℕ
8. ts-rel(ts)^n ts-init(ts) x
9. x ∈ ts-reachable(ts)
⊢ P[x]

---

Latex:

---

Latex:
\mforall{}[ts:transition-system\{i:l\}].  \mforall{}[P:ts-reachable(ts)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x:ts-reachable(ts).  SqStable(P[x]))
    {}\mRightarrow{}  (\mforall{}x,y:ts-reachable(ts).    (P[x]  {}\mRightarrow{}  (x  ts-rel(ts)  y)  {}\mRightarrow{}  P[y]))  {}\mRightarrow{}  \{\mforall{}x:ts-reachable(ts).  P[x]\} 
          supposing  P[ts-init(ts)])


By

---

Latex:
xxx(Unfold  `guard`  0
        THEN  xxx(Auto
                          THEN  (Assert  x  \mmember{}  ts-reachable(ts)  BY
                                                  Trivial)
                          THEN  D  -2
                          THEN  Unhide
                          THEN  Auto
                          THEN  RepUR  ``rel\_star  infix\_ap``  -2
                          THEN  ExRepD)xxx
        )xxx

---

Home Index