Input TRS: 1: app(nil(),y) -> y 2: app(add(n,x),y) -> add(n,app(x,y)) 3: reverse(nil()) -> nil() 4: reverse(add(n,x)) -> app(reverse(x),add(n,nil())) 5: shuffle(nil()) -> nil() 6: shuffle(add(n,x)) -> add(n,shuffle(reverse(x))) Number of Rules: 6 Direct QWPOS(mSum) ... orients all. I(nil) = 0 I(app) = x1 + x2 sigma(app) = [2,1] I(add) = x1 + x2 + 2 sigma(add) = [2,1] I(reverse) = x1 sigma(reverse) = [1] I(shuffle) = x1 + 1 sigma(shuffle) = [1] PREC: nil > reverse > app = shuffle > add Number of Rules: 0