Nuprl Lemma : es-interval-length-one-one

[es:EO]. ∀[d,b,a:E].  (b d ∈ E) supposing ((||[a, b]|| ||[a, d]|| ∈ ℤand a ≤loc d  and a ≤loc )


Definitions occuring in Statement :  es-interval: [e, e'] es-le: e ≤loc e'  es-E: E event_ordering: EO length: ||as|| uimplies: supposing a uall: [x:A]. B[x] int: equal: t ∈ T
Lemmas :  equal_wf length_wf es-interval_wf es-le_wf es-E_wf event_ordering_wf all_wf es-locl_wf es-locl-wellfnd es-le-iff es-pred_wf es-pred-locl es-locl_transitivity1 squash_wf true_wf list_wf es-interval-less iff_weakening_equal length_nil non_neg_length nil_wf length_wf_nil length_cons cons_wf length_wf_nat append_wf length_append subtype_rel_list top_wf es-pred-one-one es-interval-eq length_of_cons_lemma length_of_nil_lemma le_antisymmetry_iff add_functionality_wrt_le add-commutes le-add-cancel2 length-append l_member_non_nil pos_length decidable__le false_wf not-le-2 condition-implies-le minus-add minus-one-mul add-swap add-associates zero-add es-le-self le_wf member-es-interval
\mforall{}[es:EO].  \mforall{}[d,b,a:E].    (b  =  d)  supposing  ((||[a,  b]||  =  ||[a,  d]||)  and  a  \mleq{}loc  d    and  a  \mleq{}loc  b  )

Date html generated: 2015_07_17-AM-08_42_25
Last ObjectModification: 2015_02_04-AM-07_08_31

Home Index