Nuprl Lemma : es-interval-one-one

[es:EO]. ∀[d,b,a,c:E].
  ({(a c ∈ E) ∧ (b d ∈ E)}) supposing (([a, b] [c, d] ∈ (E List)) and c ≤loc d  and a ≤loc )


Definitions occuring in Statement :  es-interval: [e, e'] es-le: e ≤loc e'  es-E: E event_ordering: EO list: List uimplies: supposing a uall: [x:A]. B[x] guard: {T} and: P ∧ Q equal: t ∈ T
Lemmas :  equal_wf list_wf es-E_wf es-interval_wf es-le_wf event_ordering_wf hd-es-interval hd_wf pos_length es-locl_transitivity2 es-locl_irreflexivity es-locl_wf es-interval-nil es-le-loc equal-wf-T-base not_wf ge_wf length_wf es-interval-length-one-one es-le_transitivity es-le_weakening_eq and_wf
\mforall{}[es:EO].  \mforall{}[d,b,a,c:E].
    (\{(a  =  c)  \mwedge{}  (b  =  d)\})  supposing  (([a,  b]  =  [c,  d])  and  c  \mleq{}loc  d    and  a  \mleq{}loc  b  )

Date html generated: 2015_07_17-AM-08_42_27
Last ObjectModification: 2015_01_27-PM-02_41_16

Home Index