0 QTRS
i(0) → 0 +(0, y) → y +(x, 0) → x i(i(x)) → x +(i(x), x) → 0 +(x, i(x)) → 0 i(+(x, y)) → +(i(x), i(y)) +(x, +(y, z)) → +(+(x, y), z) +(+(x, i(y)), y) → x +(+(x, y), i(y)) → x