Nuprl Definition : cs-ref-map-constraints

cs-ref-map-constraints(V;A;W;f) ==
  ∀s:ConsensusState. ∀i:ℕ.
    ((i < ||f s|| ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
    ∧ (i < ||f s||
      ⇒ ((f s[i] = INITIAL ∈ consensus-state3(V)
          ⇐⇒ ∃v,v':V. ((¬(v = v' ∈ V)) ∧ in state s, inning i could commit v  ∧ in state s, inning i could commit v' ))
         ∧ (f s[i] = WITHDRAWN ∈ consensus-state3(V) ⇐⇒ ¬(∃v:V. in state s, inning i could commit v ))
         ∧ (∀v:V
              ((f s[i] = COMMITED[v] ∈ consensus-state3(V) ⇐⇒ in state s, inning i has committed v)
              ∧ (f s[i] = CONSIDERING[v] ∈ consensus-state3(V)
                ⇐⇒ in state s, inning i could commit v 
                    ∧ (¬in state s, inning i has committed v)
                    ∧ (∀v':V. (in state s, inning i could commit v'  ⇒ (v' = v ∈ V)))))))))


Definitions occuring in Statement :  cs-inning-committable: in state s, inning i could commit v ,  cs-inning-committed: in state s, inning i has committed v,  cs-inning: Inning(s;a),  consensus-state4: ConsensusState,  cs-commited: COMMITED[v],  cs-considering: CONSIDERING[v],  cs-withdrawn: WITHDRAWN,  cs-initial: INITIAL,  consensus-state3: consensus-state3(T),  Id: Id,  l_member: (x ∈ l),  select: L[n],  length: ||as||,  nat: ℕ,  less_than: a < b,  le: A ≤ B,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  iff: P ⇐⇒ Q,  not: ¬A,  implies: P ⇒ Q,  and: P ∧ Q,  set: {x:A| B[x]} ,  apply: f a,  equal: s = t ∈ T
FDL editor aliases :  cs-ref-map-constraints
Latex:
cs-ref-map-constraints(V;A;W;f)  ==
    \mforall{}s:ConsensusState.  \mforall{}i:\mBbbN{}.
        ((i  <  ||f  s||  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:\{a:Id|  (a  \mmember{}  A)\}  .  (i  \mleq{}  Inning(s;a)))
        \mwedge{}  (i  <  ||f  s||
            {}\mRightarrow{}  ((f  s[i]  =  INITIAL
                    \mLeftarrow{}{}\mRightarrow{}  \mexists{}v,v':V
                              ((\mneg{}(v  =  v'))
                              \mwedge{}  in  state  s,  inning  i  could  commit  v 
                              \mwedge{}  in  state  s,  inning  i  could  commit  v'  ))
                  \mwedge{}  (f  s[i]  =  WITHDRAWN  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(\mexists{}v:V.  in  state  s,  inning  i  could  commit  v  ))
                  \mwedge{}  (\mforall{}v:V
                            ((f  s[i]  =  COMMITED[v]  \mLeftarrow{}{}\mRightarrow{}  in  state  s,  inning  i  has  committed  v)
                            \mwedge{}  (f  s[i]  =  CONSIDERING[v]
                                \mLeftarrow{}{}\mRightarrow{}  in  state  s,  inning  i  could  commit  v 
                                        \mwedge{}  (\mneg{}in  state  s,  inning  i  has  committed  v)
                                        \mwedge{}  (\mforall{}v':V.  (in  state  s,  inning  i  could  commit  v'    {}\mRightarrow{}  (v'  =  v)))))))))


Date html generated: 2016_05_16-PM-00_06_29
Last ObjectModification: 2012_02_25-AM-11_45_00

Theory : event-ordering


Home Index