Nuprl Definition : bag-member
x ↓∈ bs == ↓∃L:T List. ((L = bs ∈ bag(T)) ∧ (x ∈ L))
Definitions occuring in Statement :
bag: bag(T),
l_member: (x ∈ l),
list: T List,
exists: ∃x:A. B[x],
squash: ↓T,
and: P ∧ Q,
equal: s = t ∈ T
Definitions occuring in definition :
squash: ↓T,
exists: ∃x:A. B[x],
list: T List,
and: P ∧ Q,
equal: s = t ∈ T,
bag: bag(T),
l_member: (x ∈ l)
FDL editor aliases :
bag-member
Latex:
x \mdownarrow{}\mmember{} bs == \mdownarrow{}\mexists{}L:T List. ((L = bs) \mwedge{} (x \mmember{} L))
Date html generated:
2016_05_15-PM-02_36_25
Last ObjectModification:
2015_09_23-AM-07_39_54
Theory : bags
Home
Index