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