{ 
[t:
]. (SimpleConsensus1(t) 
CombinatorDef) }
{ Proof }
Definitions occuring in Statement :
SimpleConsensus1: SimpleConsensus1(t),
combinator-def: CombinatorDef,
nat: ,
uall: [x:A]. B[x],
member: t T
Definitions :
uall: [x:A]. B[x],
member: t T,
SimpleConsensus1: SimpleConsensus1(t),
nat:
Lemmas :
ThresholdComb1_wf,
nat_wf,
mlt_inning_test_wf,
mlt_nxt_inning_wf,
mlt_inning_step_wf,
mlt_inning_val_wf,
mlt_simple_consensus_init_wf
\mforall{}[t:\mBbbN{}]. (SimpleConsensus1(t) \mmember{} CombinatorDef)
Date html generated:
2011_08_17-PM-06_33_16
Last ObjectModification:
2011_06_18-AM-11_56_39
Home
Index