[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs-help@csl.sri.com*Subject*: help with a question about unions (and sums)*From*: Mark Aronszajn <aronsz@csee.wvu.edu>*Date*: Sun, 17 Oct 1999 11:47:28 -0400 (EDT)*cc*: r.w.butler@larc.larc.nasa.gov

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):