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

Re: I would like to know the simpler way to prove.

All of your theorems yield to the following, which remove
the need to explicitly state the instantiations:

(apply (repeat (then (grind :if-match nil)(inst? :where +))))

The `:where' argument to inst? gives a clue as to where 
possible instantiations may be found in the sequent. The 
instantiation in grind has no such control, and picks 
incorrect instantiations from the antecedent instead.

Good luck,

Dr Dave Stringer-Calvert, Software Engineer, Computer Science Laboratory,
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA.
Phone: (650) 859-3291    Fax: (650) 859-2844   Email: dave_sc@csl.sri.com