Input TRS: 1: norm(nil()) -> 0() 2: norm(g(x,y)) -> s(norm(x)) 3: f(x,nil()) -> g(nil(),x) 4: f(x,g(y,z)) -> g(f(x,y),z) 5: rem(nil(),y) -> nil() 6: rem(g(x,y),0()) -> g(x,y) 7: rem(g(x,y),s(z)) -> rem(x,z) Number of Rules: 7 Direct QWPOS(mPol) ... orients all. I(0) = 2 I(nil) = 2 I(f) = 3 * x1 + 2 * x2 + 3 sigma(f) = [2,1] I(g) = x1 + x2 + 1 sigma(g) = [1,2] I(s) = x1 sigma(s) = [1] I(norm) = 3 * x1 + 2 sigma(norm) = [1] I(rem) = x1 + 3 * x2 + 1 sigma(rem) = [2,1] PREC: norm > 0 = g > s > nil > f = rem Number of Rules: 0