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

even & odd



Paul S. Miner writes:
 > 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
                                        ^^^^^^^^^^^^^^^
    Sorry, that should be `floor(X(e!1)/2)'

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