Nuprl Lemma : Accum-loc-classrel-weak
[B,A:
']. [f:Id 
A B B]. [init:Id bag(B)]. [X:EClass'(A)]. [es:EO']. [e:E]. [v:B].
(v 
Accum-loc-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 loc(e) a list_accum(b,a.f loc(e) 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-loc-class: Accum-loc-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),
uall: [x:A]. B[x],
pi1: fst(t),
exists: x:A. B[x],
iff: P Q,
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 :
eclass: EClass(A[eo; e]),
iff: P Q,
squash: T,
exists: x:A. B[x],
and: P Q,
member: t T,
implies: P Q,
rev_implies: P Q,
true: True,
prop: 
,
all: x:A. B[x],
cand: A c B,
top: Top,
so_lambda: 
x y.t[x; y],
uall: [x:A]. B[x],
uiff: uiff(P;Q),
uimplies: b supposing a,
so_apply: x[s1;s2],
subtype: S 
T
Lemmas :
Accum-loc-classrel,
squash_wf,
es-E_wf,
event-ordering+_inc,
Message_wf,
prior-classrel-list_wf,
classrel_wf,
bag-member_wf,
es-loc_wf,
Id_wf,
map_wf,
pi1_wf_top,
list_accum_wf,
Accum-loc-class_wf,
event-ordering+_wf,
bag_wf
\mforall{}[B,A:\mBbbU{}']. \mforall{}[f:Id {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} B]. \mforall{}[init:Id {}\mrightarrow{} bag(B)]. \mforall{}[X:EClass'(A)]. \mforall{}[es:EO']. \mforall{}[e:E]. \mforall{}[v:B].
(v \mmember{} Accum-loc-class(f;init;X)(e)
\mLeftarrow{}{}\mRightarrow{} \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 loc(e) a list\_accum(b,a.f loc(e) a b;x;map(\mlambda{}p.(fst(p));L))))))))))
Date html generated:
2011_10_20-PM-03_47_13
Last ObjectModification:
2011_09_23-PM-11_33_17
Home
Index