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

   
  

  Qed