---

Step * of Lemma ts-refinement-composition

∀ts1,ts2,ts3:transition-system{i:l}. ∀g:ts-type(ts3) ⟶ ts-type(ts2). ∀f:ts-type(ts2) ⟶ ts-type(ts1).
  (ts-refinement(ts1;ts2;f) ⇒ ts-refinement(ts2;ts3;g) ⇒ ts-refinement(ts1;ts3;f o g))
BY
{ xxx(Auto
      THEN All (Unfold `ts-refinement`)
      THEN (Assert (∀x,y:ts-reachable(ts2).  ((x (ts-rel(ts2)^*) y) ⇒ ((f x) (ts-rel(ts1)^*) (f y))))
                  ∧ (∀x,y:ts-reachable(ts3).  ((x (ts-rel(ts3)^*) y) ⇒ ((g x) (ts-rel(ts2)^*) (g y)))) BY
                  (All (Unfold `ts-reachable`) THEN D 0 THEN BLemma `rel-preserving-star-reachable`⋅ THEN Auto))
      THEN Reduce 0
      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)))
⊢ ts-init(ts1) (ts-rel(ts1)^*) (f (g ts-init(ts3)))

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

3
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
⊢ ∃y:ts-reachable(ts3). ((ts-final(ts3) y) ∧ ((f (g y)) = x ∈ ts-type(ts1)))

---

Latex:

---

Latex:
\mforall{}ts1,ts2,ts3:transition-system\{i:l\}.  \mforall{}g:ts-type(ts3)  {}\mrightarrow{}  ts-type(ts2).
\mforall{}f:ts-type(ts2)  {}\mrightarrow{}  ts-type(ts1).
    (ts-refinement(ts1;ts2;f)  {}\mRightarrow{}  ts-refinement(ts2;ts3;g)  {}\mRightarrow{}  ts-refinement(ts1;ts3;f  o  g))


By

---

Latex:
xxx(Auto
        THEN  All  (Unfold  `ts-refinement`)
        THEN  (Assert  (\mforall{}x,y:ts-reachable(ts2).    ((x  (ts-rel(ts2)\^{}*)  y)  {}\mRightarrow{}  ((f  x)  (ts-rel(ts1)\^{}*)  (f  y))))
                                \mwedge{}  (\mforall{}x,y:ts-reachable(ts3).
                                          ((x  (ts-rel(ts3)\^{}*)  y)  {}\mRightarrow{}  ((g  x)  (ts-rel(ts2)\^{}*)  (g  y))))  BY
                                (All  (Unfold  `ts-reachable`)
                                  THEN  D  0
                                  THEN  BLemma  `rel-preserving-star-reachable`\mcdot{}
                                  THEN  Auto))
        THEN  Reduce  0
        THEN  Auto)xxx

---

Home Index