Input TRS: 1: topB(i,N1(x),y) -> topA(1(),T1(x),y) 2: topA(i,x,N2(y)) -> topB(0(),x,T2(y)) 3: topB(i,S1(x),y) -> topA(i,N1(x),y) 4: topA(i,x,S2(y)) -> topB(i,x,N2(y)) 5: topA(i,N1(x),T2(y)) -> topB(i,N1(x),S2(y)) 6: topA(1(),T1(x),T2(y)) -> topB(1(),T1(x),S2(y)) e1: topA(i,N1(x),y) ->= topA(1(),T1(x),y) [relative] e2: topB(i,x,N2(y)) ->= topB(0(),x,T2(y)) [relative] e3: topA(i,S1(x),y) ->= topA(i,N1(x),y) [relative] e4: topB(i,x,S2(y)) ->= topB(i,x,N2(y)) [relative] e5: topB(i,N1(x),T2(y)) ->= topB(i,N1(x),S2(y)) [relative] e6: topB(1(),T1(x),T2(y)) ->= topB(1(),T1(x),S2(y)) [relative] e7: topA(i,N1(x),y) ->= topA(i,N1(C(x)),y) [relative] e8: topB(i,x,N2(y)) ->= topB(i,x,N2(C(y))) [relative] e9: topA(i,T1(x),y) ->= topA(i,T1(x),y) [relative] e10: topB(i,x,T2(y)) ->= topB(i,x,T2(y)) [relative] e11: topB(i,x,S2(y)) ->= topB(i,x,S2(D(y))) [relative] Removing trivial relative rule e9. Removing trivial relative rule e10. Number of Rules: 6 Direct POLO(Sum) ... removes: 4 1 3 5 6 2 e3 e1 I(1) = 0 I(T1) = x1 I(S1) = x1 + 4 I(topB) = x1 + x2 + x3 I(T2) = x1 I(D) = x1 I(C) = x1 I(0) = 0 I(topA) = x1 + x2 + x3 + 1 I(N2) = x1 I(N1) = x1 + 2 I(S2) = x1 Number of Rules: 0