{ 
[Info:Type]
es:EO+(Info)
[A:Type]
P:{L:A List| 0 < ||L||} 
. num:A 
. X:EClass(A). e:E. n:
.
Dec(collect-event(es;X;n;v.num[v];L.P[L];e)) }
{ Proof }
Definitions occuring in Statement :
collect-event: collect-event(es;X;n;v.num[v];L.P[L];e),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-E: E,
length: ||as||,
bool: ,
nat: ,
decidable: Dec(P),
uall: [x:A]. B[x],
so_apply: x[s],
all: x:A. B[x],
less_than: a < b,
set: {x:A| B[x]} ,
function: x:A B[x],
list: type List,
natural_number: $n,
int: ,
universe: Type
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
collect-event: collect-event(es;X;n;v.num[v];L.P[L];e),
member: t 
T,
so_lambda: 
x y.t[x; y],
and: P 
Q,
assert: 
b,
so_apply: x[s],
implies: P 
Q,
btrue: tt,
prop: 
,
ifthenelse: if b then t else f fi ,
false: False,
bfalse: ff,
subtype: S 
T,
so_lambda: x.t[x],
true: True,
l_exists: (
xL. P[x]),
es-E-interface: E(X),
exists: x:A. B[x],
cand: A c B,
length: ||as||,
top: Top,
ycomb: Y,
decidable: Dec(P),
or: P 
Q,
not: 
A,
so_apply: x[s1;s2],
bool: ,
unit: Unit,
iff: P 
Q,
nat: ,
uimplies: b supposing a,
sq_type: SQType(T),
guard: {T},
rev_implies: P Q,
it: 
Lemmas :
es-E_wf,
event-ordering+_inc,
eclass_wf,
event-ordering+_wf,
nat_wf,
length_wf1,
bool_wf,
in-eclass_wf,
es-interface-top,
iff_weakening_uiff,
assert_wf,
eqtt_to_assert,
not_wf,
uiff_transitivity,
bnot_wf,
eqff_to_assert,
assert_of_bnot,
decidable__cand,
false_wf,
decidable__false,
decidable__equal_int,
decidable__assert,
eclass-val_wf,
mapfilter-not-nil,
es-E-interface_wf,
es-interface-predecessors_wf,
Id_wf,
es-loc_wf,
l_member_wf,
property-from-l_member,
sq_stable__equal,
eq_int_wf,
subtype_base_sq,
bool_subtype_base,
es-interface-val_wf2,
assert_elim,
es-interface-predecessors-member,
assert_of_eq_int,
mapfilter_wf,
non_neg_length,
length_wf_nat,
top_wf,
decidable__and,
true_wf
\mforall{}[Info:Type]
\mforall{}es:EO+(Info)
\mforall{}[A:Type]
\mforall{}P:\{L:A List| 0 < ||L||\} {}\mrightarrow{} \mBbbB{}. \mforall{}num:A {}\mrightarrow{} \mBbbN{}. \mforall{}X:EClass(A). \mforall{}e:E. \mforall{}n:\mBbbZ{}.
Dec(collect-event(es;X;n;v.num[v];L.P[L];e))
Date html generated:
2011_08_16-PM-05_25_02
Last ObjectModification:
2011_06_20-AM-01_23_36
Home
Index