---

{ [V:Type]
    A:Id List. W:{a:Id| (a  A)}  List List. s:ConsensusState. i:. v:V.
      (in state s, inning i has committed v
       in state s, inning i could commit v ) }

{ Proof }

---

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,  consensus-state4: ConsensusState,  Id: Id,  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  set: {x:A| B[x]} ,  list: type List,  int: ,  universe: Type,  l_member: (x  l)
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  cs-inning-committable: in state s, inning i could commit v ,  exists: x:A. B[x],  and: P  Q,  or: P  Q,  member: t  T,  prop: ,  cand: A c B,  cs-inning-committed: in state s, inning i has committed v
Lemmas :  cs-not-completed_wf,  l_member_wf,  cs-archived_wf,  cs-inning-committed_wf,  consensus-state4_wf,  Id_wf

---

\mforall{}[V:Type]
    \mforall{}A:Id  List.  \mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List.  \mforall{}s:ConsensusState.  \mforall{}i:\mBbbZ{}.  \mforall{}v:V.
        (in  state  s,  inning  i  has  committed  v  {}\mRightarrow{}  in  state  s,  inning  i  could  commit  v  )


Date html generated: 2011_08_16-AM-10_00_11
Last ObjectModification: 2011_06_18-AM-08_58_10

Home Index