Nuprl Lemma : eclass1-disjoint-classrel

[Info,A,B,C:Type]. ∀[Y:EClass(A)]. ∀[X:EClass(B)]. ∀[f:Id ─→ B ─→ C]. ∀[es:EO+(Info)].
  (disjoint-classrel(es;B;X;A;Y)  disjoint-classrel(es;C;(f X);A;Y))


Proof




Definitions occuring in Statement :  eclass1: (f X) disjoint-classrel: disjoint-classrel(es;A;X;B;Y) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) Id: Id uall: [x:A]. B[x] implies:  Q function: x:A ─→ B[x] universe: Type
Lemmas :  eclass1-classrel all_wf not_wf classrel_wf eclass1_wf es-E_wf event-ordering+_subtype disjoint-classrel_wf event-ordering+_wf Id_wf eclass_wf
\mforall{}[Info,A,B,C:Type].  \mforall{}[Y:EClass(A)].  \mforall{}[X:EClass(B)].  \mforall{}[f:Id  {}\mrightarrow{}  B  {}\mrightarrow{}  C].  \mforall{}[es:EO+(Info)].
    (disjoint-classrel(es;B;X;A;Y)  {}\mRightarrow{}  disjoint-classrel(es;C;(f  o  X);A;Y))



Date html generated: 2015_07_17-PM-00_36_21
Last ObjectModification: 2015_01_27-PM-11_30_04

Home Index