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:
2016_05_17-AM-09_02_44
Last ObjectModification:
2014_07_25-PM-02_37_25
Theory : messages
Home
Index