§P415 Homework Assignment

Instructions:

2. Copy the PVS source files E.pvs and F.pvs

3. Using PVS, prove the theorems in each file
   

Notes and Hints:

• The PVS source files contain additional instructions and hints.

• E.pvs proofs make extensive use of the TYPEPRED prover command. You may also use GROUND for propositional simplification and arithmetic; the PVS decision procedures can solve all arithmetic subgoals, once you have set them up properly.

• In F.pvs proofs require the use of the INDUCT, in addition to commands you have already seen.

• As in earlier assignments, it is advisable to solve the problems using pencil and pencil before performing the proofs in PVS.