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

No Subject



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.