Nuprl Lemma : es-interval-less-sq
∀[es:EO]. ∀[e,e':E]. [e, e'] ~ [e, pred(e')] @ [e'] supposing (e <loc e')
Proof
Definitions occuring in Statement :
es-interval: [e, e'],
es-locl: (e <loc e'),
es-pred: pred(e),
es-E: E,
event_ordering: EO,
append: as @ bs,
cons: [a / b],
nil: [],
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
sqequal: s ~ t
Lemmas :
es-ble_wf,
es-before_wf,
cons_wf,
nil_wf,
es-pred_wf,
es-locl-first,
assert_elim,
btrue_neq_bfalse,
assert_wf,
es-first_wf2,
bool_wf,
eqtt_to_assert,
filter_cons_lemma,
filter_nil_lemma,
list_ind_nil_lemma,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
filter_append,
assert-es-ble,
es-le_wf,
es-pred-locl,
es-le_weakening
\mforall{}[es:EO]. \mforall{}[e,e':E]. [e, e'] \msim{} [e, pred(e')] @ [e'] supposing (e <loc e')
Date html generated:
2015_07_17-AM-08_42_06
Last ObjectModification:
2015_01_27-PM-02_39_57
Home
Index