Nuprl Lemma : glued-composes

[Info:Type]
  ∀es:EO+(Info)
    ∀[A,B,C:Type].
      ∀Ia:EClass(A). ∀Ib:EClass(B). ∀Ic:EClass(C). ∀f1:E(Ia) ─→ B. ∀f2:B ─→ C.
        ((glued(es;B;f1;Ia;Ib) ∧ glued(es;C;λe.(f2 Ib(e));Ib;Ic))  glued(es;C;f2 f1;Ia;Ic))


Proof




Definitions occuring in Statement :  glued: glued(es;B;f;Ia;Ib) es-E-interface: E(X) eclass-val: X(e) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) compose: g uall: [x:A]. B[x] all: x:A. B[x] implies:  Q and: P ∧ Q apply: a lambda: λx.A[x] function: x:A ─→ B[x] universe: Type
Lemmas :  glued_wf eclass-val_wf es-E_wf event-ordering+_subtype event-ordering+_wf assert_elim in-eclass_wf subtype_base_sq bool_wf bool_subtype_base es-E-interface_wf es-interface-subtype_rel2 top_wf eclass_wf glues-property compose_wf glues_wf glue-composes

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[A,B,C:Type].
            \mforall{}Ia:EClass(A).  \mforall{}Ib:EClass(B).  \mforall{}Ic:EClass(C).  \mforall{}f1:E(Ia)  {}\mrightarrow{}  B.  \mforall{}f2:B  {}\mrightarrow{}  C.
                ((glued(es;B;f1;Ia;Ib)  \mwedge{}  glued(es;C;\mlambda{}e.(f2  Ib(e));Ib;Ic))  {}\mRightarrow{}  glued(es;C;f2  o  f1;Ia;Ic))



Date html generated: 2015_07_21-PM-04_15_43
Last ObjectModification: 2015_01_27-PM-05_46_35

Home Index