1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
\DOC INT_REM_DOWN_CONV
\TYPE {INT_REM_DOWN_CONV : conv}
\SYNOPSIS
Combines nested {rem} terms into a single toplevel one.
\DESCRIBE
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
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
}
\SEEALSO
MOD_DOWN_CONV.
\ENDDOC
|
