Nuprl Definition : single-valued-class-except
single-valued-class-except{i:l}(f;hdrs;X) ==
∀es:EO+(Message(f)). ∀e:E. single-valued-bag([v∈X(e)|¬bmsg-header(snd(snd(v))) ∈b hdrs)];Interface)
Definitions occuring in Statement :
msg-interface: Interface
,
msg-header: msg-header(m)
,
Message: Message(f)
,
class-ap: X(e)
,
event-ordering+: EO+(Info)
,
es-E: E
,
name-deq: NameDeq
,
deq-member: x ∈b L)
,
bnot: ¬bb
,
pi2: snd(t)
,
all: ∀x:A. B[x]
,
single-valued-bag: single-valued-bag(b;T)
,
bag-filter: [x∈b|p[x]]
FDL editor aliases :
single-valued-class-except
Latex:
single-valued-class-except\{i:l\}(f;hdrs;X) ==
\mforall{}es:EO+(Message(f)). \mforall{}e:E.
single-valued-bag([v\mmember{}X(e)|\mneg{}\msubb{}msg-header(snd(snd(v))) \mmember{}\msubb{} hdrs)];Interface)
Date html generated:
2015_07_22-PM-00_00_45
Last ObjectModification:
2014_07_25-PM-02_37_25
Home
Index