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

Re: Help about Induction Scheme defination!

Dear Shashank Shekhar

There are several induction schemes defined in the PVS prelude that you
can use as models.  Just do M-x vpf and seach for "induct".   You can
then do M-x edit-proof (or step-proof) to see how they are proved.

In the prover, you can do (help induct) to see how to explicitly
specify an induction scheme to the induct strategy and its relatives.

John Rushby