[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?