Nuprl Definition : es-decl-set-avoids
dd avoids x == let S,ds,da = dd in ∀i:Id. ((i ∈ S) ⇒ (¬↑x ∈ dom(ds i)))
Definitions occuring in Statement :
fpf-dom: x ∈ dom(f),
id-deq: IdDeq,
Id: Id,
l_member: (x ∈ l),
assert: ↑b,
spreadn: spread3,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
apply: f a
FDL editor aliases :
es-decl-set-avoids
dd avoids x == let S,ds,da = dd in \mforall{}i:Id. ((i \mmember{} S) {}\mRightarrow{} (\mneg{}\muparrow{}x \mmember{} dom(ds i)))
Date html generated:
2015_07_17-AM-11_56_03
Last ObjectModification:
2013_03_27-AM-10_38_34
Home
Index