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

even & odd



amrani moussa writes:

 > 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)))))
 > 

After you expand the definitions of odd? and even?, you can
instantiate both goal formulae with `floor(X(e!1))'.  Then the
decision procedures should be able to finish off the proof.

-- 
-- Paul S. Miner                | phone: (757) 864-6201
-- 1 South Wright St. / MS 130  | fax:   (757) 864-4234
-- NASA Langley Research Center | mailto:p.s.miner@larc.nasa.gov
-- Hampton, Virginia 23681-2199 | http://shemesh.larc.nasa.gov/~psm/