{ 
[V:Type]
A:Id List. e:consensus-event(V;A).
((e = NextInning)
(
v:V. (e = Archive(v)))
(b:{a:Id| (a 
A)}
i:
. z:i 
V?. (e = consensus-message(b;i;z)))) }
{ Proof }
Definitions occuring in Statement :
consensus-message: consensus-message(b;i;z),
archive-event: Archive(v),
inning-event: NextInning,
consensus-event: consensus-event(V;A),
Id: Id,
int_seg: {i..j
},
nat: ,
uall: [x:A]. B[x],
all: x:A. B[x],
exists: x:A. B[x],
or: P Q,
unit: Unit,
set: {x:A| B[x]} ,
product: x:A B[x],
union: left + right,
list: type List,
natural_number: $n,
universe: Type,
equal: s = t,
l_member: (x l)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
or: P Q,
inning-event: NextInning,
exists: x:A. B[x],
it: 
,
member: t T,
guard: {T},
prop: 
,
consensus-event: consensus-event(V;A),
nat: ,
unit: Unit,
sq_type: SQType(T),
uimplies: b supposing a,
implies: P 
Q,
archive-event: Archive(v),
consensus-message: consensus-message(b;i;z)
Lemmas :
subtype_base_sq,
unit_wf,
unit_subtype_base,
it_wf,
inning-event_wf,
archive-event_wf,
l_member_wf,
nat_wf,
int_seg_wf,
consensus-message_wf,
consensus-event_wf,
Id_wf,
nat_properties
\mforall{}[V:Type]
\mforall{}A:Id List. \mforall{}e:consensus-event(V;A).
((e = NextInning)
\mvee{} (\mexists{}v:V. (e = Archive(v)))
\mvee{} (\mexists{}b:\{a:Id| (a \mmember{} A)\} . \mexists{}i:\mBbbN{}. \mexists{}z:\mBbbN{}i \mtimes{} V?. (e = consensus-message(b;i;z))))
Date html generated:
2011_08_16-AM-10_09_24
Last ObjectModification:
2011_06_18-AM-09_02_44
Home
Index