---

{ [Info:Type]. [P:es:EO+(Info)  E  ].
    p:es:EO+(Info). e:E.  Dec(P[es;e])
      [A,B:Type].
        Ia:EClass(A). Ib:EClass(B). g:es:EO+(Info)  E(Ib)  E.
        q:es:EO+(Info). e:E.  Dec((e  Ib) c P[es;g es e]).
          ((es:EO+(Info). e:E.  P[es;g es e] supposing e  Ib)
           (es:EO+(Info). f:E(Ia)  B.
                [Q,R:E  E  ].
                  (g es glues (Ia|p):Q f (Ib|q):R
                   g es glues (Ia|p):Q f Ib:R))) }

{ Proof }

---

Definitions occuring in Statement :  Q-R-glues: g glues Ia:Qa f Ib:Rb,  es-interface-restrict: (I|p),  es-E-interface: E(X),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-E: E,  assert: b,  decidable: Dec(P),  uimplies: b supposing a,  uall: [x:A]. B[x],  cand: A c B,  prop: ,  so_apply: x[s1;s2],  all: x:A. B[x],  implies: P  Q,  apply: f a,  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  prop: ,  all: x:A. B[x],  so_apply: x[s1;s2],  es-E-interface: E(X),  cand: A c B,  implies: P  Q,  uimplies: b supposing a,  member: t  T,  so_lambda: x y.t[x; y],  subtype: S  T,  suptype: suptype(S; T),  guard: {T}
Lemmas :  Q-R-glues_wf,  es-interface-restrict_wf,  es-E_wf,  event-ordering+_wf,  assert_wf,  in-eclass_wf,  subtype_rel_function,  es-E-interface_wf,  top_wf,  subtype_rel_self,  decidable_wf,  eclass_wf,  Q-R-glues-trivial-restrict,  es-interface-top,  event-ordering+_inc,  assert_witness,  es-E-interface-restrict

---

\mforall{}[Info:Type].  \mforall{}[P:es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}p:\mforall{}es:EO+(Info).  \mforall{}e:E.    Dec(P[es;e])
        \mforall{}[A,B:Type].
            \mforall{}Ia:EClass(A).  \mforall{}Ib:EClass(B).  \mforall{}g:es:EO+(Info)  {}\mrightarrow{}  E(Ib)  {}\mrightarrow{}  E.  \mforall{}q:\mforall{}es:EO+(Info).  \mforall{}e:E.
                                                                                                                                                Dec((\muparrow{}e  \mmember{}\msubb{}  Ib)
                                                                                                                                                c\mwedge{}  P[es;g  es  e]).
                ((\mforall{}es:EO+(Info).  \mforall{}e:E.    P[es;g  es  e]  supposing  \muparrow{}e  \mmember{}\msubb{}  Ib)
                {}\mRightarrow{}  (\mforall{}es:EO+(Info).  \mforall{}f:E(Ia)  {}\mrightarrow{}  B.
                            \mforall{}[Q,R:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].
                                (g  es  glues  (Ia|p):Q  {}{}f{}\mrightarrow{}  (Ib|q):R  {}\mRightarrow{}  g  es  glues  (Ia|p):Q  {}{}f{}\mrightarrow{}  Ib:R)))


Date html generated: 2011_08_16-PM-05_59_17
Last ObjectModification: 2010_11_10-AM-04_24_31

Home Index