The rewrite relation of the following TRS is considered.
a__f(X,X) | → | a__f(a,b) | (1) |
a__b | → | a | (2) |
mark(f(X1,X2)) | → | a__f(mark(X1),X2) | (3) |
mark(b) | → | a__b | (4) |
mark(a) | → | a | (5) |
a__f(X1,X2) | → | f(X1,X2) | (6) |
a__b | → | b | (7) |
[f(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[a] | = |
|
||||||||||||||||||||||||||||||||||||
[a__b] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[a__f(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[b] | = |
|
a__b | → | a | (2) |
mark(a) | → | a | (5) |
a__b | → | b | (7) |
[f(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[a] | = |
|
||||||||||||||||||||||||||||||||||||
[a__b] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[a__f(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[b] | = |
|
mark(b) | → | a__b | (4) |
[f(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[a] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[a__f(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[b] | = |
|
mark(f(X1,X2)) | → | a__f(mark(X1),X2) | (3) |
[f(x1, x2)] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||
[a] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||
[a__f(x1, x2)] | = |
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||
[b] | = |
|
a__f(X1,X2) | → | f(X1,X2) | (6) |
a__f#(X,X) | → | a__f#(a,b) | (8) |
The dependency pairs are split into 0 components.