[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
help with a question about unions (and sums)
I haven't gotten any feedback on a couple of questions I've posed. I
could use some help.
I had asked whether a union operation--that takes a set (or predicate) of
sets, S, and returns the union of the members (satisfiers) of S. I know
that there is a similar operation for summation (in the finite_sets_sum
theory). I went ahead and defined my own unioning operation, but I still
don't know for sure that there wasn't one already defined in PVS.
My current questions are: Can the summation operation only be defined on
finite sets of sets; if so, how come? Presumably the same reasoning would
require that my unioning operation only be defined on finite sets
(predicates). Is that right?