# [PVS-Help] Proving invariant properties in PVS

```* The simple question: Is there a way to use the definition of a
recursive function as the induction scheme to prove an invariant
property?

* For example, given this trivial function

f(n,m) : RECURSIVE nat=
if (n >= m) then n
else 2+f(n+2,m)
endif
MEASURE if (n >= m) then 0 else m-n endif

I want to prove
f_odd : LEMMA
odd?(n) IMPLIES
odd?(f(n,m))

using the definition of the function as the induction scheme, i.e.,

( (odd?(n) AND n>=m implies odd?(n)) AND
(odd?(n) IMPLIES odd?(n+2)) AND
(odd?(n) AND odd?(f(n+2,m)) IMPLIES odd?(2+f(n+2,m)))
IMPLIES
(odd?(n) IMPLIES odd?(f(n,m)) )

* Of course, I could write

f(n:(odd?),m): RECURSIVE (odd?) = ...

and one of the TCCs is similar to the induction scheme above. However,
if I also want to prove

f_even : LEMMA
even?(n) IMPLIES
even?(f(n,m))

or for that matter, any other invariant, I have to modify the type of my
function "f" (and then the TCCs gets reordered, and some proofs are
rewritten, etc, ...).

* I could probably manage to get what I need with (measure-induct+ ...)
but I wonder if there is something similar to (rule-induct ...) for
recursive functions. Does this make sense ?

Thanks,
Cesar

--
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace      mailto://C.A.Munoz@larc.nasa.gov
144 Research Drive                  http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 766 1539 Fax +1 (757) 766 1855

```