{ 
[Info:Type]. [P:es:EO+(Info) 
E 
].
(local-pred-class(P) 
EClass({e':E|
(e' <loc e)
(
(P es e'))
(e'':E
((e' <loc e'')
(e'' <loc e)
(
(P es e''))))} )) }
{ Proof }
Definitions occuring in Statement :
local-pred-class: local-pred-class(P),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-locl: (e <loc e'),
es-E: E,
assert: b,
bool: ,
uall: [x:A]. B[x],
all: x:A. B[x],
not: A,
implies: P Q,
and: P Q,
member: t T,
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
universe: Type
Definitions :
subtype: S 
T,
prop: 
,
sq_exists: 
x:{A| B[x]},
union: left + right,
or: P 
Q,
axiom: Ax,
eclass: EClass(A[eo; e]),
local-pred-class: local-pred-class(P),
universe: Type,
uall: [x:A]. B[x],
bool: ,
event_ordering: EO,
isect: 
x:A. B[x],
member: t T,
equal: s = t,
event-ordering+: EO+(Info),
bag: bag(T),
set: {x:A| B[x]} ,
and: P Q,
product: x:A 
B[x],
all: x:A. B[x],
es-E: E,
implies: P Q,
function: x:A B[x],
es-locl: (e <loc e'),
not: A,
assert: b,
single-bag: {x},
empty-bag: {},
lambda: 
x.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
es-local-pred: last(P),
apply: f a,
Auto: Error :Auto,
Unfolds: Error :Unfolds,
CollapseTHEN: Error :CollapseTHEN
Lemmas :
es-local-pred_wf,
single-bag_wf,
empty-bag_wf,
es-locl_wf,
not_wf,
assert_wf,
event-ordering+_wf,
es-E_wf,
event-ordering+_inc,
bool_wf
\mforall{}[Info:Type]. \mforall{}[P:es:EO+(Info) {}\mrightarrow{} E {}\mrightarrow{} \mBbbB{}].
(local-pred-class(P) \mmember{} EClass(\{e':E|
(e' <loc e)
\mwedge{} (\muparrow{}(P es e'))
\mwedge{} (\mforall{}e'':E. ((e' <loc e'') {}\mRightarrow{} (e'' <loc e) {}\mRightarrow{} (\mneg{}\muparrow{}(P es e''))))\} ))
Date html generated:
2011_08_16-PM-04_42_12
Last ObjectModification:
2011_06_20-AM-01_02_11
Home
Index