INT_REM_DOWN_CONV : conv

SYNOPSIS

Combines nested rem terms into a single toplevel one.

DESCRIPTION

When applied to a term containing integer arithmetic operations of negation, addition, subtraction, multiplication and exponentiation, interspersed with applying rem with a fixed modulus n, and a toplevel ... rem n too, the conversion INT_REM_DOWN_CONV proves that this is equal to a simplified term with only the toplevel rem.

FAILURE CONDITIONS

Never fails but may have no effect

EXAMPLE

  # let tm = `((x rem n) + (y rem n * &3) pow 2) rem n`;;
  val tm : term = `(x rem n + (y rem n * &3) pow 2) rem n`

  # INT_REM_DOWN_CONV tm;;
  val it : thm =
    |- (x rem n + (y rem n * &3) pow 2) rem n = (x + (y * &3) pow 2) rem n

SEE ALSO

MOD_DOWN_CONV.