TRS: { sum(0()) -> 0(), sum(s(x)) -> +(sqr(s(x)), sum(x)), sqr(x) -> *(x, x), sum(s(x)) -> +(*(s(x), s(x)), sum(x))} POP*: Precedence: sqr > *, sum > +, sum > sqr, sum > * empty Normal: pi(sqr) = [1], pi(sum) = [1] Safe: pi(*) = [1,2], pi(s) = [1], pi(+) = [1,2] Predicative System: { sum(0();) -> 0(), sum(s(;x);) -> +(;sqr(s(;x);),sum(x;)), sqr(x;) -> *(;x,x), sum(s(;x);) -> +(;*(;s(;x),s(;x)),sum(x;))} Qed