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