Nuprl Lemma : local-simulation-validity2

∀correct:Id ⟶ ℙ. ∀g,f:Name ⟶ Type. ∀X:EClass(Interface).
  (LocalClass(X)
  ⇒ (∀locs:bag(Id). ∀hdr:Name.
        ∀hdrs:Name List. ∀es:EO+(Message(f)).
          ((∀i:Id. ((correct i) ⇒ local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)))
          ⇒ (∀R:Interface ⟶ Message(g) ⟶ ℙ. ∀R':Interface ⟶ Message(f) ⟶ ℙ.
                ((∀eo:EO+(Message(g))
                    (eo-msg-interface-constraint(eo;X;hdrs;g)
                    ⇒ for every v in X there is an
                       earlier event  with info=m such that
                       R[v;m]))
                ⇒ (∀e:E. ∀v:Interface.
                      ((correct loc(e))
                      ⇒ (↑has-header-and-in-locs(info(e);hdr;locs))
                      ⇒ R[v;snd(msg-body(info(e)))]
                      ⇒ (↓∃e':E. ((e' < e) ∧ R'[v;info(e')]))))
                ⇒ for every v in local-simulation-class(X;locs;hdr) at location i s.t. correct i
                   there is an earlier event with info=m  such that R'[v;m]))) 
        supposing hdr encodes Id × Message(g)))


Proof



Definitions occuring in Statement :  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,  has-header-and-in-locs: has-header-and-in-locs(msg;hdr;locs),  local-simulation-class: local-simulation-class(X;locs;hdr),  encodes-msg-type: hdr encodes T,  msg-body: msg-body(msg),  Message: Message(f),  local-class: LocalClass(X),  correct-causal-class-relation: for every a in X at location i s.t. Correct[i] there is an earlier event with info=b  such that R[a; b],  causal-class-relation: causal-class-relation,  eclass: EClass(A[eo; e]),  es-info: info(e),  event-ordering+: EO+(Info),  es-causl: (e < e'),  es-loc: loc(e),  es-E: E,  Id: Id,  name: Name,  list: T List,  assert: ↑b,  uimplies: b supposing a,  prop: ℙ,  so_apply: x[s1;s2],  pi2: snd(t),  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  squash: ↓T,  implies: P ⇒ Q,  and: 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,  so_lambda: λ2x.t[x],  uall: ∀[x:A]. B[x],  so_apply: x[s1;s2],  so_apply: x[s],  causal-class-relation: causal-class-relation,  and: P ∧ Q,  exists: ∃x:A. B[x],  prop: ℙ,  subtype_rel: A ⊆r B,  encodes-msg-type: hdr encodes T,  guard: {T},  top: Top,  iff: P ⇐⇒ Q,  msg-type: msg-type(msg;f),  rev_implies: P ⇐ Q,  so_lambda: λ2x y.t[x; y],  label: ...$L... t,  correct-causal-class-relation: for every a in X at location i s.t. Correct[i] there is an earlier event with info=b  such that R[a; b],  true: True,  squash: ↓T,  es-locl: (e <loc e'),  cand: A c∧ B
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{}es:EO+(Message(f)).
                    ((\mforall{}i:Id.  ((correct  i)  {}\mRightarrow{}  local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)))
                    {}\mRightarrow{}  (\mforall{}R:Interface  {}\mrightarrow{}  Message(g)  {}\mrightarrow{}  \mBbbP{}.  \mforall{}R':Interface  {}\mrightarrow{}  Message(f)  {}\mrightarrow{}  \mBbbP{}.
                                ((\mforall{}eo:EO+(Message(g))
                                        (eo-msg-interface-constraint(eo;X;hdrs;g)
                                        {}\mRightarrow{}  for  every  v  in  X  there  is  an
                                              earlier  event    with  info=m  such  that
                                              R[v;m]))
                                {}\mRightarrow{}  (\mforall{}e:E.  \mforall{}v:Interface.
                                            ((correct  loc(e))
                                            {}\mRightarrow{}  (\muparrow{}has-header-and-in-locs(info(e);hdr;locs))
                                            {}\mRightarrow{}  R[v;snd(msg-body(info(e)))]
                                            {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E.  ((e'  <  e)  \mwedge{}  R'[v;info(e')]))))
                                {}\mRightarrow{}  for  every  v  in  local-simulation-class(X;locs;hdr)  at  location  i  s.t.  correct  i
                                      there  is  an  earlier  event  with  info=m    such  that  R'[v;m]))) 
                supposing  hdr  encodes  Id  \mtimes{}  Message(g)))


Date html generated: 2016_05_17-AM-09_14_38
Last ObjectModification: 2016_01_17-PM-11_14_49

Theory : classrel!lemmas


Home Index