Nuprl Lemma : OARcast-orderhdr
∀[M:{T:Type| valueall-type(T)} ]. ∀[deliverhdr:Atom List]. ∀[deqM:EqDecider(M)]. ∀[flrs:ℤ].
∀[oarcasthdr,orderedhdr:Atom List]. ∀[orderers:bag(Id)]. ∀[orderhdr:Atom List]. ∀[receivers,senders:bag(Id)].
∀[mf:OARcast_headers_type{i:l}(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr)]. ∀[es:EO+(Message(mf))]. ∀[e:E]. ∀[d:ℤ].
∀[i:Id]. ∀[auth:𝔹]. ∀[i1:Id]. ∀[k:ℤ]. ∀[v:M].
(<d, i, mk-msg(auth;orderhdr;<i1, k, v>)> ∈ OARcast_main(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhd\000Cr;receivers;senders;mf)(e)
⇐⇒ loc(e) ↓∈ senders
∧ ((header(e) = oarcasthdr ∈ Name) ∧ has-es-info-type(es;e;mf;M))
∧ i ↓∈ orderers
∧ (d = 0 ∈ ℤ)
∧ auth = tt
∧ (i1 = loc(e) ∈ Id)
∧ (k = OARcast_SenderStateFun(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf;es;e) ∈ ℤ)
∧ (v = msgval(e) ∈ M))
Error : references
Latex:
\mforall{}[M:\{T:Type| valueall-type(T)\} ]. \mforall{}[deliverhdr:Atom List]. \mforall{}[deqM:EqDecider(M)]. \mforall{}[flrs:\mBbbZ{}].
\mforall{}[oarcasthdr,orderedhdr:Atom List]. \mforall{}[orderers:bag(Id)]. \mforall{}[orderhdr:Atom List].
\mforall{}[receivers,senders:bag(Id)].
\mforall{}[mf:OARcast\_headers\_type\{i:l\}(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr)].
\mforall{}[es:EO+(Message(mf))]. \mforall{}[e:E]. \mforall{}[d:\mBbbZ{}]. \mforall{}[i:Id]. \mforall{}[auth:\mBbbB{}]. \mforall{}[i1:Id]. \mforall{}[k:\mBbbZ{}]. \mforall{}[v:M].
(<d
, i
, mk-msg(auth;orderhdr;<i1
, k
, v>)> \mmember{}
OARcast\_main(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;receivers;...;mf)(e)
\mLeftarrow{}{}\mRightarrow{} loc(e) \mdownarrow{}\mmember{} senders
\mwedge{} ((header(e) = oarcasthdr) \mwedge{} has-es-info-type(es;e;mf;M))
\mwedge{} i \mdownarrow{}\mmember{} orderers
\mwedge{} (d = 0)
\mwedge{} auth = tt
\mwedge{} (i1 = loc(e))
\mwedge{} (k = OARcast\_SenderStateFun(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf;es;e))
\mwedge{} (v = msgval(e)))
Date html generated:
2015_07_23-PM-05_21_26
Last ObjectModification:
2015_01_29-PM-09_36_25
Home
Index