The rewrite relation of the following TRS is considered.
f(X) | → | if(X,c,n__f(n__true)) | (1) |
if(true,X,Y) | → | X | (2) |
if(false,X,Y) | → | activate(Y) | (3) |
f(X) | → | n__f(X) | (4) |
true | → | n__true | (5) |
activate(n__f(X)) | → | f(activate(X)) | (6) |
activate(n__true) | → | true | (7) |
activate(X) | → | X | (8) |
activate#(n__f(X)) | → | activate#(X) | (9) |
f#(X) | → | if#(X,c,n__f(n__true)) | (10) |
activate#(n__true) | → | true# | (11) |
activate#(n__f(X)) | → | f#(activate(X)) | (12) |
if#(false,X,Y) | → | activate#(Y) | (13) |
The dependency pairs are split into 1 component.
if#(false,X,Y) | → | activate#(Y) | (13) |
activate#(n__f(X)) | → | f#(activate(X)) | (12) |
f#(X) | → | if#(X,c,n__f(n__true)) | (10) |
activate#(n__f(X)) | → | activate#(X) | (9) |
[activate(x1)] | = | 1 |
[n__true] | = | 0 |
[activate#(x1)] | = | x1 + 0 |
[false] | = | 4 |
[c] | = | 0 |
[true] | = | 1 |
[f(x1)] | = | 1 |
[if(x1, x2, x3)] | = | x1 + x3 + 0 |
[n__f(x1)] | = | x1 + 1 |
[f#(x1)] | = | 1 |
[if#(x1, x2, x3)] | = | x3 + 0 |
[true#] | = | 0 |
true | → | n__true | (5) |
activate(n__true) | → | true | (7) |
activate#(n__f(X)) | → | activate#(X) | (9) |
The dependency pairs are split into 1 component.
f#(X) | → | if#(X,c,n__f(n__true)) | (10) |
if#(false,X,Y) | → | activate#(Y) | (13) |
activate#(n__f(X)) | → | f#(activate(X)) | (12) |
[activate(x1)] | = | x1 + 1 |
[n__true] | = | 0 |
[activate#(x1)] | = | x1 + 3 |
[false] | = | 4 |
[c] | = | 0 |
[true] | = | 1 |
[f(x1)] | = | x1 + 1 |
[if(x1, x2, x3)] | = | x1 + x2 + x3 + 0 |
[n__f(x1)] | = | x1 + 1 |
[f#(x1)] | = | x1 + 2 |
[if#(x1, x2, x3)] | = | x1 + x3 + 0 |
[true#] | = | 0 |
f(X) | → | n__f(X) | (4) |
activate(X) | → | X | (8) |
f(X) | → | if(X,c,n__f(n__true)) | (1) |
if(false,X,Y) | → | activate(Y) | (3) |
true | → | n__true | (5) |
activate(n__true) | → | true | (7) |
activate(n__f(X)) | → | f(activate(X)) | (6) |
if(true,X,Y) | → | X | (2) |
f#(X) | → | if#(X,c,n__f(n__true)) | (10) |
if#(false,X,Y) | → | activate#(Y) | (13) |
activate#(n__f(X)) | → | f#(activate(X)) | (12) |
The dependency pairs are split into 0 components.