Nuprl Lemma : es-le-before-no_repeats
∀[es:EO]. ∀[e:E]. no_repeats(E;≤loc(e))
Proof
Definitions occuring in Statement :
es-le-before: ≤loc(e),
es-E: E,
event_ordering: EO,
no_repeats: no_repeats(T;l),
uall: ∀[x:A]. B[x]
Lemmas :
no_repeats-append,
es-before_wf,
cons_wf,
nil_wf,
es-before-no_repeats,
no_repeats_singleton,
l_disjoint_singleton,
l_member_wf,
no_repeats_witness,
es-E_wf,
es-le-before_wf2,
subtype_rel_list,
es-le_wf,
event_ordering_wf,
es-locl_irreflexivity,
member-es-before
\mforall{}[es:EO]. \mforall{}[e:E]. no\_repeats(E;\mleq{}loc(e))
Date html generated:
2015_07_17-AM-08_44_27
Last ObjectModification:
2015_01_27-PM-02_28_53
Home
Index