---

Step * of Lemma glues-via-flow-lemma1

∀[Info:Type]
  ∀es:EO+(Info)
    ∀[A:Type]
      ∀Sys,In,Out:EClass(A). ∀f:E(Sys) ⟶ E(Sys).
        ((∀x:E(Sys). f x c≤ x)
        ⇒ (global-order-preserving(es;Sys;f)
              ⇒ (Bij(E(Out);E(In);λe.f**(e)) ⇒ λe.f**(e) glues In ──λe.In(e)⟶ Out) supposing 
                    ((∀e1,e2:E(Out).  (loc(e1) = loc(e2) ∈ Id)) and 
                    (∀e:E(Out). (Out(e) = Sys(e) ∈ A)) and 
                    (∀e:E(In). (Sys(e) = In(e) ∈ A)) and 
                    (∀e:E(Sys). (Sys(e) = Sys(f e) ∈ A)) and 
                    (∀e:E(Sys). (↑e ∈b In ⇐⇒ (f e) = e ∈ E)))) supposing 
              ((E(Out) ⊆r E(Sys)) and 
              (E(In) ⊆r E(Sys))))
BY
{ (RepeatFor 16 ((D 0 THENA Auto)) THEN Assert ⌜λe.f**(e) ∈ E(Out) ⟶ E(In)⌝⋅) }

1
.....assertion..... 
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)
⊢ λe.f**(e) ∈ E(Out) ⟶ E(In)

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)
⊢ Bij(E(Out);E(In);λe.f**(e)) ⇒ λe.f**(e) glues In ──λe.In(e)⟶ Out

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[A:Type]
            \mforall{}Sys,In,Out:EClass(A).  \mforall{}f:E(Sys)  {}\mrightarrow{}  E(Sys).
                ((\mforall{}x:E(Sys).  f  x  c\mleq{}  x)
                {}\mRightarrow{}  (global-order-preserving(es;Sys;f)
                            {}\mRightarrow{}  (Bij(E(Out);E(In);\mlambda{}e.f**(e))  {}\mRightarrow{}  \mlambda{}e.f**(e)  glues  In  {}{}\mlambda{}e.In(e){}\mrightarrow{}  Out)  supposing 
                                        ((\mforall{}e1,e2:E(Out).    (loc(e1)  =  loc(e2)))  and 
                                        (\mforall{}e:E(Out).  (Out(e)  =  Sys(e)))  and 
                                        (\mforall{}e:E(In).  (Sys(e)  =  In(e)))  and 
                                        (\mforall{}e:E(Sys).  (Sys(e)  =  Sys(f  e)))  and 
                                        (\mforall{}e:E(Sys).  (\muparrow{}e  \mmember{}\msubb{}  In  \mLeftarrow{}{}\mRightarrow{}  (f  e)  =  e))))  supposing 
                            ((E(Out)  \msubseteq{}r  E(Sys))  and 
                            (E(In)  \msubseteq{}r  E(Sys))))


By

---

Latex:
(RepeatFor  16  ((D  0  THENA  Auto))  THEN  Assert  \mkleeneopen{}\mlambda{}e.f**(e)  \mmember{}  E(Out)  {}\mrightarrow{}  E(In)\mkleeneclose{}\mcdot{})

---

Home Index