---

Step * 2 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
⊢ (f (g x)) (ts-rel(ts1)^*) (f (g y))
BY
{ (Assert (g x ∈ ts-reachable(ts2)) ∧ (g y ∈ ts-reachable(ts2)) BY
         (D 0
          THEN All (Unfold `ts-reachable`)
          THEN (DVar `x' THEN DVar `y')
          THEN MemTypeCD
          THEN Auto
          THEN (Using [`y',⌜g ts-init(ts3)⌝] (BLemma `rel_star_transitivity`)⋅ THEN Auto)⋅)) }

1
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))

---

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
\mvdash{}  (f  (g  x))  rel\_star(ts-type(ts1);  ts-rel(ts1))  (f  (g  y))


By

---

Latex:
(Assert  (g  x  \mmember{}  ts-reachable(ts2))  \mwedge{}  (g  y  \mmember{}  ts-reachable(ts2))  BY
              (D  0
                THEN  All  (Unfold  `ts-reachable`)
                THEN  (DVar  `x'  THEN  DVar  `y')
                THEN  MemTypeCD
                THEN  Auto
                THEN  (Using  [`y',\mkleeneopen{}g  ts-init(ts3)\mkleeneclose{}]  (BLemma  `rel\_star\_transitivity`)\mcdot{}  THEN  Auto)\mcdot{}))

---

Home Index