Input TRS: 1: f(c(X,s(Y))) -> f(c(s(X),Y)) 2: g(c(s(X),Y)) -> f(c(X,s(Y))) Number of Rules: 2 Direct POLO(Sum) ... removes: 2 I(c) = x1 + x2 I(f) = x1 I(g) = x1 + 1 I(s) = x1 Number of Rules: 1 Direct POLO(Sum) ...Direct QLPOS ... removes: 1 sigma(c) = [2,1] sigma(f) = [1] sigma(s) = [1] PREC: c > f = s Number of Rules: 0