Nuprl Lemma : es-locl-wellfnd

es:EO. WellFnd{i}(E;x,y.(x <loc y))


Proof




Definitions occuring in Statement :  es-locl: (e <loc e') es-E: E event_ordering: EO wellfounded: WellFnd{i}(A;x,y.R[x; y]) all: x:A. B[x]
Lemmas :  strongwf-implies es-E_wf es-locl_wf es-causl-swellfnd all_wf less_than_wf nat_wf event_ordering_wf
\mforall{}es:EO.  WellFnd\{i\}(E;x,y.(x  <loc  y))



Date html generated: 2015_07_17-AM-08_36_13
Last ObjectModification: 2015_01_27-PM-02_58_19

Home Index