---

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

{ Proof }

---

Definitions occuring in Statement :  glued: glued(es;B;f;Ia;Ib),  Q-R-glued: Ia:Qa f  Ib:Rb,  es-E-interface: E(X),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-le: e loc e' ,  uall: [x:A]. B[x],  all: x:A. B[x],  iff: P  Q,  lambda: x.A[x],  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  iff: P  Q,  glued: glued(es;B;f;Ia;Ib),  Q-R-glued: Ia:Qa f  Ib:Rb,  and: P  Q,  implies: P  Q,  rev_implies: P  Q,  exists: x:A. B[x],  glues: g glues Ia f Ib,  member: t  T,  so_lambda: x y.t[x; y],  so_apply: x[s1;s2],  prop:
Lemmas :  Q-R-glues_wf,  glued_wf,  glues_wf,  Q-R-glued_wf,  es-le_wf,  es-E_wf,  es-E-interface_wf,  eclass_wf,  event-ordering+_wf

---

\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.
                (glued(es;B;f;Ia;Ib)  \mLeftarrow{}{}\mRightarrow{}  Ia:\mlambda{}e,e'.e  \mleq{}loc  e'    \mrightarrow{}{}f{}\mrightarrow{}    Ib:\mlambda{}e,e'.e  \mleq{}loc  e'  )


Date html generated: 2011_08_16-PM-06_01_11
Last ObjectModification: 2011_06_20-AM-01_44_28

Home Index