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

*To*: pvs-help@csl.sri.com*Subject*: Proving properties of finite sets*From*: taylort@dg-rtp.dg.com (Tad Taylor)*Date*: Tue, 22 Jul 1997 15:15:00 -0400

I'm having trouble proving the following theorem: |------- {1} is_finite[Access_Primitives](singleton[Access_Primitives](Mode(request!1))) It seems to me that the lemma finite_singleton from the finite_sets_def library would be helpful, but I can't seem to successfully use it. When I try I just get the following behavior: Rule? (use "finite_singleton") No change on: (USE "finite_singleton") Access_Added_TCC1 : |------- {1} is_finite[Access_Primitives](singleton[Access_Primitives](Mode(request!1))) Is there some special invocation I need to use a lemma from a library? Thanks, Tad -- /* Tad Taylor | 919-248-6374 */ /* Data General Corporation | taylort@dg-rtp.dg.com */ /* 62 T.W. Alexander Dr. | */ /* RTP, NC 27709 | FAX: 919-248-6108 */ >> SDA - Standard Disclaimers Apply <<

- Prev by Date:
**EMACS** - Next by Date:
**Proving properties of finite sets** - Prev by thread:
**Re: Inequations in long proof** - Next by thread:
**Proving properties of finite sets** - Index(es):