TRS: { sum(0()) -> 0(), sum(s(x)) -> +(sum(x), s(x)), +(x, 0()) -> x, +(x, s(y)) -> s(+(x, y))} MPO: Prec: + > s, sum > + empty Strict: {} Weak: {} Qed