---

Step * of Lemma ts-reachable-induction3

∀ts:transition-system{i:l}
  ∀[P:ts-reachable(ts) ⟶ ℙ]
    (P[ts-init(ts)]
    ⇒ (∀x:ts-type(ts). ((ts-init(ts) (ts-rel(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
{ xxx(Unfold `guard` 0
      THEN xxx(Auto
               THEN (Assert x ∈ ts-reachable(ts) BY
                           (MemTypeCD 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. P[ts-init(ts)]
4. ∀x:ts-type(ts). ((ts-init(ts) (ts-rel(ts)^*) x) ⇒ (∀y:ts-reachable(ts). (P[x] ⇒ (x ts-rel(ts) y) ⇒ P[y])))
5. x : ts-type(ts)
6. n : ℕ
7. ts-rel(ts)^n ts-init(ts) x
8. x ∈ ts-reachable(ts)
⊢ P[x]

---

Latex:

---

Latex:
\mforall{}ts:transition-system\{i:l\}
    \mforall{}[P:ts-reachable(ts)  {}\mrightarrow{}  \mBbbP{}]
        (P[ts-init(ts)]
        {}\mRightarrow{}  (\mforall{}x:ts-type(ts)
                    ((ts-init(ts)  rel\_star(ts-type(ts);  ts-rel(ts))  x)
                    {}\mRightarrow{}  (\mforall{}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:
xxx(Unfold  `guard`  0
        THEN  xxx(Auto
                          THEN  (Assert  x  \mmember{}  ts-reachable(ts)  BY
                                                  (MemTypeCD  THEN  Auto))
                          THEN  RepUR  ``rel\_star  infix\_ap``  -2
                          THEN  ExRepD)xxx
        )xxx

---

Home Index