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
Definitions unfolded in proof :
es-effective: es-effective(es;e),
alle-at: ∀e@i.P[e],
failure-known: failure-known(es;e;i),
uall: ∀[x:A]. B[x],
member: t ∈ T,
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
all: ∀x:A. B[x],
implies: P ⇒ Q,
not: ¬A,
false: False,
prop: ℙ,
so_lambda: λ2x.t[x],
so_apply: x[s],
exists: ∃x:A. B[x],
squash: ↓T,
true: True,
subtype_rel: A ⊆r B,
guard: {T},
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q
Latex:
\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:
2016_05_16-AM-10_22_14
Last ObjectModification:
2016_01_17-PM-01_21_09
Theory : new!event-ordering
Home
Index