0 QTRS
minus(0) → 0 +(x, 0) → x +(0, y) → y +(minus(1), 1) → 0 minus(minus(x)) → x +(x, minus(y)) → minus(+(minus(x), y)) +(x, +(y, z)) → +(+(x, y), z) +(minus(+(x, 1)), 1) → minus(x)