---

{ [Info:Type]
    es:EO+(Info)
      [R:E  E  ]. [A,B:Type].
        Ia:EClass(A). Ib:EClass(B). f:E(Ia)  B.
          [Q1,Q2:E  E  ].
            g:E(Ib)  E
              (Q1  Q2
               (g glues Ia:Q1 f Ib:R  g glues Ia:Q2 f Ib:R)) }

{ Proof }

---

Definitions occuring in Statement :  Q-R-glues: g glues Ia:Qa f Ib:Rb,  es-E-interface: E(X),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-E: E,  uall: [x:A]. B[x],  prop: ,  all: x:A. B[x],  iff: P  Q,  implies: P  Q,  function: x:A  B[x],  universe: Type,  rel_equivalent: R1  R2
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  prop: ,  implies: P  Q,  iff: P  Q,  Q-R-glues: g glues Ia:Qa f Ib:Rb,  and: P  Q,  rev_implies: P  Q,  cand: A c B,  member: t  T,  subtype: S  T,  suptype: suptype(S; T),  so_lambda: x y.t[x; y],  es-interface-predicate: {I},  exists: x:A. B[x],  predicate_rev_implies: P1  P2,  rel_rev_implies: R1  R2,  rel_equivalent: R1  R2,  label: ...$L... t,  es-E-interface: E(X),  squash: T,  true: True,  so_apply: x[s1;s2],  guard: {T},  uimplies: b supposing a,  sq_stable: SqStable(P)
Lemmas :  Q-R-glues_wf,  rel_equivalent_wf,  es-E-interface_wf,  es-E-interface-subtype,  es-E_wf,  eclass_wf,  event-ordering+_wf,  es-interface-top,  event-ordering+_inc,  es-interface-predicate_wf,  Q-R-pre-preserving_functionality_wrt_implies,  predicate_implies_weakening,  predicate_equivalent_weakening,  rel_implies_weakening,  rel_equivalent_inversion,  rel_equivalent_weakening,  weak-antecedent-surjection-property,  assert_wf,  in-eclass_wf,  sq_stable__assert

---

\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[R:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[A,B:Type].
            \mforall{}Ia:EClass(A).  \mforall{}Ib:EClass(B).  \mforall{}f:E(Ia)  {}\mrightarrow{}  B.
                \mforall{}[Q1,Q2:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].
                    \mforall{}g:E(Ib)  {}\mrightarrow{}  E.  (Q1  \mLeftarrow{}{}\mRightarrow{}  Q2  {}\mRightarrow{}  (g  glues  Ia:Q1  {}{}f{}\mrightarrow{}  Ib:R  \mLeftarrow{}{}\mRightarrow{}  g  glues  Ia:Q2  {}{}f{}\mrightarrow{}  Ib:R))


Date html generated: 2011_08_16-PM-05_57_27
Last ObjectModification: 2011_06_20-AM-01_40_17

Home Index