Nuprl Lemma : failure-known-effective
∀[es:EO]. ∀[i:Id]. ∀[e:E]. uiff(failure-known(es;e;i);∀x@i.e c≤ x ⇒ (¬es-effective(es;x)))
Proof
Definitions occuring in Statement :
es-effective: es-effective(es;e),
failure-known: failure-known(es;e;i),
es-causle: e c≤ e',
alle-at: ∀e@i.P[e],
es-E: E,
event_ordering: EO,
Id: Id,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
not: ¬A,
implies: P ⇒ Q
Lemmas :
exists_wf,
es-E_wf,
es-causle_wf,
not_wf,
equal_wf,
Id_wf,
es-loc_wf,
all_wf,
event_ordering_wf,
squash_wf,
true_wf,
iff_weakening_equal
\mforall{}[es:EO]. \mforall{}[i:Id]. \mforall{}[e:E]. uiff(failure-known(es;e;i);\mforall{}x@i.e c\mleq{} x {}\mRightarrow{} (\mneg{}es-effective(es;x)))
Date html generated:
2015_07_17-AM-09_04_28
Last ObjectModification:
2015_02_04-PM-06_27_40
Home
Index