{ 
es:event_system{i:l}. T:Type. leaders,failset:Id List. tg1a:Id.
X,Y:Temporary AbsInterface(es;T).
(Paxos-spec9(es;T;leaders;failset;tg1a;X;Y) 
) }
{ Proof }
Definitions occuring in Statement :
Paxos-spec9: Paxos-spec9(es;T;leaders;failset;tg1a;Decide;Input),
es-interface: Temporary AbsInterface(es;A),
Id: Id,
prop: ,
all: x:A. B[x],
member: t T,
list: type List,
universe: Type
Definitions :
tactic: Error :tactic,
Paxos-spec9: Paxos-spec9(es;T;leaders;failset;tg1a;Decide;Input),
exists: 
x:A. B[x],
product: x:A 
B[x],
prop: ,
Paxos-spec9-body: Paxos-spec9-body(es;T;f;acceptors;leaders;Input;Decide;...;...;...;...;...;...),
all: x:A. B[x],
function: x:A 
B[x],
equal: s = t,
nat_plus: 
,
es-interface: Temporary AbsInterface(es;A),
Id: Id,
list: type List,
universe: Type,
nat: ,
event_ordering: EO,
subtype: S 
T,
member: t T
Lemmas :
nat_plus_inc,
Paxos-spec9-body_wf,
Id_wf,
nat_plus_wf,
event_ordering_wf,
es-interface_wf
\mforall{}es:event\_system\{i:l\}. \mforall{}T:Type. \mforall{}leaders,failset:Id List. \mforall{}tg1a:Id.
\mforall{}X,Y:Temporary AbsInterface(es;T).
(Paxos-spec9(es;T;leaders;failset;tg1a;X;Y) \mmember{} \mBbbP{})
Date html generated:
2010_08_28-PM-01_57_31
Last ObjectModification:
2010_07_15-PM-02_25_53
Home
Index