Nuprl Definition : es-decl-set-avoids-tag
es-decl-set-avoids-tag(dd;b) ==
let S,ds,da = dd in
∀i:Id. ((i ∈ S) ⇒ (∀k:Knd. ((k ∈ fpf-domain(da i)) ⇒ (↑isrcv(k)) ⇒ (¬(tag(k) = b ∈ Id)))))
Definitions occuring in Statement :
fpf-domain: fpf-domain(f),
tagof: tag(k),
isrcv: isrcv(k),
Knd: Knd,
Id: Id,
l_member: (x ∈ l),
assert: ↑b,
spreadn: spread3,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
apply: f a,
equal: s = t ∈ T
FDL editor aliases :
es-decl-set-avoids-tag
es-decl-set-avoids-tag(dd;b) ==
let S,ds,da = dd in
\mforall{}i:Id. ((i \mmember{} S) {}\mRightarrow{} (\mforall{}k:Knd. ((k \mmember{} fpf-domain(da i)) {}\mRightarrow{} (\muparrow{}isrcv(k)) {}\mRightarrow{} (\mneg{}(tag(k) = b)))))
Date html generated:
2015_07_17-AM-11_56_13
Last ObjectModification:
2013_03_27-AM-10_38_39
Home
Index