{ 
es:EO
[P:E 
]
((e:E. Dec(P[e]))
(
m:E
(P[m] 
(e:E. (P[e] ((e = m) 
(e':E. ((e' < e) P[e'])))))))
(e,e':E. (P[e] P[e'] (((e < e') (e = e')) (e' < e))))
supposing e,e',x:E.
((es-p-immediate-pred(es;
e.P[e]) e x)
(es-p-immediate-pred(es;e.P[e]) e' x)
(e = e'))) }
{ Proof }
Definitions occuring in Statement :
es-p-immediate-pred: es-p-immediate-pred(es;P),
es-causl: (e < e'),
es-E: E,
event_ordering: EO,
decidable: Dec(P),
uimplies: b supposing a,
uall: [x:A]. B[x],
prop: ,
so_apply: x[s],
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
or: P Q,
and: P Q,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
equal: s = t
Definitions :
same-thread: same-thread(es;p;e;e'),
subtype: S 
T,
suptype: suptype(S; T),
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ifthenelse: if b then t else f fi ,
do-apply: do-apply(f;x),
rev_implies: P 
Q,
can-apply: can-apply(f;x),
iff: P Q,
p-inject: p-inject(A;B;f),
causal-predecessor: causal-predecessor(es;p),
top: Top,
record: record(x.T[x]),
void: Void,
false: False,
true: True,
squash: 
T,
pair: <a, b>,
fpf: a:A fp-> B[a],
guard: {T},
limited-type: LimitedType,
strong-subtype: strong-subtype(A;B),
assert: 
b,
eq_atom: x =a y,
eq_atom: eq_atom$n(x;y),
record-select: r.x,
infix_ap: x f y,
dep-isect: Error :dep-isect,
record+: record+,
le: A 
B,
ge: i 
j ,
not: 
A,
less_than: a < b,
uiff: uiff(P;Q),
subtype_rel: A r B,
and: P Q,
product: x:A 
B[x],
exists: x:A. B[x],
axiom: Ax,
event_ordering: EO,
uall: [x:A]. B[x],
or: P Q,
union: left + right,
universe: Type,
uimplies: b supposing a,
isect: 
x:A. B[x],
equal: s = t,
es-r-pred: es-r-pred{i:l}(es;d),
so_apply: x[s],
lambda: x.A[x],
es-p-immediate-pred: es-p-immediate-pred(es;P),
es-causl: (e < e'),
so_apply: x[s1;s2],
implies: P Q,
es-E: E,
all: x:A. B[x],
prop: ,
function: x:A B[x],
set: {x:A| B[x]} ,
member: t 
T,
apply: f a,
decidable: Dec(P),
cand: A c B,
bool: 
,
final-iterate: final-iterate(f;x),
p-graph: p-graph(A;f),
strongwellfounded: SWellFounded(R[x; y]),
nat: 
,
rel_implies: R1 => R2,
so_lambda: 
x y.t[x; y],
int: 
,
p-fun-exp: f^n
Lemmas :
false_wf,
ifthenelse_wf,
final-iterate-p-immediate-pred,
final-iterate-property,
rel_implies_wf,
p-graph_wf,
p-graph_wf2,
strongwf-monotone,
strongwellfounded_wf,
nat_wf,
es-causl-swellfnd,
final-iterate_wf,
es-E_wf,
es-p-immediate-pred_wf,
not_wf,
decidable_wf,
decidable__es-p-immediate-pred,
event_ordering_wf,
es-causl_wf,
true_wf,
squash_wf,
es-r-pred-property,
thread-ordered,
es-r-pred_wf,
assert_wf,
p-inject_wf,
do-apply_wf,
can-apply_wf,
top_wf,
member_wf,
same-thread_wf
\mforall{}es:EO
\mforall{}[P:E {}\mrightarrow{} \mBbbP{}]
((\mforall{}e:E. Dec(P[e]))
{}\mRightarrow{} (\mexists{}m:E. (P[m] \mwedge{} (\mforall{}e:E. (P[e] {}\mRightarrow{} ((e = m) \mvee{} (\mexists{}e':E. ((e' < e) \mwedge{} P[e'])))))))
{}\mRightarrow{} (\mforall{}e,e':E. (P[e] {}\mRightarrow{} P[e'] {}\mRightarrow{} (((e < e') \mvee{} (e = e')) \mvee{} (e' < e))))
supposing \mforall{}e,e',x:E.
((es-p-immediate-pred(es;\mlambda{}e.P[e]) e x)
{}\mRightarrow{} (es-p-immediate-pred(es;\mlambda{}e.P[e]) e' x)
{}\mRightarrow{} (e = e')))
Date html generated:
2011_08_16-AM-11_17_41
Last ObjectModification:
2011_06_20-AM-00_22_58
Home
Index