[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs-help@csl.sri.com*From*: "Michele Rendine" <mirendi@jumpy.it>*Date*: Tue, 13 Jun 2000 21:22:30 +0200*Delivery-Date*: Tue Jun 13 12:23:19 2000

I’m having problems with PVS : I’ve defined a recursive function, called “doublefatt”, in this way : doublefatt(x) : RECURSIVE posnat = IF x=0 THEN 1 ELSIF x=1 THEN 1 ELSE x*doublefatt(x-2) ENDIF MEASURE x Then, I’ve defined also the factorial and I’ve tried to prove the following property : prop : THEOREM FORALL ( x : posnat) : x>0 IMPLIES fatt(x) = doublefatt(x)*doublefatt(x-1) The demonstration of this property is very simple if we use an inductive approach : Base : 1! = 1!*0! TRUE Inductive Hp : " m<n m! = m!!*(m-1)!! Then : n! = n* (n-1)! = n*(n-1)!!*(n-2)!! = (n-1)!!*n*(n-2)!! = (n-1)!! *n!! How is possible to obtain the same result with PVS ? Does it exists a standard way to obtain inductive proves? Thank you for your attenction.

- Prev by Date:
**Re: simple problem** - Next by Date:
**No Subject** - Prev by thread:
**No Subject** - Next by thread:
**No Subject** - Index(es):