Nuprl Lemma : Accum-classrel-weak
[B,A:
']. [f:A 
B B]. [init:Id bag(B)]. [X:EClass'(A)]. [es:EO']. [e:E]. [v:B].
(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. (x init loc(e) (v = (f a es-history-accum(es;A;B;x;f;L)))))))))
Proof not projected
Definitions occuring in Statement :
es-history-accum: es-history-accum(es;A;B;x;f;L),
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,
uall: [x:A]. B[x],
exists: x:A. B[x],
iff: P Q,
squash: T,
and: P Q,
apply: f a,
function: x:A B[x],
product: x:A B[x],
list: type List,
universe: Type,
equal: s = t,
bag-member: x bs,
bag: bag(T)
Definitions :
uall: [x:A]. B[x],
iff: P Q,
classrel: v X(e),
squash: T,
exists: x:A. B[x],
and: P Q,
bag-member: x bs,
es-history-accum: es-history-accum(es;A;B;x;f;L),
member: t T,
implies: P Q,
rev_implies: P Q,
so_lambda: 
x.t[x],
true: True,
label: ...$L... t,
uiff: uiff(P;Q),
uimplies: b supposing a,
prop: 
,
so_apply: x[s],
all: x:A. B[x],
subtype: S 
T
Lemmas :
Accum-classrel,
classrel_wf,
Message_wf,
Accum-class_wf,
squash_wf,
exists_wf,
es-E_wf,
event-ordering+_inc,
and_wf,
prior-classrel-list_wf,
bag-member_wf,
es-loc_wf,
equal_wf,
es-history-accum_wf,
event-ordering+_wf,
eclass_wf2,
Id_wf,
bag_wf
\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].
(v \mmember{} Accum-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. (x \mdownarrow{}\mmember{} init loc(e) \mwedge{} (v = (f a es-history-accum(es;A;B;x;f;L)))))))))
Date html generated:
2012_01_23-PM-01_18_57
Last ObjectModification:
2012_01_07-PM-02_57_52
Home
Index