### Nuprl Lemma : es-interval-partition

`∀[es:EO]. ∀[e',e,a:E].  [e, e'] = ([e, pred(a)] @ [a, e']) ∈ (E List) supposing (e <loc a) ∧ a ≤loc e' `

Proof

Definitions occuring in Statement :  es-interval: `[e, e']` es-le: `e ≤loc e' ` es-locl: `(e <loc e')` es-pred: `pred(e)` es-E: `E` event_ordering: `EO` append: `as @ bs` list: `T List` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` and: `P ∧ Q` equal: `s = t ∈ T`
Lemmas :  es-locl_wf es-le_wf es-E_wf event_ordering_wf all_wf list_wf es-interval_wf append_wf es-pred_wf es-locl-first assert_elim btrue_neq_bfalse assert_wf es-first_wf2 es-interval-less es-locl_transitivity2 equal_wf es-locl-wellfnd es-le-iff es-le-trans3 es-pred-locl cons_wf nil_wf append_assoc squash_wf true_wf es-locl_transitivity1 iff_weakening_equal not_wf and_wf es-interval-eq2
\mforall{}[es:EO].  \mforall{}[e',e,a:E].    [e,  e']  =  ([e,  pred(a)]  @  [a,  e'])  supposing  (e  <loc  a)  \mwedge{}  a  \mleq{}loc  e'

Date html generated: 2015_07_17-AM-08_42_36
Last ObjectModification: 2015_02_04-AM-07_08_19

Home Index