[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.
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: email@example.com