Nuprl Lemma : Accum-classrel
[B,A:
']. [f:A 
B B]. [init:Id bag(B)]. [X:EClass'(A)]. [es:EO']. [e:E]. [v:B].
uiff(v 
Accum-class(f;init;X)(e);
L:(A 
E) List
(prior-classrel-list(es;A;X;L;e)
(a:A
(a X(e)
(x:B
(bag-member(B;x;init loc(e))
(v = (f a list_accum(b,a.f a b;x;map(
p.(fst(p));L))))))))))
Proof not projected
Definitions occuring in Statement :
prior-classrel-list: prior-classrel-list(es;A;X;L;e),
Accum-class: Accum-class(f;init;X),
Message: Message,
classrel: v X(e),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-loc: loc(e),
es-E: E,
Id: Id,
map: map(f;as),
uiff: uiff(P;Q),
uall: [x:A]. B[x],
pi1: fst(t),
exists: x:A. B[x],
squash: T,
and: P Q,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
product: x:A B[x],
list: type List,
universe: Type,
equal: s = t,
list_accum: list_accum(x,a.f[x; a];y;l),
bag-member: bag-member(T;x;bs),
bag: bag(T)
Definitions :
uall: [x:A]. B[x],
uiff: uiff(P;Q),
squash: T,
exists: x:A. B[x],
and: P Q,
member: t T,
all: x:A. B[x],
label: ...$L... t,
prop: 
,
cand: A c B,
uimplies: b supposing a,
top: Top,
so_lambda: 
x y.t[x; y],
true: True,
rev_implies: P 
Q,
iff: P 
Q,
implies: P Q,
prior-classrel-list: prior-classrel-list(es;A;X;L;e),
l_all: (xL.P[x]),
subtype: S 
T,
or: P 
Q,
so_lambda: x.t[x],
not: 
A,
assert: 
b,
null: null(as),
last: last(L),
map: map(f;as),
ycomb: Y,
btrue: tt,
bfalse: ff,
ifthenelse: if b then t else f fi ,
select: l[i],
length: ||as||,
le_int: i 
z j,
bnot: 
b,
lt_int: i <z j,
classrel-list: classrel-list(es;A;X;L;e),
pi2: snd(t),
pi1: fst(t),
guard: {T},
l_disjoint: l_disjoint(T;l1;l2),
es-le: e loc e' ,
band: p q,
list_accum: list_accum(x,a.f[x; a];y;l),
so_apply: x[s1;s2],
so_apply: x[s],
false: False,
bool: 
,
unit: Unit,
it: 
Lemmas :
Accum-classrel1,
es-E_wf,
event-ordering+_inc,
Message_wf,
event-ordering+_wf,
eclass_wf2,
Id_wf,
bag_wf,
classrel_wf,
Accum-class_wf,
squash_wf,
last_wf,
null-map,
map_wf,
pi1_wf_top,
list_accum_wf,
uiff_functionality_wrt_uiff2,
iff_weakening_uiff,
last_lemma,
prior-classrel-list_wf,
bag-member_wf,
es-loc_wf,
length_wf_nat,
top_wf,
nat_wf,
member_append,
l_member_wf,
member_wf,
sorted-by-append,
es-locl_wf,
pi2_wf,
sorted-by_wf,
no_repeats_wf,
map_append_sq,
no_repeats-append,
iff_wf,
es-le_wf,
append_wf,
all_functionality_wrt_iff,
iff_functionality_wrt_iff,
es-le_weakening,
last_append,
false_wf,
not_wf,
assert_wf,
null_wf3,
map_functionality,
member_singleton,
es-locl_transitivity2,
es-le_weakening_eq,
es-locl_irreflexivity,
member_map,
last_member,
true_wf,
eclass_wf,
list_accum_append,
classrel-list_wf,
l_all_append,
l_all_single,
sorted-by-single,
no_repeats-single,
iff_transitivity,
or_functionality_wrt_iff,
null_append,
bool_wf,
uiff_transitivity,
eqtt_to_assert,
assert_of_null,
bnot_wf,
eqff_to_assert,
assert_of_bnot,
not_functionality_wrt_uiff
\mforall{}[B,A:\mBbbU{}']. \mforall{}[f:A {}\mrightarrow{} B {}\mrightarrow{} B]. \mforall{}[init:Id {}\mrightarrow{} bag(B)]. \mforall{}[X:EClass'(A)]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[v:B].
uiff(v \mmember{} Accum-class(f;init;X)(e);\mdownarrow{}\mexists{}L:(A \mtimes{} E) List
(prior-classrel-list(es;A;X;L;e)
\mwedge{} (\mexists{}a:A
(a \mmember{} X(e)
\mwedge{} (\mexists{}x:B
(bag-member(B;x;init loc(e))
\mwedge{} (v
= (f a
list\_accum(b,a.f a b;
x;
map(\mlambda{}p.(fst(p));L))))))))))
Date html generated:
2011_10_20-PM-03_46_13
Last ObjectModification:
2011_08_24-PM-03_01_38
Home
Index