---

Step * 3 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,y:ts-reachable(ts3).  ((x ts-rel(ts3) y) ⇒ ((f (g x)) (ts-rel(ts1)^*) (f (g y))))
16. x : ts-reachable(ts1)
17. ts-final(ts1) x
18. y : ts-reachable(ts2)
19. ts-final(ts2) y
20. (f y) = x ∈ ts-type(ts1)
⊢ ∃y:ts-reachable(ts3). ((ts-final(ts3) y) ∧ ((f (g y)) = x ∈ ts-type(ts1)))
BY
{ xxx(Assert ∃z:ts-reachable(ts3). ((ts-final(ts3) z) ∧ ((g z) = y ∈ ts-type(ts2))) BY
            (BackThruSomeHyp THEN Auto))xxx }

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,y:ts-reachable(ts3).  ((x ts-rel(ts3) y) ⇒ ((f (g x)) (ts-rel(ts1)^*) (f (g y))))
16. x : ts-reachable(ts1)
17. ts-final(ts1) x
18. y : ts-reachable(ts2)
19. ts-final(ts2) y
20. (f y) = x ∈ ts-type(ts1)
21. ∃z:ts-reachable(ts3). ((ts-final(ts3) z) ∧ ((g z) = y ∈ ts-type(ts2)))
⊢ ∃y:ts-reachable(ts3). ((ts-final(ts3) y) ∧ ((f (g y)) = x ∈ ts-type(ts1)))

---

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.  \mforall{}x,y:ts-reachable(ts3).
            ((x  ts-rel(ts3)  y)  {}\mRightarrow{}  ((f  (g  x))  (ts-rel(ts1)\^{}*)  (f  (g  y))))
16.  x  :  ts-reachable(ts1)
17.  ts-final(ts1)  x
18.  y  :  ts-reachable(ts2)
19.  ts-final(ts2)  y
20.  (f  y)  =  x
\mvdash{}  \mexists{}y:ts-reachable(ts3).  ((ts-final(ts3)  y)  \mwedge{}  ((f  (g  y))  =  x))


By

---

Latex:
xxx(Assert  \mexists{}z:ts-reachable(ts3).  ((ts-final(ts3)  z)  \mwedge{}  ((g  z)  =  y))  BY
                    (BackThruSomeHyp  THEN  Auto))xxx

---

Home Index