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

.....subterm..... T:t
2:n
1. Info Type
2. es EO+(Info)@i'
3. Type
4. Sys EClass(A)@i'
5. In EClass(A)@i'
6. Out EClass(A)@i'
7. E(Sys) ⟶ E(Sys)@i
8. ∀x:E(Sys). c≤ x@i
9. E(In) ⊆E(Sys)
10. E(Out) ⊆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))
21. ∀e1,e2:E(Sys).  (e1 is f*(e2)  (Sys(e1) Sys(e2) ∈ A))
22. E(Out)@i
23. Sys(f**(e)) Sys(e) ∈ A
⊢ In(f**(e)) Sys(f**(e)) ∈ A
BY
InstHyp [⌜f**(e)⌝14⋅ }

1
.....wf..... 
1. Info Type
2. es EO+(Info)@i'
3. Type
4. Sys EClass(A)@i'
5. In EClass(A)@i'
6. Out EClass(A)@i'
7. E(Sys) ⟶ E(Sys)@i
8. ∀x:E(Sys). c≤ x@i
9. E(In) ⊆E(Sys)
10. E(Out) ⊆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))
21. ∀e1,e2:E(Sys).  (e1 is f*(e2)  (Sys(e1) Sys(e2) ∈ A))
22. E(Out)@i
23. Sys(f**(e)) Sys(e) ∈ A
⊢ f**(e) ∈ E(In)

2
1. Info Type
2. es EO+(Info)@i'
3. Type
4. Sys EClass(A)@i'
5. In EClass(A)@i'
6. Out EClass(A)@i'
7. E(Sys) ⟶ E(Sys)@i
8. ∀x:E(Sys). c≤ x@i
9. E(In) ⊆E(Sys)
10. E(Out) ⊆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))
21. ∀e1,e2:E(Sys).  (e1 is f*(e2)  (Sys(e1) Sys(e2) ∈ A))
22. E(Out)@i
23. Sys(f**(e)) Sys(e) ∈ A
24. Sys(f**(e)) In(f**(e)) ∈ A
⊢ In(f**(e)) Sys(f**(e)) ∈ A


Latex:


Latex:
.....subterm.....  T:t
2:n
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)
18.  Bij(E(Out);E(In);\mlambda{}e.f**(e))@i
19.  interface-order-preserving(es;Sys;\mlambda{}e.f**(e))
20.  strong-interface-fifo(es;Sys;\mlambda{}e.f**(e))
21.  \mforall{}e1,e2:E(Sys).    (e1  is  f*(e2)  {}\mRightarrow{}  (Sys(e1)  =  Sys(e2)))
22.  e  :  E(Out)@i
23.  Sys(f**(e))  =  Sys(e)
\mvdash{}  In(f**(e))  =  Sys(f**(e))


By


Latex:
InstHyp  [\mkleeneopen{}f**(e)\mkleeneclose{}]  14\mcdot{}




Home Index