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(mSum) ... orients all. I(0) = 0 I(nil) = 1 I(f) = x1 + x2 + 2 sigma(f) = [1,2] I(g) = x1 + x2 + 1 sigma(g) = [1,2] I(s) = x1 sigma(s) = [1] I(norm) = x1 sigma(norm) = [1] I(rem) = x1 + x2 sigma(rem) = [1,2] PREC: nil = f > 0 = g > norm = rem > s Number of Rules: 0