We consider two TRSs R and S where R contains the rules
| if(true,a,x) | → | a | (1) |
| if(true,b,x) | → | b | (2) |
| if(true,g(a),x) | → | g(a) | (3) |
| if(true,g(b),x) | → | g(b) | (4) |
| if(false,x,a) | → | a | (5) |
| if(false,x,b) | → | b | (6) |
| if(false,x,g(a)) | → | g(a) | (7) |
| if(false,x,g(b)) | → | g(b) | (8) |
| g(a) | → | g(g(a)) | (9) |
| g(b) | → | a | (10) |
| f'(a,b) | → | b | (11) |
| f'(g(g(a)),x) | → | b | (12) |
and S contains the following rules:
| h(c,c) | → | h(b,f(b)) | (13) |
| f(h(a,h(c,a))) | → | c | (14) |
| h(c,b) | → | f(a) | (15) |
The underlying signature is as follows:
{a/0, b/0, c/0, f/1, g/1, h/2, f'/2, if/3, true/0, false/0}