NUM_CANCEL_CONV : term -> thm
Cancels identical terms from both sides of natural number equation.
Given an equational term `t1 + ... + tn = s1 + ... + sm` (with arbitrary
association of the additions) where both sides have natural number type, the
conversion identifies common elements among the ti and si, and cancels them
from both sides, returning a theorem:
where the ui and vi are the remaining elements of the ti and
si respectively, in some order.
|- t1 + ... + tn = s1 + ... + sm <=> u1 + ... + uk = v1 + ... + vl
- FAILURE CONDITIONS
Fails if applied to a term that is not an equation between natural number
# NUM_CANCEL_CONV `(a + b + x * y + SUC c) + d = SUC c + d + y * z`;;
val it : thm =
|- (a + b + x * y + SUC c) + d = SUC c + d + y * z <=>
x * y + b + a = y * z
Simplifying equations where explicitly directing the cancellation would be
tedious. However, this is mostly intended for ``bootstrapping'', before more
powerful rules like ARITH_RULE and NUM_RING are available.
- SEE ALSO
ARITH_RULE, ARITH_TAC, NUM_RING.