HOL
HOL copied to clipboard
Arithmetic normalisation involving two subtractions fails if either can't be moved
Viz:
> SIMP_CONV (srw_ss() ++ numSimps.ARITH_ss) [] ``n2 + (fxx - 1) + 1 - n2``;
Exception- UNCHANGED raised
The n2
's should be cancelled even though the -1
can't be moved out from under the fxx
.