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

Re: [PVS-Help] Question regarding the "use" command



Hi there,

as the message says, provide actuals, like:

(use "sets_lemmas[T].union_empty")

Regards,
Johannes

* ADITI TAGORE [Wed, Nov 25, 2009 at 02:50:16PM +0000]:
> Hello,
> 
> I have declared a lemma called
> 
> f1: LEMMA union(s0,emptyset) = s0
> where i have defined s0 as :     s0 : VAR set[T]
> 
> When i try to prove this lemma using the command (grind) followed by  (use "sets_lemmas.union_empty") , I get a message saying
> 
> Found 0 resolutions for sets_lemmas.union_empty relative to the substitution. Please check the substitution ,provide actual parameters for lemma name, or supply more substitutions.
> 
> However , when i try (grind) followed by (apply-extensionality) , the lemma is proved.
> 
> Could you please tell me why using a lemma already defined in the prelude is not sufficient? And why does the "apply-extensionality" command prove it ?
> 
> Aditi Tagore
> The Ohio State University
> 
> 

-- 
Johannes W. E. Eriksson, M.Sc.
Ph.D. Student / Turku Centre For Computer Science (TUCS)
Åbo Akademi University / Department of Information Technologies
e-mail: joheriks@abo.fi  www: http://www.abo.fi/~joheriks