Copy PVS source files
I.pvs
and
J.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.
Turn in
modified .pvs files,
and
.prf
and
.status
as usual.
The Prover command
(both-sides opargfmla)
applies the arithmetic operation op
with argument arg
to both sides of an (in)equality. For example, (both-sides "*" "X+3" 1) mulitplies both sides of the
equation in formula 1 by X+3.
Take care not to
EXPAND
to far. If you do, you are likely to see conditional expressions
in the sequent. The proofs for this file do not require you
to manipulate conditionals—so back up.
The command (EXPAND "name" fn) expands the nthoccurance of function name in formula f.
In case you want to manipulate the conditionals anyway, the commands
LIFT-IF
and
CASE
are used. Examples will be done in lecture.
The
DATATYPE declaration
is used to define inductive types, which are types over
which one may apply induction.
So try
(induct "L")).
Much more will be said about
DATATYPE in lecture,