{ 
[voters,clients:Id List]. (sc-rules(voters;clients) 
E#Rule List) }
{ Proof }
Definitions occuring in Statement :
sc-rules: sc-rules(voters;clients),
esharp-rule: E#Rule,
Id: Id,
uall: [x:A]. B[x],
member: t T,
list: type List
Definitions :
uall: [x:A]. B[x],
member: t T,
sc-rules: sc-rules(voters;clients),
spreadn: spread3,
btrue: tt,
assert: 
b,
le: A 
B,
prop: 
,
ifthenelse: if b then t else f fi ,
true: True,
false: False,
all: x:A. B[x],
subtype: S 
T,
and: P 
Q,
not: 
A,
implies: P 
Q,
nat: 
,
rev_implies: P 
Q,
iff: P Q
Lemmas :
mk-prop-rule_wf,
sc-Archive_wf,
nat_wf,
product-limited,
int_wf_limited,
band_wf,
le_int_wf,
nat_properties,
assert_wf,
sc-Learn_wf,
btrue_wf,
true_wf,
esharp-rule_wf,
Id_wf,
le_wf,
iff_weakening_uiff,
uiff_transitivity,
assert_of_band,
and_functionality_wrt_uiff,
assert_of_le_int
\mforall{}[voters,clients:Id List]. (sc-rules(voters;clients) \mmember{} E\#Rule List)
Date html generated:
2011_08_17-PM-06_33_52
Last ObjectModification:
2011_06_18-AM-11_57_38
Home
Index