Input TRS: 1: top(old(x)) -> top(check(x)) 2: top(new(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)) ->= old(x) [relative] Number of Rules: 2 Direct Mat2b ... removes: 1 I(new) = [1,1;0,0] * x1 I(top) = [1,1;1,1] * x1 I(bot) = [1;0] I(check) = x1 I(old) = [1,1;0,1] * x1 + [1;0] Number of Rules: 1 Direct Mat2b ... removes: e3 e4 I(new) = [2,0;1,0] * x1 + [0;1] I(top) = [2,1;0,1] * x1 I(bot) = [0;1] I(check) = [2,0;1,0] * x1 + [0;1] I(old) = [1,0;0,0] * x1 + [1;1] Number of Rules: 1 Direct Mat2b ... failed.