Nuprl Lemma : es-pred?_wf
∀[es:EO]. ∀[e:E]. (es-pred?(es;e) ∈ {e':E| (e' <loc e) ∧ (e' = pred(e) ∈ E)} ?)
Proof
Definitions occuring in Statement :
es-locl: (e <loc e'),
es-pred?: es-pred?(es;e),
es-pred: pred(e),
es-E: E,
event_ordering: EO,
uall: ∀[x:A]. B[x],
and: P ∧ Q,
unit: Unit,
member: t ∈ T,
set: {x:A| B[x]} ,
union: left + right,
equal: s = t ∈ T
Lemmas :
es-first_wf,
bool_wf,
eqtt_to_assert,
it_wf,
es-locl_wf,
es-pred_wf,
uiff_transitivity,
equal-wf-T-base,
assert_wf,
bnot_wf,
not_wf,
eqff_to_assert,
assert_of_bnot,
unit_wf2,
es-E_wf,
event_ordering_wf,
uall_wf,
isect_wf,
Id_wf,
es-loc_wf,
es-causl_wf,
assert-es-first,
es-pred_property
\mforall{}[es:EO]. \mforall{}[e:E]. (es-pred?(es;e) \mmember{} \{e':E| (e' <loc e) \mwedge{} (e' = pred(e))\} ?)
Date html generated:
2015_07_17-AM-08_35_59
Last ObjectModification:
2015_01_27-PM-02_58_30
Home
Index