{ 
[A,B:Type]. [P:B 
]. [num:A 
]. [init:B]. [f:B A B].
(collect_accum(x.num[x];init;a,v.f[a;v];a.P[a]) 
B (B + Top)
A
( B (B + Top))) }
{ Proof }
Definitions occuring in Statement :
collect_accum: collect_accum(x.num[x];init;a,v.f[a; v];a.P[a]),
bool: ,
nat: ,
uall: [x:A]. B[x],
top: Top,
so_apply: x[s1;s2],
so_apply: x[s],
member: t T,
function: x:A B[x],
product: x:A B[x],
union: left + right,
int: ,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
top: Top,
collect_accum: collect_accum(x.num[x];init;a,v.f[a; v];a.P[a]),
so_apply: x[s],
so_apply: x[s1;s2],
spreadn: spread3,
ifthenelse: if b then t else f fi ,
all: x:A. B[x],
implies: P 
Q,
btrue: tt,
prop: 
,
bfalse: ff,
bool: ,
nat: ,
unit: Unit,
iff: P 
Q,
and: P 
Q,
it: 
,
has-value: has-value(a)
Lemmas :
bool_wf,
iff_weakening_uiff,
assert_wf,
eqtt_to_assert,
rational-has-value,
int-rational,
nat_wf,
ifthenelse_wf,
lt_int_wf,
top_wf,
not_wf,
uiff_transitivity,
bnot_wf,
eqff_to_assert,
assert_of_bnot
\mforall{}[A,B:Type]. \mforall{}[P:B {}\mrightarrow{} \mBbbB{}]. \mforall{}[num:A {}\mrightarrow{} \mBbbN{}]. \mforall{}[init:B]. \mforall{}[f:B {}\mrightarrow{} A {}\mrightarrow{} B].
(collect\_accum(x.num[x];init;a,v.f[a;v];a.P[a]) \mmember{} \mBbbZ{} \mtimes{} B \mtimes{} (B + Top) {}\mrightarrow{} A {}\mrightarrow{} (\mBbbZ{} \mtimes{} B \mtimes{} (B + Top)))
Date html generated:
2011_08_16-AM-11_04_44
Last ObjectModification:
2011_06_18-AM-09_37_26
Home
Index