---

{ [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))) and 
                      (e:E(Out). (Out(e) = Sys(e))) and 
                      (e:E(In). (Sys(e) = In(e))) and 
                      (e:E(Sys). (Sys(e) = Sys(f e))) and 
                      (e:E(Sys). (e  In  (f e) = e)))) supposing 
                ((E(Out) r E(Sys)) and 
                (E(In) r E(Sys)))) }

{ Proof }

---

Definitions occuring in Statement :  glues: g glues Ia f Ib,  global-order-preserving: global-order-preserving(es;X;f),  es-E-interface: E(X),  eclass-val: X(e),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-fix: f**(e),  es-causle: e c e',  es-loc: loc(e),  es-E: E,  Id: Id,  biject: Bij(A;B;f),  subtype_rel: A r B,  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  all: x:A. B[x],  iff: P  Q,  implies: P  Q,  apply: f a,  lambda: x.A[x],  function: x:A  B[x],  universe: Type,  equal: s = t
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  uimplies: b supposing a,  iff: P  Q,  assert: b,  member: t  T,  and: P  Q,  rev_implies: P  Q,  prop: ,  so_lambda: x y.t[x; y],  btrue: tt,  ifthenelse: if b then t else f fi ,  true: True,  es-E-interface: E(X),  guard: {T},  so_apply: x[s1;s2],  top: Top,  squash: T,  sq_type: SQType(T),  strong-interface-fifo: strong-interface-fifo(es;X;f),  subtype: S  T
Lemmas :  assert_wf,  in-eclass_wf,  es-interface-top,  assert_witness,  es-E_wf,  event-ordering+_inc,  es-E-interface-subtype_rel,  es-E-interface_wf,  Id_wf,  es-loc_wf,  eclass-val_wf,  event-ordering+_wf,  subtype_base_sq,  bool_subtype_base,  es-interface-val_wf2,  iff_wf,  global-order-preserving_wf,  es-causle_wf,  eclass_wf,  assert_elim,  es-fix_wf2,  es-fix_property,  es-fix-order-preserving,  strong-interface-fifo-order-preserving,  biject_wf,  bool_wf,  glues-iff,  es-fix-causle,  fun-connected-induction,  fun-connected_wf,  not_wf,  es-interface-subtype_rel2,  top_wf,  squash_wf

---

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


Date html generated: 2011_08_16-PM-06_10_29
Last ObjectModification: 2011_06_20-AM-01_48_53

Home Index