[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 ?
The Ohio State University