Input TRS: 1: p(0(),y) -> y 2: p(s(x),y) -> s(p(x,y)) e1: p(x,y) ->= p(x,s(y)) [relative] Number of Rules: 2 Direct Mat3b ... removes: 1 I(s) = x1 I(p) = [1,0,0;1,1,0;0,0,0] * x1 + [1,0,1;0,1,0;0,0,1] * x2 + [1;1;1] I(0) = [0;1;1] Number of Rules: 1 Direct Mat3b ... removes: 2 I(s) = [1,0,0;0,1,1;0,1,0] * x1 + [0;1;1] I(p) = [1,1,1;0,1,1;0,1,0] * x1 + [1,0,0;0,0,0;0,0,0] * x2 + [1;1;1] Number of Rules: 0