Nuprl Lemma : OARcast-orderedhdr

∀[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,i2:Id]. ∀[k:ℤ]. ∀[v:M].
  (<d, i, mk-msg(auth;orderedhdr;<i1, i2, k, v>)> ∈ OARcast_main(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;o\000Crderhdr;receivers;senders;mf)(
                      e)
  ⇐⇒ ↓∃b2:(ℤ × M) List
        ∃b4:ℤ
         ∃b5:(ℤ × M) List
          ∃e':{e':E| e' ≤loc e } 
           ∃b:Id List
            (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)
            ∧ (d = 0 ∈ ℤ)
            ∧ auth = tt
            ∧ (i1 = loc(e) ∈ Id)
            ∧ (i2 = (fst(msgval(e'))) ∈ Id)
            ∧ i ↓∈ receivers
            ∧ <k, v> ↓∈ b2))
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,i2:Id].  \mforall{}[k:\mBbbZ{}].  \mforall{}[v:M].
    (<d
      ,  i
      ,  mk-msg(auth;orderedhdr;<i1
                                                        ,  i2
                                                        ,  k
                                                        ,  v>)>  \mmember{}
        OARcast\_main(M;deliverhdr;deqM;flrs;oarcasthdr;orderedhdr;orderers;orderhdr;receivers;...;mf)(e)
    \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}\mexists{}b2:(\mBbbZ{}  \mtimes{}  M)  List
                \mexists{}b4:\mBbbZ{}
                  \mexists{}b5:(\mBbbZ{}  \mtimes{}  M)  List
                    \mexists{}e':\{e':E|  e'  \mleq{}loc  e  \} 
                      \mexists{}b:Id  List
                        (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{}  (d  =  0)
                        \mwedge{}  auth  =  tt
                        \mwedge{}  (i1  =  loc(e))
                        \mwedge{}  (i2  =  (fst(msgval(e'))))
                        \mwedge{}  i  \mdownarrow{}\mmember{}  receivers
                        \mwedge{}  <k,  v>  \mdownarrow{}\mmember{}  b2))


Date html generated: 2015_07_23-PM-05_21_30
Last ObjectModification: 2015_01_29-PM-09_36_25

Home Index