Nuprl Lemma : local-simulation-agreement

∀correct:Id ⟶ ℙ. ∀g,f:Name ⟶ Type. ∀X:EClass(Interface).
  (LocalClass(X)
  ⇒ (∀locs:bag(Id). ∀hdr:Name.
        ∀hdrs:Name List. ∀R:Interface ⟶ Interface ⟶ ℙ. ∀es:EO+(Message(f)).
          ((∀i,j:Id.  ((correct i) ⇒ (correct j) ⇒ local-simulation-input-consistency(g;X;hdr;locs;es;i;j)))
          ⇒ (∀i:Id. ((correct i) ⇒ local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)))
          ⇒ (∀eo:EO+(Message(g)). (eo-msg-interface-constraint(eo;X;hdrs;g) ⇒ any v1,v2 from X satisfy R[v1;v2]))
          ⇒ any v1,v2 from local-simulation-class(X;locs;hdr) satisfy
             R[v1;v2]
             at locations i.correct i) 
        supposing hdr encodes Id × Message(g)))


Proof



Definitions occuring in Statement :  local-simulation-input-consistency: local-simulation-input-consistency(g;X;hdr;locs;es;i;j),  local-simulation-input-validity: local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i),  eo-msg-interface-constraint: eo-msg-interface-constraint(es;X;hdrs;f),  msg-interface: Interface,  local-simulation-class: local-simulation-class(X;locs;hdr),  encodes-msg-type: hdr encodes T,  Message: Message(f),  local-class: LocalClass(X),  correct-consistent-class: correct-consistent-class,  consistent-class: consistent-class,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  Id: Id,  name: Name,  list: T List,  uimplies: b supposing a,  prop: ℙ,  so_apply: x[s1;s2],  all: ∀x:A. B[x],  implies: P ⇒ Q,  apply: f a,  function: x:A ⟶ B[x],  product: x:A × B[x],  universe: Type,  bag: bag(T)
Definitions unfolded in proof :  all: ∀x:A. B[x],  member: t ∈ T,  implies: P ⇒ Q,  uimplies: b supposing a,  encodes-msg-type: hdr encodes T,  subtype_rel: A ⊆r B,  uall: ∀[x:A]. B[x],  correct-consistent-class: correct-consistent-class,  so_lambda: λ2x y.t[x; y],  prop: ℙ,  so_lambda: λ2x.t[x],  so_apply: x[s],  so_apply: x[s1;s2],  iff: P ⇐⇒ Q,  and: P ∧ Q,  rev_implies: P ⇐ Q,  cand: A c∧ B,  top: Top,  true: True,  local-simulation-input-consistency: local-simulation-input-consistency(g;X;hdr;locs;es;i;j),  label: ...$L... t,  guard: {T},  exists: ∃x:A. B[x],  consistent-class: consistent-class
Latex:
\mforall{}correct:Id  {}\mrightarrow{}  \mBbbP{}.  \mforall{}g,f:Name  {}\mrightarrow{}  Type.  \mforall{}X:EClass(Interface).
    (LocalClass(X)
    {}\mRightarrow{}  (\mforall{}locs:bag(Id).  \mforall{}hdr:Name.
                \mforall{}hdrs:Name  List.  \mforall{}R:Interface  {}\mrightarrow{}  Interface  {}\mrightarrow{}  \mBbbP{}.  \mforall{}es:EO+(Message(f)).
                    ((\mforall{}i,j:Id.
                            ((correct  i)
                            {}\mRightarrow{}  (correct  j)
                            {}\mRightarrow{}  local-simulation-input-consistency(g;X;hdr;locs;es;i;j)))
                    {}\mRightarrow{}  (\mforall{}i:Id.  ((correct  i)  {}\mRightarrow{}  local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)))
                    {}\mRightarrow{}  (\mforall{}eo:EO+(Message(g))
                                (eo-msg-interface-constraint(eo;X;hdrs;g)  {}\mRightarrow{}  any  v1,v2  from  X  satisfy  R[v1;v2]))
                    {}\mRightarrow{}  any  v1,v2  from  local-simulation-class(X;locs;hdr)  satisfy
                          R[v1;v2]
                          at  locations  i.correct  i) 
                supposing  hdr  encodes  Id  \mtimes{}  Message(g)))


Date html generated: 2016_05_17-AM-09_14_19
Last ObjectModification: 2015_12_29-PM-04_10_48

Theory : classrel!lemmas


Home Index