NUM_EVEN_CONV : conv

SYNOPSIS

Proves whether a natural number numeral is even.

DESCRIPTION

If n is a numeral (e.g. 0, 1, 2, 3,...), then NUM_EVEN_CONV `n` returns one of the theorems:

  |- EVEN(n) <=> T

  |- EVEN(n) <=> F

according to whether the number denoted by n is even.

FAILURE CONDITIONS

Fails if applied to a term that is not of the form `EVEN n` with n a numeral.

EXAMPLE

  # NUM_EVEN_CONV `EVEN 99`;;
  val it : thm = |- EVEN 99 <=> F
  # NUM_EVEN_CONV `EVEN 123456`;;
  val it : thm = |- EVEN 123456 <=> T

SEE ALSO