TRS: {*(x, +(y, z)) -> +(*(x, y), *(x, z))} LMPO: Quasi-Precedence: empty Normal: pi(*) = [1,2] Safe: Predicative System: {*(x,+(y,z;);) -> +(*(x,y;),*(x,z;);)} Qed