---

{ [Info:Type]
    es:EO+(Info)
      [A,B:Type].
        Ia:EClass(A). Ib:EClass(B). f:E(Ia)  B. g:E(Ib)  E(Ia).
          (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' ,  biject: Bij(A;B;f),  uall: [x:A]. B[x],  guard: {T},  all: x:A. B[x],  iff: P  Q,  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],  iff: P  Q,  guard: {T},  and: P  Q,  implies: P  Q,  rev_implies: P  Q,  cand: A c B,  member: t  T,  prop: ,  subtype: S  T,  suptype: suptype(S; T),  assert: b,  so_lambda: x y.t[x; y],  btrue: tt,  ifthenelse: if b then t else f fi ,  true: True,  biject: Bij(A;B;f),  inject: Inj(A;B;f),  surject: Surj(A;B;f),  exists: x:A. B[x],  es-E-interface: E(X),  glues: g glues Ia f Ib,  Q-R-glues: g glues Ia:Qa f Ib:Rb,  weak-antecedent-surjection: Q = f== P,  weak-antecedent-function: Q ==f== P,  es-interface-predicate: {I},  Q-R-pre-preserving: f is Q-R-pre-preserving on P,  so_apply: x[s1;s2],  uimplies: b supposing a,  sq_type: SQType(T)
Lemmas :  es-le_wf,  es-E-interface-subtype_rel,  es-E-interface_wf,  glues_wf,  es-E-interface-subtype,  biject_wf,  es-causle_wf,  event-ordering+_inc,  eclass-val_wf,  es-E_wf,  event-ordering+_wf,  subtype_base_sq,  bool_wf,  bool_subtype_base,  eclass_wf,  assert_elim,  in-eclass_wf,  es-interface-top,  assert_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.  \mforall{}g:E(Ib)  {}\mrightarrow{}  E(Ia).
                (g  glues  Ia  {}{}f{}\mrightarrow{}  Ib
                \mLeftarrow{}{}\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_49
Last ObjectModification: 2011_06_20-AM-01_42_54

Home Index