Copy PVS source files
K.pvs
and
L.pvs
into your working directory.
Prove all theorems in both files. Note: in order to do this you
will need to introduce some theorems of your own. Not all
the results can be proved without additional facts.
At the end of K.pvs,
you are asked to define a function, ADD, that performs
binary addition, and prove that it is correct.
P415 students: Define and test ADD in the
way illustrated earlier in the file. You are not required to complete the proof, although
I recommend that you try.
P515 students: Define and test ADD, then prove
it correct.