Nuprl Lemma : OARcast-ilf
∀[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]. ∀[m:Message(mf)].
{<d, i, m> ∈ OARcast_main(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;receivers;senders;mf)(e)
⇐⇒ ↓((∃e':{e':E| e' ≤loc e }
∃b:Id List
∃b2:(ℤ × M) List
∃b4:ℤ
∃b5:(ℤ × M) List
∃v1:ℤ
∃v2:M
(loc(e) ↓∈ orderers
∧ (((↑es-info-auth(es;e')) ∧ (header(e') = orderhdr ∈ Name) ∧ has-es-info-type(es;e';mf;Id × ℤ × M))
∧ b ∈ OARcast_OrdererState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)(e')
∧ (¬(fst(msgval(e')) ∈ b)))
∧ <b2, b4, b5> ∈ OARcast_OrdererForSenderState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)
(fst(msgval(e')))(e)
∧ <v1, v2> ↓∈ b2
∧ (d = 0 ∈ ℤ)
∧ (m = make-Authentic-Msg(orderedhdr;<loc(e), fst(msgval(e')), v1, v2>) ∈ Message(mf))
∧ i ↓∈ receivers))
∨ (∃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)
∧ (m
= make-Msg(deliverhdr;<fst(snd(msgval(e')))
, fst(snd(snd(msgval(e1))))
, outl(oarcast-deliver-output((2 * flrs) + 1;<b2, b3>))>)
∈ Message(mf)))))
∨ (loc(e) ↓∈ senders
∧ ((header(e) = oarcasthdr ∈ Name) ∧ has-es-info-type(es;e;mf;M))
∧ i ↓∈ orderers
∧ (d = 0 ∈ ℤ)
∧ (m
= make-Authentic-Msg(orderhdr;<loc(e)
, OARcast_SenderStateFun(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf;es;e)
, msgval(e)>)
∈ Message(mf)))}
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{}[m:Message(mf)].
\{<d, i, m> \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{}b2:(\mBbbZ{} \mtimes{} M) List
\mexists{}b4:\mBbbZ{}
\mexists{}b5:(\mBbbZ{} \mtimes{} M) List
\mexists{}v1:\mBbbZ{}
\mexists{}v2:M
(loc(e) \mdownarrow{}\mmember{} orderers
\mwedge{} (((\muparrow{}es-info-auth(es;e'))
\mwedge{} (header(e') = orderhdr)
\mwedge{} has-es-info-type(es;e';mf;Id \mtimes{} \mBbbZ{} \mtimes{} M))
\mwedge{} b \mmember{} OARcast\_OrdererState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)(e')
\mwedge{} (\mneg{}(fst(msgval(e')) \mmember{} b)))
\mwedge{} <b2, b4, b5> \mmember{}
OARcast\_OrdererForSenderState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)
(fst(msgval(e')))(e)
\mwedge{} <v1, v2> \mdownarrow{}\mmember{} b2
\mwedge{} (d = 0)
\mwedge{} (m = make-Authentic-Msg(orderedhdr;<loc(e), fst(msgval(e')), v1, v2>))
\mwedge{} i \mdownarrow{}\mmember{} receivers))
\mvee{} (\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;...;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{} (m
= make-Msg(deliverhdr;<fst(snd(msgval(e')))
, fst(snd(snd(msgval(e1))))
, outl(oarcast-deliver-output((2 * flrs) + 1;<b2, b3>))>))))\000C)
\mvee{} (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{} (m
= make-Authentic-Msg(orderhdr;<loc(e)
, OARcast\_SenderStateFun(M;deliverhdr;...;...;...;mf;es;e)
, msgval(e)>)))\}
Date html generated:
2015_07_23-PM-05_21_22
Last ObjectModification:
2015_01_29-PM-09_36_25
Home
Index