The rewrite relation of the following TRS is considered.
app(id,x) | → | x | (1) |
app(add,0) | → | id | (2) |
app(app(add,app(s,x)),y) | → | app(s,app(app(add,x),y)) | (3) |
app(app(map,f),nil) | → | nil | (4) |
app(app(map,f),app(app(cons,x),xs)) | → | app(app(cons,app(f,x)),app(app(map,f),xs)) | (5) |
The TRS is overlay and locally confluent:
10Hence, it suffices to show innermost termination in the following.
app#(app(add,app(s,x)),y) | → | app#(s,app(app(add,x),y)) | (6) |
app#(app(add,app(s,x)),y) | → | app#(app(add,x),y) | (7) |
app#(app(add,app(s,x)),y) | → | app#(add,x) | (8) |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(app(cons,app(f,x)),app(app(map,f),xs)) | (9) |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(cons,app(f,x)) | (10) |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(f,x) | (11) |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(app(map,f),xs) | (12) |
The dependency pairs are split into 2 components.
app#(app(map,f),app(app(cons,x),xs)) | → | app#(app(map,f),xs) | (12) |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(f,x) | (11) |
We restrict the rewrite rules to the following usable rules of the DP problem.
There are no rules.
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
app#(app(map,f),app(app(cons,x),xs)) | → | app#(app(map,f),xs) | (12) |
1 | ≥ | 1 | |
2 | > | 2 | |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(f,x) | (11) |
1 | > | 1 | |
2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
app#(app(add,app(s,x)),y) | → | app#(app(add,x),y) | (7) |
We restrict the rewrite rules to the following usable rules of the DP problem.
app(add,0) | → | id | (2) |
[app(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[add] | = | 1 |
[0] | = | 1 |
[id] | = | 0 |
[app#(x1, x2)] | = | 2 · x1 + 1 · x2 |
[s] | = | 0 |
app(add,0) | → | id | (2) |
app#(app(add,app(s,x)),y) | → | app#(app(add,x),y) | (7) |
app(add,0) | → | id | (2) |
There are no pairs anymore.