help with a question about unions (and sums)

[Mark Aronszajn <aronsz@csee.wvu.edu>]

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?

---

• Prev by Date: having problem in Recursive definition.
• Next by Date: type vs. set
• Prev by thread: Re: type vs. set
• Next by thread: having problem in Recursive definition.
• Index(es):
  • Date
  • Thread