Nuprl Definition : failure-known
failure-known(es;e;i) == ∀x@i.e c≤ x ⇒ (∀j:Id. ((¬(j = i ∈ Id)) ⇒ ∀y@j.¬x c≤ y))
Definitions occuring in Statement :
es-causle: e c≤ e',
alle-at: ∀e@i.P[e],
Id: Id,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
equal: s = t ∈ T
FDL editor aliases :
failure-known
failure-known
failure-known(es;e;i) == \mforall{}x@i.e c\mleq{} x {}\mRightarrow{} (\mforall{}j:Id. ((\mneg{}(j = i)) {}\mRightarrow{} \mforall{}y@j.\mneg{}x c\mleq{} y))
Date html generated:
2015_07_17-AM-09_04_05
Last ObjectModification:
2013_03_25-PM-01_56_21
Home
Index