failure-known(es;e;i) == 
x@i.e c
x 
(j:Id. ((
(j = i)) y@j.x c y))
Definitions :
all: x:A. B[x],
implies: P Q,
equal: s = t,
Id: Id,
alle-at: e@i.P[e],
not: A,
es-causle: e c e'
FDL editor aliases :
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:
2010_08_27-AM-09_40_10
Last ObjectModification:
2009_12_16-AM-08_57_38
Home
Index