Nuprl Lemma : global-order-pairwise-compat-msg-and-classrel

f:Name ─→ Type. ∀hdrs:Name List. ∀X:EClass(Interface).
  (LocalClass(X)
   (∀LL:(Id × Message(f)) List List
        ((∀L1,L2∈LL.  L1 || L2)
         (∀L∈LL.eo-msg-interface-constraint(global-eo(L);X;hdrs;f))
         (∃G:(Id × Message(f)) List
             (eo-msg-interface-constraint(global-eo(G);X;hdrs;f)
             ∧ (∀L∈LL.∃g:E ─→ E. ∀[e:E]. ∀[v:Interface].  (v ∈ X(e) ⇐⇒ v ∈ X(g e))))))))


Proof




Definitions occuring in Statement :  eo-msg-interface-constraint: eo-msg-interface-constraint(es;X;hdrs;f) msg-interface: Interface Message: Message(f) global-order-compat: L1 || L2 global-eo: global-eo(L) local-class: LocalClass(X) classrel: v ∈ X(e) eclass: EClass(A[eo; e]) es-E: E Id: Id name: Name pairwise: (∀x,y∈L.  P[x; y]) l_all: (∀x∈L.P[x]) list: List uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] iff: ⇐⇒ Q implies:  Q and: P ∧ Q apply: a function: x:A ─→ B[x] product: x:A × B[x] universe: Type
Lemmas :  global-order-pairwise-compat-msg-interface-constraint embedding-preserves-local-class Message_wf msg-interface_wf global-eo_wf select_wf list_wf Id_wf sq_stable__le uall_wf es-E_wf event-ordering+_subtype iff_wf classrel_wf int_seg_wf length_wf eo-msg-interface-constraint_wf l_all_wf2 l_member_wf exists_wf pairwise_wf global-order-compat_wf local-class_wf eclass_wf3 name_wf

Latex:
\mforall{}f:Name  {}\mrightarrow{}  Type.  \mforall{}hdrs:Name  List.  \mforall{}X:EClass(Interface).
    (LocalClass(X)
    {}\mRightarrow{}  (\mforall{}LL:(Id  \mtimes{}  Message(f))  List  List
                ((\mforall{}L1,L2\mmember{}LL.    L1  ||  L2)
                {}\mRightarrow{}  (\mforall{}L\mmember{}LL.eo-msg-interface-constraint(global-eo(L);X;hdrs;f))
                {}\mRightarrow{}  (\mexists{}G:(Id  \mtimes{}  Message(f))  List
                          (eo-msg-interface-constraint(global-eo(G);X;hdrs;f)
                          \mwedge{}  (\mforall{}L\mmember{}LL.\mexists{}g:E  {}\mrightarrow{}  E.  \mforall{}[e:E].  \mforall{}[v:Interface].    (v  \mmember{}  X(e)  \mLeftarrow{}{}\mRightarrow{}  v  \mmember{}  X(g  e))))))))



Date html generated: 2015_07_22-AM-11_59_38
Last ObjectModification: 2015_01_28-AM-08_41_49

Home Index