The rewrite relation of the following TRS is considered.
a__f(f(X)) | → | a__c(f(g(f(X)))) | (1) |
a__c(X) | → | d(X) | (2) |
a__h(X) | → | a__c(d(X)) | (3) |
mark(f(X)) | → | a__f(mark(X)) | (4) |
mark(c(X)) | → | a__c(X) | (5) |
mark(h(X)) | → | a__h(mark(X)) | (6) |
mark(g(X)) | → | g(X) | (7) |
mark(d(X)) | → | d(X) | (8) |
a__f(X) | → | f(X) | (9) |
a__c(X) | → | c(X) | (10) |
a__h(X) | → | h(X) | (11) |
[d(x1)] | = |
|
||||||||||||||||||||||||
[h(x1)] | = |
|
||||||||||||||||||||||||
[a__f(x1)] | = |
|
||||||||||||||||||||||||
[a__c(x1)] | = |
|
||||||||||||||||||||||||
[a__h(x1)] | = |
|
||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||
[c(x1)] | = |
|
||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||
[g(x1)] | = |
|
a__h(X) | → | a__c(d(X)) | (3) |
[d(x1)] | = | 0 · x1 + -∞ |
[h(x1)] | = | 0 · x1 + -∞ |
[a__f(x1)] | = | 0 · x1 + -∞ |
[a__c(x1)] | = | 0 · x1 + -∞ |
[a__h(x1)] | = | 0 · x1 + -∞ |
[f(x1)] | = | 0 · x1 + -∞ |
[c(x1)] | = | 0 · x1 + -∞ |
[mark(x1)] | = | 1 · x1 + -∞ |
[g(x1)] | = | 0 · x1 + -∞ |
mark(c(X)) | → | a__c(X) | (5) |
mark(g(X)) | → | g(X) | (7) |
mark(d(X)) | → | d(X) | (8) |
[d(x1)] | = |
|
||||||||||||||||||||||||
[h(x1)] | = |
|
||||||||||||||||||||||||
[a__f(x1)] | = |
|
||||||||||||||||||||||||
[a__c(x1)] | = |
|
||||||||||||||||||||||||
[a__h(x1)] | = |
|
||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||
[c(x1)] | = |
|
||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||
[g(x1)] | = |
|
a__c(X) | → | d(X) | (2) |
[h(x1)] | = |
|
||||||||||||||||||||||||
[a__f(x1)] | = |
|
||||||||||||||||||||||||
[a__c(x1)] | = |
|
||||||||||||||||||||||||
[a__h(x1)] | = |
|
||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||
[c(x1)] | = |
|
||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||
[g(x1)] | = |
|
a__f(X) | → | f(X) | (9) |
a__c(X) | → | c(X) | (10) |
a__h(X) | → | h(X) | (11) |
[h(x1)] | = |
|
||||||||||||||||||||||||
[a__f(x1)] | = |
|
||||||||||||||||||||||||
[a__c(x1)] | = |
|
||||||||||||||||||||||||
[a__h(x1)] | = |
|
||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||
[g(x1)] | = |
|
mark(h(X)) | → | a__h(mark(X)) | (6) |
[a__f(x1)] | = |
|
||||||||||||||||||||||||
[a__c(x1)] | = |
|
||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||
[g(x1)] | = |
|
mark(f(X)) | → | a__f(mark(X)) | (4) |
prec(a__c) | = | 1 | weight(a__c) | = | 1 | ||||
prec(g) | = | 3 | weight(g) | = | 0 | ||||
prec(a__f) | = | 2 | weight(a__f) | = | 2 | ||||
prec(f) | = | 0 | weight(f) | = | 1 |
a__f(f(X)) | → | a__c(f(g(f(X)))) | (1) |
There are no rules in the TRS. Hence, it is terminating.