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