Nuprl Lemma : OARcast-deliverhdr
∀[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;deliverhdr;<i1, k, v>)> ∈ OARcast_main(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;order\000Chdr;receivers;senders;mf)(e)
⇐⇒ ↓∃e':{e':E| e' ≤loc e }
∃b:Id List
∃e1:{e1:E| e1 ≤loc e }
∃b1:ℤ List
∃b2:bag(Id)
∃b3:(M × ℕ) List
(loc(e) ↓∈ receivers
∧ (((↑es-info-auth(es;e')) ∧ (header(e') = orderedhdr ∈ Name) ∧ has-es-info-type(es;e';mf;Id × Id × ℤ × M))
∧ b ∈ OARcast_DelivererState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)(e')
∧ (¬(fst(snd(msgval(e'))) ∈ b)))
∧ (((↑es-info-auth(es.e';e1))
∧ (header(e1) = orderedhdr ∈ Name)
∧ has-es-info-type(es;e1;mf;Id × Id × ℤ × M))
∧ b1 ∈ OARcast_DelivererForSenderState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)
(fst(snd(msgval(e'))))(e1)
∧ (¬(fst(snd(snd(msgval(e1)))) ∈ b1)))
∧ <b2, b3> ∈
OARcast_DelivererForSenderSeqState(M;deliverhdr;deqM;oarcasthdr;orderedhdr;orderers;orderhdr;mf)
(fst(snd(msgval(e'))))
(fst(snd(snd(msgval(e1)))))(e)
∧ (↑isl(oarcast-deliver-output((2 * flrs) + 1;<b2, b3>)))
∧ (d = 0 ∈ ℤ)
∧ (i = loc(e) ∈ Id)
∧ auth = ff
∧ (i1 = (fst(snd(msgval(e')))) ∈ Id)
∧ (k = (fst(snd(snd(msgval(e1))))) ∈ ℤ)
∧ (v = outl(oarcast-deliver-output((2 * flrs) + 1;<b2, b3>)) ∈ 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;deliverhdr;<i1
, k
, v>)> \mmember{}
OARcast\_main(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;receivers;...;mf)(e)
\mLeftarrow{}{}\mRightarrow{} \mdownarrow{}\mexists{}e':\{e':E| e' \mleq{}loc e \}
\mexists{}b:Id List
\mexists{}e1:\{e1:E| e1 \mleq{}loc e \}
\mexists{}b1:\mBbbZ{} List
\mexists{}b2:bag(Id)
\mexists{}b3:(M \mtimes{} \mBbbN{}) List
(loc(e) \mdownarrow{}\mmember{} receivers
\mwedge{} (((\muparrow{}es-info-auth(es;e'))
\mwedge{} (header(e') = orderedhdr)
\mwedge{} has-es-info-type(es;e';mf;Id \mtimes{} Id \mtimes{} \mBbbZ{} \mtimes{} M))
\mwedge{} b \mmember{} OARcast\_DelivererState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)(e')
\mwedge{} (\mneg{}(fst(snd(msgval(e'))) \mmember{} b)))
\mwedge{} (((\muparrow{}es-info-auth(es.e';e1))
\mwedge{} (header(e1) = orderedhdr)
\mwedge{} has-es-info-type(es;e1;mf;Id \mtimes{} Id \mtimes{} \mBbbZ{} \mtimes{} M))
\mwedge{} b1 \mmember{}
OARcast\_DelivererForSenderState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)
(fst(snd(msgval(e'))))(e1)
\mwedge{} (\mneg{}(fst(snd(snd(msgval(e1)))) \mmember{} b1)))
\mwedge{} <b2, b3> \mmember{}
OARcast\_DelivererForSenderSeqState(M;deliverhdr;deqM;oarcasthdr;...;...;...;mf)
(fst(snd(msgval(e'))))
(fst(snd(snd(msgval(e1)))))(e)
\mwedge{} (\muparrow{}isl(oarcast-deliver-output((2 * flrs) + 1;<b2, b3>)))
\mwedge{} (d = 0)
\mwedge{} (i = loc(e))
\mwedge{} auth = ff
\mwedge{} (i1 = (fst(snd(msgval(e')))))
\mwedge{} (k = (fst(snd(snd(msgval(e1))))))
\mwedge{} (v = outl(oarcast-deliver-output((2 * flrs) + 1;<b2, b3>)))))
Date html generated:
2015_07_23-PM-05_21_34
Last ObjectModification:
2015_01_29-PM-09_36_26
Home
Index