Nuprl Lemma : es-le-before-partition2

[es:EO]. ∀[e,a:E].  (≤loc(e) (≤loc(pred(a)) [a, e]) ∈ (E List)) supposing ((¬↑first(a)) and a ≤loc )


Definitions occuring in Statement :  es-interval: [e, e'] es-le-before: loc(e) es-le: e ≤loc e'  es-first: first(e) es-pred: pred(e) es-E: E event_ordering: EO append: as bs list: List assert: b uimplies: supposing a uall: [x:A]. B[x] not: ¬A equal: t ∈ T
Lemmas :  es-le-before-partition list_wf es-E_wf append_wf es-le-before_wf2 es-pred_wf subtype_rel_list es-le_wf es-interval_wf iff_weakening_equal es-le-before-pred not_wf assert_wf es-first_wf2 event_ordering_wf
\mforall{}[es:EO].  \mforall{}[e,a:E].    (\mleq{}loc(e)  =  (\mleq{}loc(pred(a))  @  [a,  e]))  supposing  ((\mneg{}\muparrow{}first(a))  and  a  \mleq{}loc  e  )

Date html generated: 2015_07_17-AM-08_42_58
Last ObjectModification: 2015_02_04-AM-07_08_44

Home Index