---

Step * 2 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)))
14. ts-init(ts1) (ts-rel(ts1)^*) (f (g ts-init(ts3)))
15. x : ts-reachable(ts3)
16. y : ts-reachable(ts3)
17. x ts-rel(ts3) y
18. (g x ∈ ts-reachable(ts2)) ∧ (g y ∈ ts-reachable(ts2))
⊢ (f (g x)) (ts-rel(ts1)^*) (f (g y))
BY
{ (RepeatFor 2 (BackThruSomeHyp⋅) THEN xxxBLemma `rel_rel_star`xxx 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)))
14.  ts-init(ts1)  rel\_star(ts-type(ts1);  ts-rel(ts1))  (f  (g  ts-init(ts3)))
15.  x  :  ts-reachable(ts3)
16.  y  :  ts-reachable(ts3)
17.  x  ts-rel(ts3)  y
18.  (g  x  \mmember{}  ts-reachable(ts2))  \mwedge{}  (g  y  \mmember{}  ts-reachable(ts2))
\mvdash{}  (f  (g  x))  rel\_star(ts-type(ts1);  ts-rel(ts1))  (f  (g  y))


By

---

Latex:
(RepeatFor  2  (BackThruSomeHyp\mcdot{})  THEN  xxxBLemma  `rel\_rel\_star`xxx  THEN  Auto)\mcdot{}

---

Home Index