{ 
[t:
]. [voters,clients:Id List]. (sc-env(t;voters;clients) 
E#Env) }
{ Proof }
Definitions occuring in Statement :
sc-env: sc-env(t;voters;clients),
esharp-env: E#Env,
Id: Id,
nat: ,
uall: [x:A]. B[x],
member: t T,
list: type List
Definitions :
uall: [x:A]. B[x],
member: t T,
esharp-env: E#Env,
sc-env: sc-env(t;voters;clients),
and: P 
Q,
prop: 
Lemmas :
mk-base_wf,
sc-Inputs_wf,
sc-Votes_wf,
mk-combdef_wf,
SimpleConsensus1_wf,
SimpleConsensus2_wf,
DisjointUnionComb_wf,
LeftComb_wf,
nat_wf,
RightComb_wf,
base-deriv_wf,
combinator-def_wf,
classderiv_wf,
cdv-wf_wf,
length_wf1,
cdv-types_wf,
Id_wf
\mforall{}[t:\mBbbN{}]. \mforall{}[voters,clients:Id List]. (sc-env(t;voters;clients) \mmember{} E\#Env)
Date html generated:
2011_08_17-PM-06_33_41
Last ObjectModification:
2011_06_18-AM-11_57_23
Home
Index