---

Step * of Lemma ts-refinement_wf

∀[ts1,ts2:transition-system{i:l}]. ∀[f:ts-type(ts2) ⟶ ts-type(ts1)].  (ts-refinement(ts1;ts2;f) ∈ ℙ)
BY
{ xxxProveWfLemmaxxx }

---

Latex:

---

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


By

---

Latex:
xxxProveWfLemmaxxx

---

Home Index