---

Step * of Lemma ts-refinement-reachable

∀[ts1,ts2:transition-system{i:l}]. ∀[f:ts-type(ts2) ⟶ ts-type(ts1)].
  ∀[s:ts-reachable(ts2)]. (f s ∈ ts-reachable(ts1)) supposing ts-refinement(ts1;ts2;f)
BY
{ ((UnivCD THENA Auto)
   THEN D -1
   THEN MemTypeCD
   THEN Auto
   THEN Using [`y',⌜f ts-init(ts2)⌝] (BLemma `rel_star_transitivity`)⋅
   THEN Auto
   THEN BLemma `ts-refinement-reachable2`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[ts1,ts2:transition-system\{i:l\}].  \mforall{}[f:ts-type(ts2)  {}\mrightarrow{}  ts-type(ts1)].
    \mforall{}[s:ts-reachable(ts2)].  (f  s  \mmember{}  ts-reachable(ts1))  supposing  ts-refinement(ts1;ts2;f)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto
  THEN  Using  [`y',\mkleeneopen{}f  ts-init(ts2)\mkleeneclose{}]  (BLemma  `rel\_star\_transitivity`)\mcdot{}
  THEN  Auto
  THEN  BLemma  `ts-refinement-reachable2`
  THEN  Auto)

---

Home Index