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

Re: What have I missed ? (a proof failed)



Yechiel,

Dave's message told you how to prove it, but didn't tell you why
(grind :theories ("stack_0")) didn't do it on its own.  The reason is
that grind only uses lemmas that have the form of (conditional)
rewrite rules, and equal_ax doesn't have this form.

A single command that does prove the conjecture is
(STEW :LEMMAS "equal_ax"))

The stew strategy is described in the "less elementary tutorial": 
at http://www.csl.sri.com/csl-95-10.html

John
-------