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

Re: Help about Induction Scheme defination!




In addition to John's comments, please check page 19 of the PVS Language
Reference Guide (for 2.3, available at http://pvs.csl.sri.com/manuals.html)
This describes how to define even numbers using an inductive definition,
which automatically generates the necessary induction schemas for use by
(rule-induct)

Dave

---
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 David.Stringer-Calvert@sri.com