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)))))
Definitions :
spreadn: spread3,
all: x:A. B[x],
l_member: (x l),
fpf-domain: fpf-domain(f),
apply: f a,
Knd: Knd,
implies: P Q,
assert: b,
isrcv: isrcv(k),
not: A,
equal: s = t,
Id: Id,
tagof: tag(k)
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:
2010_08_27-AM-09_31_57
Last ObjectModification:
2009_12_16-AM-01_09_13
Home
Index