---

Step * 1 of Lemma ts-refinement-composition


1. ts1 : transition-system{i:l}
2. ts2 : transition-system{i:l}
3. ts3 : transition-system{i:l}
4. g : ts-type(ts3) ⟶ ts-type(ts2)
5. f : ts-type(ts2) ⟶ ts-type(ts1)
6. ts-init(ts1) (ts-rel(ts1)^*) (f ts-init(ts2))
7. ∀x,y:ts-reachable(ts2).  ((x ts-rel(ts2) y) ⇒ ((f x) (ts-rel(ts1)^*) (f y)))
8. ∀x:ts-reachable(ts1). ((ts-final(ts1) x) ⇒ (∃y:ts-reachable(ts2). ((ts-final(ts2) y) ∧ ((f y) = x ∈ ts-type(ts1)))))
9. ts-init(ts2) (ts-rel(ts2)^*) (g ts-init(ts3))
10. ∀x,y:ts-reachable(ts3).  ((x ts-rel(ts3) y) ⇒ ((g x) (ts-rel(ts2)^*) (g y)))
11. ∀x:ts-reachable(ts2)
      ((ts-final(ts2) x) ⇒ (∃y:ts-reachable(ts3). ((ts-final(ts3) y) ∧ ((g y) = x ∈ ts-type(ts2)))))
12. ∀x,y:ts-reachable(ts2).  ((x (ts-rel(ts2)^*) y) ⇒ ((f x) (ts-rel(ts1)^*) (f y)))
13. ∀x,y:ts-reachable(ts3).  ((x (ts-rel(ts3)^*) y) ⇒ ((g x) (ts-rel(ts2)^*) (g y)))
⊢ ts-init(ts1) (ts-rel(ts1)^*) (f (g ts-init(ts3)))
BY
{ (Using [`y', ⌜f ts-init(ts2)⌝] (BLemma `rel_star_transitivity`)⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  ts1  :  transition-system\{i:l\}
2.  ts2  :  transition-system\{i:l\}
3.  ts3  :  transition-system\{i:l\}
4.  g  :  ts-type(ts3)  {}\mrightarrow{}  ts-type(ts2)
5.  f  :  ts-type(ts2)  {}\mrightarrow{}  ts-type(ts1)
6.  ts-init(ts1)  rel\_star(ts-type(ts1);  ts-rel(ts1))  (f  ts-init(ts2))
7.  \mforall{}x,y:ts-reachable(ts2).    ((x  ts-rel(ts2)  y)  {}\mRightarrow{}  ((f  x)  rel\_star(ts-type(ts1);  ts-rel(ts1))  (f  y)))
8.  \mforall{}x:ts-reachable(ts1)
          ((ts-final(ts1)  x)  {}\mRightarrow{}  (\mexists{}y:ts-reachable(ts2).  ((ts-final(ts2)  y)  \mwedge{}  ((f  y)  =  x))))
9.  ts-init(ts2)  rel\_star(ts-type(ts2);  ts-rel(ts2))  (g  ts-init(ts3))
10.  \mforall{}x,y:ts-reachable(ts3).
            ((x  ts-rel(ts3)  y)  {}\mRightarrow{}  ((g  x)  (ts-rel(ts2)\^{}*)  (g  y)))
11.  \mforall{}x:ts-reachable(ts2)
            ((ts-final(ts2)  x)  {}\mRightarrow{}  (\mexists{}y:ts-reachable(ts3).  ((ts-final(ts3)  y)  \mwedge{}  ((g  y)  =  x))))
12.  \mforall{}x,y:ts-reachable(ts2).
            ((x  (ts-rel(ts2)\^{}*)  y)  {}\mRightarrow{}  ((f  x)  (ts-rel(ts1)\^{}*)  (f  y)))
13.  \mforall{}x,y:ts-reachable(ts3).
            ((x  (ts-rel(ts3)\^{}*)  y)  {}\mRightarrow{}  ((g  x)  (ts-rel(ts2)\^{}*)  (g  y)))
\mvdash{}  ts-init(ts1)  rel\_star(ts-type(ts1);  ts-rel(ts1))  (f  (g  ts-init(ts3)))


By

---

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

---

Home Index