Nuprl Lemma : es-le-first
∀[es:EO]. ∀[j,e:E]. if first(j) then j else e fi = e ∈ E supposing e ≤loc j
Proof
Definitions occuring in Statement :
es-le: e ≤loc e' ,
es-first: first(e),
es-E: E,
event_ordering: EO,
ifthenelse: if b then t else f fi ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Lemmas :
es-le_wf,
es-E_wf,
event_ordering_wf,
equal-wf-T-base,
assert_wf,
bnot_wf,
not_wf,
eqtt_to_assert,
uiff_transitivity,
eqff_to_assert,
assert_of_bnot,
es-locl-iff
\mforall{}[es:EO]. \mforall{}[j,e:E]. if first(j) then j else e fi = e supposing e \mleq{}loc j
Date html generated:
2015_07_17-AM-08_36_30
Last ObjectModification:
2015_01_27-PM-02_59_54
Home
Index