Nuprl Lemma : pes-axioms
∀the_es:EO
(Trans(E;e,e'.(e <loc e'))
∧ SWellFounded((e <loc e'))
∧ (∀e,e':E. (loc(e) = loc(e') ∈ Id ⇐⇒ (e <loc e') ∨ (e = e' ∈ E) ∨ (e' <loc e)))
∧ (∀e:E. (↑first(e) ⇐⇒ ∀e':E. (¬(e' <loc e))))
∧ (∀e:E. (pred(e) <loc e) ∧ (∀e':E. (¬((pred(e) <loc e') ∧ (e' <loc e)))) supposing ¬↑first(e))
∧ Trans(E;e,e'.(e < e'))
∧ SWellFounded((e < e'))
∧ (∀e,e':E. ((e <loc e') ⇒ (e < e'))))
Proof
Definitions occuring in Statement :
es-locl: (e <loc e'),
es-first: first(e),
es-pred: pred(e),
es-causl: (e < e'),
es-loc: loc(e),
es-E: E,
event_ordering: EO,
strongwellfounded: SWellFounded(R[x; y]),
Id: Id,
trans: Trans(T;x,y.E[x; y]),
assert: ↑b,
uimplies: b supposing a,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
equal: s = t ∈ T
Lemmas :
es-causl_transitivity,
es-locl_wf,
es-E_wf,
es-causl-swellfnd,
all_wf,
less_than_wf,
nat_wf,
es-causl-total,
equal_wf,
Id_wf,
es-loc_wf,
or_wf,
es-causl_wf,
and_wf,
uall_wf,
isect_wf,
not_wf,
assert-es-first,
assert_wf,
es-first_wf,
iff_wf,
es-pred_property,
es-pred_wf,
squash_wf,
true_wf,
event_ordering_wf,
iff_weakening_equal,
es-locl_irreflexivity
\mforall{}the$_{es}$:EO
(Trans(E;e,e'.(e <loc e'))
\mwedge{} SWellFounded((e <loc e'))
\mwedge{} (\mforall{}e,e':E. (loc(e) = loc(e') \mLeftarrow{}{}\mRightarrow{} (e <loc e') \mvee{} (e = e') \mvee{} (e' <loc e)))
\mwedge{} (\mforall{}e:E. (\muparrow{}first(e) \mLeftarrow{}{}\mRightarrow{} \mforall{}e':E. (\mneg{}(e' <loc e))))
\mwedge{} (\mforall{}e:E. (pred(e) <loc e) \mwedge{} (\mforall{}e':E. (\mneg{}((pred(e) <loc e') \mwedge{} (e' <loc e)))) supposing \mneg{}\muparrow{}first(e))
\mwedge{} Trans(E;e,e'.(e < e'))
\mwedge{} SWellFounded((e < e'))
\mwedge{} (\mforall{}e,e':E. ((e <loc e') {}\mRightarrow{} (e < e'))))
Date html generated:
2015_07_17-AM-08_36_19
Last ObjectModification:
2015_02_04-AM-07_07_41
Home
Index