{ 
es:EO. p:E 
(E + Top).
(causal-predecessor(es;p) 
SWellFounded(p-graph(E;p) y x)) }
{ Proof }
Definitions occuring in Statement :
causal-predecessor: causal-predecessor(es;p),
es-E: E,
event_ordering: EO,
top: Top,
all: x:A. B[x],
implies: P Q,
apply: f a,
function: x:A B[x],
union: left + right,
p-graph: p-graph(A;f),
strongwellfounded: SWellFounded(R[x; y])
Definitions :
equal: s = t,
member: t 
T,
function: x:A B[x],
all: x:A. B[x],
strongwellfounded: SWellFounded(R[x; y]),
subtype_rel: A 
r B,
strong-subtype: strong-subtype(A;B),
apply: f a,
record-select: r.x,
infix_ap: x f y,
assert: 
b,
causal-predecessor: causal-predecessor(es;p),
dep-isect: Error :dep-isect,
eq_atom: x =a y,
eq_atom: eq_atom$n(x;y),
record+: record+,
event_ordering: EO,
es-E: E,
universe: Type,
prop: 
,
rel_implies: R1 => R2,
p-graph: p-graph(A;f),
lambda: 
x.A[x],
implies: P Q,
top: Top,
union: left + right,
es-causl: (e < e'),
so_lambda: 
x y.t[x; y],
void: Void,
isect: 
x:A. B[x],
subtype: S T,
do-apply: do-apply(f;x),
suptype: suptype(S; T),
can-apply: can-apply(f;x),
cand: A c
B,
product: x:A 
B[x],
and: P Q,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ifthenelse: if b then t else f fi ,
guard: {T},
set: {x:A| B[x]}
Lemmas :
es-causl-swellfnd,
assert_wf,
can-apply_wf,
do-apply_wf,
member_wf,
causal-predecessor_wf,
top_wf,
event_ordering_wf,
strongwf-monotone,
p-graph_wf2,
p-graph_wf,
rel_implies_wf,
es-causl_wf,
es-E_wf,
strongwellfounded_wf
\mforall{}es:EO. \mforall{}p:E {}\mrightarrow{} (E + Top). (causal-predecessor(es;p) {}\mRightarrow{} SWellFounded(p-graph(E;p) y x))
Date html generated:
2011_08_16-AM-11_12_39
Last ObjectModification:
2010_09_24-PM-08_47_30
Home
Index