TRS: { rev(a()) -> a(), rev(b()) -> b(), rev(++(x, y)) -> ++(rev(y), rev(x)), rev(++(x, x)) -> rev(x)} Fail