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) |
app#(app(add,app(s,x)),y) | → | app#(add,x) | (6) |
app#(app(add,app(s,x)),y) | → | app#(app(add,x),y) | (7) |
app#(app(add,app(s,x)),y) | → | app#(s,app(app(add,x),y)) | (8) |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(app(map,f),xs) | (9) |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(f,x) | (10) |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(cons,app(f,x)) | (11) |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(app(cons,app(f,x)),app(app(map,f),xs)) | (12) |
The dependency pairs are split into 1 component.
app#(app(map,f),app(app(cons,x),xs)) | → | app#(app(map,f),xs) | (9) |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(f,x) | (10) |
app#(app(add,app(s,x)),y) | → | app#(app(add,x),y) | (7) |
π(app#) | = | 2 |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(app(map,f),xs) | (9) |
app#(app(map,f),app(app(cons,x),xs)) | → | app#(f,x) | (10) |
prec(app#) | = | 0 | stat(app#) | = | lex | |
prec(s) | = | 0 | stat(s) | = | lex | |
prec(0) | = | 0 | stat(0) | = | lex | |
prec(add) | = | 0 | stat(add) | = | lex | |
prec(app) | = | 4 | stat(app) | = | lex | |
prec(id) | = | 0 | stat(id) | = | lex |
π(app#) | = | [1] |
π(s) | = | [] |
π(0) | = | [] |
π(add) | = | [] |
π(app) | = | [2] |
π(id) | = | [] |
app(add,0) | → | id | (2) |
app#(app(add,app(s,x)),y) | → | app#(app(add,x),y) | (7) |
There are no pairs anymore.