Nuprl Lemma : es-init-identity
∀[es:EO]. ∀[e:E]. uiff(es-init(es;e) = e ∈ E;↑first(e))
Proof
Definitions occuring in Statement :
es-init: es-init(es;e),
es-first: first(e),
es-E: E,
event_ordering: EO,
assert: ↑b,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Lemmas :
assert_witness,
es-first_wf2,
equal_wf,
es-E_wf,
es-init_wf,
assert_wf,
event_ordering_wf,
es-first-init,
bool_wf,
eqtt_to_assert,
eqff_to_assert,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base
\mforall{}[es:EO]. \mforall{}[e:E]. uiff(es-init(es;e) = e;\muparrow{}first(e))
Date html generated:
2015_07_17-AM-08_45_10
Last ObjectModification:
2015_01_27-PM-02_28_01
Home
Index