Nuprl Lemma : es-pred-one-one

[es:EO]. ∀[a,b:E].  (a b ∈ E) supposing ((pred(a) pred(b) ∈ E) and (¬↑first(b)) and (¬↑first(a)))


Definitions occuring in Statement :  es-first: first(e) es-pred: pred(e) es-E: E event_ordering: EO assert: b uimplies: supposing a uall: [x:A]. B[x] not: ¬A equal: t ∈ T
Lemmas :  pes-axioms Id_wf es-loc_wf iff_weakening_equal es-le-pred es-le_wf equal_wf es-E_wf es-pred_wf not_wf assert_wf es-first_wf2 event_ordering_wf es-locl_irreflexivity es-loc-pred and_wf
\mforall{}[es:EO].  \mforall{}[a,b:E].    (a  =  b)  supposing  ((pred(a)  =  pred(b))  and  (\mneg{}\muparrow{}first(b))  and  (\mneg{}\muparrow{}first(a)))

Date html generated: 2015_07_17-AM-08_39_18
Last ObjectModification: 2015_02_04-AM-07_07_51

Home Index