m(-A) => [d(D), p(ptimes(-1,A,R)), a(R)],
m(max(A,B)) => [d(D), p(pgeq(R, A)), p(pgeq(R, B)), p(pmax(A,B,R)), a(A,B,R)],
m(min(A,B)) => [d(D), p(pgeq(A, R)), p(pgeq(B, R)), p(pmin(A,B,R)), a(A,B,R)],
- m(abs(A)) => [g(#R#>=0), d(D), p(pabs(A, R)), a(A,R)],
+ m(abs(A)) => [d(D), g(#R#>=0), p(pabs(A, R)), a(A,R)],
+ m(A^B) => [d(D), p(pexp(A,B,R)), a(A,B,R)],
m(A/B) => [d(D1), p(preified_slash(A,B,D2,R)),
p(reified_and(D1,[],D2,[],D)),a(D2),a(A,B,R)],
m(A//B) => [skeleton(A,B,D,R,ptzdiv)],
m(A div B) => [skeleton(A,B,D,R,pdiv)],
m(A mod B) => [skeleton(A,B,D,R,pmod)],
m(A rem B) => [skeleton(A,B,D,R,prem)],
- m(A^B) => [d(D), p(pexp(A,B,R)), a(A,B,R)],
% bitwise operations
m(\A) => [function(D,\,A,R)],
m(msb(A)) => [g(#A#>0) ,function(D,msb,A,R)],