### 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: supposing a all: x:A. B[x] iff: ⇐⇒ Q not: ¬A implies:  Q or: P ∨ Q and: P ∧ Q equal: 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