---

{ [V:Type]
    x:consensus-state3(V). (cs-is-committed(x)  v:V. (x = COMMITED[v])) }

{ Proof }

---

Definitions occuring in Statement :  cs-is-committed: cs-is-committed(x),  cs-commited: COMMITED[v],  consensus-state3: consensus-state3(T),  assert: b,  uall: [x:A]. B[x],  all: x:A. B[x],  exists: x:A. B[x],  iff: P  Q,  universe: Type,  equal: s = t
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  consensus-state3: consensus-state3(T),  iff: P  Q,  cs-is-committed: cs-is-committed(x),  exists: x:A. B[x],  cs-commited: COMMITED[v],  and: P  Q,  implies: P  Q,  rev_implies: P  Q,  member: t  T,  prop: ,  outl: outl(x),  assert: b,  isl: isl(x),  btrue: tt,  ifthenelse: if b then t else f fi ,  true: True,  uimplies: b supposing a,  bfalse: ff,  false: False
Lemmas :  assert_wf,  isl_wf,  bool_wf,  outl_wf

---

\mforall{}[V:Type].  \mforall{}x:consensus-state3(V).  (\muparrow{}cs-is-committed(x)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}v:V.  (x  =  COMMITED[v]))


Date html generated: 2011_08_16-AM-09_55_42
Last ObjectModification: 2011_06_18-AM-08_55_31

Home Index