---

Step * 2 of Lemma glues-via-flow-lemma1


1. [Info] : Type
2. es : EO+(Info)@i'
3. [A] : Type
4. Sys : EClass(A)@i'
5. In : EClass(A)@i'
6. Out : EClass(A)@i'
7. f : E(Sys) ─→ E(Sys)@i
8. ∀x:E(Sys). f x c≤ x@i
9. E(In) ⊆r E(Sys)
10. E(Out) ⊆r E(Sys)
11. global-order-preserving(es;Sys;f)@i
12. ∀e:E(Sys). (↑e ∈b In ⇐⇒ (f e) = e ∈ E)
13. ∀e:E(Sys). (Sys(e) = Sys(f e) ∈ A)
14. ∀e:E(In). (Sys(e) = In(e) ∈ A)
15. ∀e:E(Out). (Out(e) = Sys(e) ∈ A)
16. ∀e1,e2:E(Out).  (loc(e1) = loc(e2) ∈ Id)
17. λe.f**(e) ∈ E(Out) ─→ E(In)
⊢ Bij(E(Out);E(In);λe.f**(e)) ⇒ λe.f**(e) glues In ──λe.In(e)─→ Out
BY
{ ((D 0 THENA Auto)
   THEN OnMaybeHyp 10 (\h. (((FLemma `es-fix-order-preserving` [h]) THENA Auto)
                            THEN ((FLemma `strong-interface-fifo-order-preserving` [-1])
                                  THENA (Try (Complete (Auto))
                                         THEN (MemCD THENA Auto)
                                         THEN SubsumeC ⌈E(Sys)⌉⋅
                                         THEN Auto)
                                  )
                            ))
   ) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. [A] : Type
4. Sys : EClass(A)@i'
5. In : EClass(A)@i'
6. Out : EClass(A)@i'
7. f : E(Sys) ─→ E(Sys)@i
8. ∀x:E(Sys). f x c≤ x@i
9. E(In) ⊆r E(Sys)
10. E(Out) ⊆r E(Sys)
11. global-order-preserving(es;Sys;f)@i
12. ∀e:E(Sys). (↑e ∈b In ⇐⇒ (f e) = e ∈ E)
13. ∀e:E(Sys). (Sys(e) = Sys(f e) ∈ A)
14. ∀e:E(In). (Sys(e) = In(e) ∈ A)
15. ∀e:E(Out). (Out(e) = Sys(e) ∈ A)
16. ∀e1,e2:E(Out).  (loc(e1) = loc(e2) ∈ Id)
17. λe.f**(e) ∈ E(Out) ─→ E(In)
18. Bij(E(Out);E(In);λe.f**(e))@i
19. interface-order-preserving(es;Sys;λe.f**(e))
20. strong-interface-fifo(es;Sys;λe.f**(e))
⊢ λe.f**(e) glues In ──λe.In(e)─→ Out

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  [A]  :  Type
4.  Sys  :  EClass(A)@i'
5.  In  :  EClass(A)@i'
6.  Out  :  EClass(A)@i'
7.  f  :  E(Sys)  {}\mrightarrow{}  E(Sys)@i
8.  \mforall{}x:E(Sys).  f  x  c\mleq{}  x@i
9.  E(In)  \msubseteq{}r  E(Sys)
10.  E(Out)  \msubseteq{}r  E(Sys)
11.  global-order-preserving(es;Sys;f)@i
12.  \mforall{}e:E(Sys).  (\muparrow{}e  \mmember{}\msubb{}  In  \mLeftarrow{}{}\mRightarrow{}  (f  e)  =  e)
13.  \mforall{}e:E(Sys).  (Sys(e)  =  Sys(f  e))
14.  \mforall{}e:E(In).  (Sys(e)  =  In(e))
15.  \mforall{}e:E(Out).  (Out(e)  =  Sys(e))
16.  \mforall{}e1,e2:E(Out).    (loc(e1)  =  loc(e2))
17.  \mlambda{}e.f**(e)  \mmember{}  E(Out)  {}\mrightarrow{}  E(In)
\mvdash{}  Bij(E(Out);E(In);\mlambda{}e.f**(e))  {}\mRightarrow{}  \mlambda{}e.f**(e)  glues  In  {}{}\mlambda{}e.In(e){}\mrightarrow{}  Out


By

---

Latex:
((D  0  THENA  Auto)
  THEN  OnMaybeHyp  10  (\mbackslash{}h.  (((FLemma  `es-fix-order-preserving`  [h])  THENA  Auto)
                                                    THEN  ((FLemma  `strong-interface-fifo-order-preserving`  [-1])
                                                                THENA  (Try  (Complete  (Auto))
                                                                              THEN  (MemCD  THENA  Auto)
                                                                              THEN  SubsumeC  \mkleeneopen{}E(Sys)\mkleeneclose{}\mcdot{}
                                                                              THEN  Auto)
                                                                )
                                                    ))
  )

---

Home Index