even & odd

["Paul S. Miner" <p.s.miner@larc.nasa.gov>]

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

---

• References:
  • even & odd
    • From: amrani moussa <amranim@ufrima.imag.fr>
  • even & odd
    • From: "Paul S. Miner" <p.s.miner@larc.nasa.gov>

• Prev by Date: even & odd
• Next by Date: Recursive Functions with negative domain
• Prev by thread: even & odd
• Next by thread: Euclidian Division
• Index(es):
  • Date
  • Thread