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

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


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