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

Proving properties of finite sets



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