---

Step * of Lemma ts-reachable-induction2

∀ts:transition-system{i:l}
  ∀[P:ts-reachable(ts) ⟶ ℙ]
    (P[ts-init(ts)]
    ⇒ (∀x,y:ts-reachable(ts).  (P[x] ⇒ (x ts-rel(ts) y) ⇒ P[y]))
    ⇒ {∀x:ts-type(ts). ((ts-init(ts) (ts-rel(ts)^*) x) ⇒ P[x])})
BY
{ (InstLemma `ts-reachable-induction3` [] THEN RepeatFor 4 ((ParallelLast' THENA Auto)) THEN MemTypeCD THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `ts-reachable-induction3`  []
  THEN  RepeatFor  4  ((ParallelLast'  THENA  Auto))
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index