{ 
es:EO
[P:E 
]. [R:E E ].
((e:E. Dec(P[e]))
(e,e':E. Dec(R e' e))
R => 
x,y.(x < y)
(e,e':E. ((P[e] 
(R e' e)) P[e']))
(e,e':E.
(P[e] P[e'] (((e R
e') 
(e = e')) (e' R e)))) supposing
((a,b,e:E.
((x,y:E.
(x c
e
y c e
P[x]
P[y]
(((x R y) (x = y)) (y R x))))
((R e a) (R e b))
((P[e] P[a]) P[b])
(a = b) supposing
((z:E. (
((R e z) (R z b) P[z]))) and
(z:E. (((R e z) (R z a) P[z])))))) and
(m,m':E.
(P[m]
P[m']
(m = m') supposing
((e:E. ((e R m') (P[e]))) and
(e:E. ((e R m) (P[e])))))))) }
{ Proof }
Definitions occuring in Statement :
es-causle: e c e',
es-causl: (e < e'),
es-E: E,
event_ordering: EO,
decidable: Dec(P),
uimplies: b supposing a,
uall: [x:A]. B[x],
prop: ,
infix_ap: x f y,
so_apply: x[s],
all: x:A. B[x],
not: A,
implies: P Q,
or: P Q,
and: P Q,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
equal: s = t,
rel_implies: R1 => R2,
rel_plus: R
Definitions :
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,
set: {x:A| B[x]} ,
dep-isect: Error :dep-isect,
record+: record+,
le: A B,
ge: i 
j ,
less_than: a < b,
uiff: uiff(P;Q),
subtype_rel: A 
r B,
es-causle: e c e',
rel_plus: R,
axiom: Ax,
lambda: x.A[x],
member: t 
T,
infix_ap: x f y,
not: A,
equal: s = t,
product: x:A 
B[x],
and: P Q,
es-causl: (e < e'),
rel_implies: R1 => R2,
apply: f a,
so_apply: x[s],
decidable: Dec(P),
event_ordering: EO,
uall: [x:A]. B[x],
es-E: E,
uimplies: b supposing a,
isect: 
x:A. B[x],
or: P Q,
union: left + right,
prop: ,
universe: Type,
implies: P Q,
all: x:A. B[x],
function: x:A B[x],
Auto: Error :Auto,
tactic: Error :tactic,
pair: <a, b>,
guard: {T},
l_member: (x l),
bool: 
,
record: record(x.T[x]),
MaAuto: Error :MaAuto,
CollapseTHEN: Error :CollapseTHEN,
trans: Trans(T;x,y.E[x; y]),
CollapseTHENA: Error :CollapseTHENA,
Unfold: Error :Unfold,
THENL_cons: Error :THENL_nil,
THENL_cons: Error :THENL_cons,
THENL_v2: Error :THENL,
void: Void,
false: False,
D: Error :D,
exists: 
x:A. B[x],
fpf: a:A fp-> B[a],
Complete: Error :Complete,
BHyp: Error :BHyp,
so_lambda: 
x y.t[x; y],
Try: Error :Try
Lemmas :
rel_plus_trans,
trans_wf,
single-threaded-relation,
false_wf,
rel-rel-plus,
rel_plus_implies,
rel_plus_minimal,
es-causl_transitivity,
decidable__rel_plus-causl,
uiff_inversion,
es-E_wf,
rel_plus_wf,
not_wf,
es-causle_wf,
rel_implies_wf,
es-causl_wf,
decidable_wf,
event_ordering_wf
\mforall{}es:EO
\mforall{}[P:E {}\mrightarrow{} \mBbbP{}]. \mforall{}[R:E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}].
((\mforall{}e:E. Dec(P[e]))
{}\mRightarrow{} (\mforall{}e,e':E. Dec(R e' e))
{}\mRightarrow{} R => \mlambda{}x,y.(x < y)
{}\mRightarrow{} (\mforall{}e,e':E. ((P[e] \mwedge{} (R e' e)) {}\mRightarrow{} P[e']))
{}\mRightarrow{} (\mforall{}e,e':E. (P[e] {}\mRightarrow{} P[e'] {}\mRightarrow{} (((e R\msupplus{} e') \mvee{} (e = e')) \mvee{} (e' R\msupplus{} e)))) supposing
((\mforall{}a,b,e:E.
((\mforall{}x,y:E. (x c\mleq{} e {}\mRightarrow{} y c\mleq{} e {}\mRightarrow{} P[x] {}\mRightarrow{} P[y] {}\mRightarrow{} (((x R\msupplus{} y) \mvee{} (x = y)) \mvee{} (y R\msupplus{} x))))
{}\mRightarrow{} ((R e a) \mwedge{} (R e b))
{}\mRightarrow{} ((P[e] \mwedge{} P[a]) \mwedge{} P[b])
{}\mRightarrow{} (a = b) supposing
((\mforall{}z:E. (\mneg{}((R\msupplus{} e z) \mwedge{} (R\msupplus{} z b) \mwedge{} P[z]))) and
(\mforall{}z:E. (\mneg{}((R\msupplus{} e z) \mwedge{} (R\msupplus{} z a) \mwedge{} P[z])))))) and
(\mforall{}m,m':E.
(P[m]
{}\mRightarrow{} P[m']
{}\mRightarrow{} (m = m') supposing ((\mforall{}e:E. ((e R m') {}\mRightarrow{} (\mneg{}P[e]))) and (\mforall{}e:E. ((e R m) {}\mRightarrow{} (\mneg{}P[e])))))\000C)))
Date html generated:
2011_08_16-AM-11_18_03
Last ObjectModification:
2011_06_20-AM-00_23_10
Home
Index