Step
*
2
1
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)
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
BY
{ ((BLemma `glues-iff` THENA Auto) THEN Reduce 0 THEN SplitAndConcl) }
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))
⊢ Bij(E(Out);E(In);λe.f**(e))
2
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:E(Out). f**(e) c≤ e
3
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,e':E(Out). (f**(e) ≤loc f**(e') ⇒ e ≤loc e' )
4
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:E(Out). (In(f**(e)) = Out(e) ∈ A)
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)
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))
\mvdash{} \mlambda{}e.f**(e) glues In {}{}\mlambda{}e.In(e){}\mrightarrow{} Out
By
Latex:
((BLemma `glues-iff` THENA Auto) THEN Reduce 0 THEN SplitAndConcl)
Home
Index