Input TRS: 1: top(ok(new(x))) -> top(check(x)) 2: top(ok(old(x))) -> top(check(x)) e1: bot() ->= new(bot()) [relative] e2: check(new(x)) ->= new(check(x)) [relative] e3: check(old(x)) ->= old(check(x)) [relative] e4: check(old(x)) ->= ok(old(x)) [relative] e5: new(ok(x)) ->= ok(new(x)) [relative] e6: old(ok(x)) ->= ok(old(x)) [relative] Number of Rules: 2 Direct Mat3b ... removes: 2 I(new) = [1,0,0;0,1,0;1,0,0] * x1 + [0;0;1] I(top) = [1,1,0;0,1,0;0,0,0] * x1 I(bot) = [1;1;2] I(check) = [2,0,0;1,1,0;1,0,1] * x1 + [1;1;1] I(ok) = [2,0,0;1,1,0;1,0,1] * x1 + [1;1;1] I(old) = [2,0,0;0,1,1;1,1,0] * x1 + [1;1;1] Number of Rules: 1 Direct Mat3b ... removes: 1 e5 I(new) = [1,1,0;1,1,0;1,1,0] * x1 + [0;0;1] I(top) = [1,1,0;0,0,0;0,1,0] * x1 I(bot) = [0;0;1] I(check) = [1,1,0;1,1,0;1,0,1] * x1 + [0;0;1] I(ok) = [1,0,0;0,1,0;0,0,0] * x1 + [0;1;1] I(old) = x1 + [1;0;1] Number of Rules: 0