Nuprl Definition : bag-no-repeats
bag-no-repeats(T;bs) == ↓∃L:T List. ((L = bs ∈ bag(T)) ∧ no_repeats(T;L))
Definitions occuring in Statement :
bag: bag(T),
no_repeats: no_repeats(T;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),
no_repeats: no_repeats(T;l)
FDL editor aliases :
bag-no-repeats
Latex:
bag-no-repeats(T;bs) == \mdownarrow{}\mexists{}L:T List. ((L = bs) \mwedge{} no\_repeats(T;L))
Date html generated:
2016_05_15-PM-02_33_32
Last ObjectModification:
2015_09_23-AM-07_39_33
Theory : bags
Home
Index