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