---

Step * of Lemma ts-refinement-reachable2

∀ts1,ts2:transition-system{i:l}. ∀f:ts-type(ts2) ⟶ ts-type(ts1).
  (ts-refinement(ts1;ts2;f)
  ⇒ (∀s1,s2:ts-reachable(ts2).  ((s1 (ts-rel(ts2)^*) s2) ⇒ ((f s1) (ts-rel(ts1)^*) (f s2)))))
BY
{ (RepeatFor 4 ((D 0 THENA Auto)) THEN Unfold `ts-reachable` 0 THEN BLemma `rel-preserving-star-reachable`⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}ts1,ts2:transition-system\{i:l\}.  \mforall{}f:ts-type(ts2)  {}\mrightarrow{}  ts-type(ts1).
    (ts-refinement(ts1;ts2;f)
    {}\mRightarrow{}  (\mforall{}s1,s2:ts-reachable(ts2).
                ((s1  rel\_star(ts-type(ts2);  ts-rel(ts2))  s2)  {}\mRightarrow{}  ((f  s1)  (ts-rel(ts1)\^{}*)  (f  s2)))))


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  Unfold  `ts-reachable`  0
  THEN  BLemma  `rel-preserving-star-reachable`\mcdot{}
  THEN  Auto)

---

Home Index