[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.