---

{ SimpleConsensus2()  CombinatorDef }

{ Proof }

---

Definitions occuring in Statement :  SimpleConsensus2: SimpleConsensus2(),  combinator-def: CombinatorDef,  member: t  T
Definitions :  SimpleConsensus2: SimpleConsensus2(),  ThresholdComb2: ThresholdComb2(A;B),  all: x:A. B[x],  function: x:A  B[x],  equal: s = t,  nat: ,  universe: Type,  list: type List,  int: ,  union: left + right,  member: t  T,  product: x:A  B[x]
Lemmas :  nat_wf,  ThresholdComb2_wf

---

SimpleConsensus2()  \mmember{}  CombinatorDef


Date html generated: 2010_08_27-PM-08_31_26
Last ObjectModification: 2010_06_24-AM-10_46_51

Home Index