{ 
[t:
]. [voters,clients:Id List].
(sc-spec{i:l}(t;voters;clients) 
EO' 
') }
{ Proof }
Definitions occuring in Statement :
sc-spec: sc-spec{i:l}(t;voters;clients),
Message: Message,
event-ordering+: EO+(Info),
Id: Id,
nat: ,
uall: [x:A]. B[x],
prop: ,
member: t T,
function: x:A B[x],
list: type List
Definitions :
uall: [x:A]. B[x],
member: t T,
sc-spec: sc-spec{i:l}(t;voters;clients),
uimplies: b supposing a,
all: x:A. B[x]
Lemmas :
comp-spec_wf,
sc-compiled_wf,
sc-ok,
Id_wf,
nat_wf
\mforall{}[t:\mBbbN{}]. \mforall{}[voters,clients:Id List]. (sc-spec\{i:l\}(t;voters;clients) \mmember{} EO' {}\mrightarrow{} \mBbbP{}')
Date html generated:
2011_08_17-PM-06_35_35
Last ObjectModification:
2011_06_18-AM-11_58_22
Home
Index