---

{ [V:Type]
    A:Id List. s:ConsensusState. a:{a:Id| (a  A)} . i:. v:V.
      ((v,v':V.  Dec(v = v'))  Dec(by state s, a archived v in inning i)) }

{ Proof }

---

Definitions occuring in Statement :  cs-archived: by state s, a archived v in inning i,  consensus-state4: ConsensusState,  Id: Id,  decidable: Dec(P),  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  set: {x:A| B[x]} ,  list: type List,  int: ,  universe: Type,  equal: s = t,  l_member: (x  l)
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  cs-archived: by state s, a archived v in inning i,  member: t  T,  prop: ,  consensus-state4: ConsensusState,  and: P  Q,  so_lambda: x.t[x],  true: True,  uimplies: b supposing a,  so_apply: x[s],  uiff: uiff(P;Q),  iff: P  Q,  rev_implies: P  Q,  fpf-domain: fpf-domain(f),  cand: A c B
Lemmas :  decidable_wf,  Id_wf,  l_member_wf,  consensus-state4_wf,  decidable__cand,  fpf-domain_wf,  cs-estimate_wf,  subtype-fpf2,  subtype-top,  fpf-ap_wf,  member-fpf-dom,  subtype_rel_function,  fpf_wf,  top_wf,  subtype_rel_self,  subtype_rel_simple_product,  decidable__l_member,  decidable__equal_int

---

\mforall{}[V:Type]
    \mforall{}A:Id  List.  \mforall{}s:ConsensusState.  \mforall{}a:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}i:\mBbbZ{}.  \mforall{}v:V.
        ((\mforall{}v,v':V.    Dec(v  =  v'))  {}\mRightarrow{}  Dec(by  state  s,  a  archived  v  in  inning  i))


Date html generated: 2011_08_16-AM-09_59_03
Last ObjectModification: 2011_06_18-AM-08_57_27

Home Index