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

even & odd



Hi, PVS users

I want to prove that a natural number must be odd? or even? but not the twice in 
the same time ! But i don't fint the correct instanciation !!!
(X(e!1) is a nat !)

  |-------
{1}    ((inv(e!1) AND (X(e!1) /= 0)) => ((odd?(X(e!1))) OR (even?(X(e!1)))))

Thanks for your help


--------------------------------------------------------------------------------
****    Moussa AMRANI			|  Tel.: +33683438236
****					|
****    Laboratoire L.S.R. 		|  Tel.: +33476827246
****	Licence   d'informatique  	|
****    Magistere d'Informatique    	|
********************************************************************************
****    38420 Grenoble
****    FRANCE
--------------------------------------------------------------------------------