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