---

{ [Info:Type]
    es:EO+(Info)
      [A,B:Type].
        Ia:EClass(A). Ib:EClass(B). f:E(Ia)  B. g:E(Ib)  E.
          (g glues Ia f Ib
           {Bij(E(Ib);E(Ia);g)
              (e:E(Ib). g e c e)
              (e,e':E(Ib).  (g e loc g e'   e loc e' ))
              (e:E(Ib). ((f (g e)) = Ib(e)))}) }

{ Proof }

---

Definitions occuring in Statement :  glues: g glues Ia f Ib,  es-E-interface: E(X),  eclass-val: X(e),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-causle: e c e',  es-le: e loc e' ,  es-E: E,  biject: Bij(A;B;f),  uall: [x:A]. B[x],  guard: {T},  all: x:A. B[x],  implies: P  Q,  and: P  Q,  apply: f a,  function: x:A  B[x],  universe: Type,  equal: s = t
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  member: t  T,  so_lambda: x y.t[x; y],  so_apply: x[s1;s2],  iff: P  Q,  and: P  Q,  uimplies: b supposing a,  prop: ,  subtype: S  T
Lemmas :  glues-iff,  glues_wf,  es-E-interface_wf,  es-E_wf,  eclass_wf,  event-ordering+_inc,  event-ordering+_wf,  glues-property

---

\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[A,B:Type].
            \mforall{}Ia:EClass(A).  \mforall{}Ib:EClass(B).  \mforall{}f:E(Ia)  {}\mrightarrow{}  B.  \mforall{}g:E(Ib)  {}\mrightarrow{}  E.
                (g  glues  Ia  {}{}f{}\mrightarrow{}  Ib
                {}\mRightarrow{}  \{Bij(E(Ib);E(Ia);g)
                      \mwedge{}  (\mforall{}e:E(Ib).  g  e  c\mleq{}  e)
                      \mwedge{}  (\mforall{}e,e':E(Ib).    (g  e  \mleq{}loc  g  e'    {}\mRightarrow{}  e  \mleq{}loc  e'  ))
                      \mwedge{}  (\mforall{}e:E(Ib).  ((f  (g  e))  =  Ib(e)))\})


Date html generated: 2011_08_16-PM-06_00_56
Last ObjectModification: 2011_06_20-AM-01_43_03

Home Index