The rewrite relation of the following TRS is considered.
| app(app(app(consif,true),x),ys) | → | app(app(cons,x),ys) | (1) |
| app(app(app(consif,false),x),ys) | → | ys | (2) |
| app(app(filter,f),nil) | → | nil | (3) |
| app(app(filter,f),app(app(cons,x),xs)) | → | app(app(app(consif,app(f,x)),x),app(app(filter,f),xs)) | (4) |
We uncurry the binary symbol app in combination with the following symbol map which also determines the applicative arities of these symbols.
| consif | is mapped to | consif, | consif1(x1), | consif2(x1, x2), | consif3(x1, x2, x3) |
| true | is mapped to | true | |||
| cons | is mapped to | cons, | cons1(x1), | cons2(x1, x2) | |
| false | is mapped to | false | |||
| filter | is mapped to | filter, | filter1(x1), | filter2(x1, x2) | |
| nil | is mapped to | nil |
| consif3(true,x,ys) | → | cons2(x,ys) | (12) |
| consif3(false,x,ys) | → | ys | (13) |
| filter2(f,nil) | → | nil | (14) |
| filter2(f,cons2(x,xs)) | → | consif3(app(f,x),x,filter2(f,xs)) | (15) |
| app(consif,y1) | → | consif1(y1) | (5) |
| app(consif1(x0),y1) | → | consif2(x0,y1) | (6) |
| app(consif2(x0,x1),y1) | → | consif3(x0,x1,y1) | (7) |
| app(cons,y1) | → | cons1(y1) | (8) |
| app(cons1(x0),y1) | → | cons2(x0,y1) | (9) |
| app(filter,y1) | → | filter1(y1) | (10) |
| app(filter1(x0),y1) | → | filter2(x0,y1) | (11) |
| prec(consif3) | = | 2 | stat(consif3) | = | mul | |
| prec(true) | = | 3 | stat(true) | = | mul | |
| prec(cons2) | = | 1 | stat(cons2) | = | mul | |
| prec(false) | = | 4 | stat(false) | = | mul | |
| prec(filter2) | = | 7 | stat(filter2) | = | mul | |
| prec(nil) | = | 5 | stat(nil) | = | mul | |
| prec(app) | = | 7 | stat(app) | = | mul | |
| prec(consif) | = | 8 | stat(consif) | = | mul | |
| prec(consif1) | = | 0 | stat(consif1) | = | lex | |
| prec(consif2) | = | 6 | stat(consif2) | = | lex | |
| prec(cons) | = | 9 | stat(cons) | = | mul | |
| prec(cons1) | = | 0 | stat(cons1) | = | lex | |
| prec(filter) | = | 10 | stat(filter) | = | mul | |
| prec(filter1) | = | 7 | stat(filter1) | = | mul |
| π(consif3) | = | [1,2,3] |
| π(true) | = | [] |
| π(cons2) | = | [1,2] |
| π(false) | = | [] |
| π(filter2) | = | [1,2] |
| π(nil) | = | [] |
| π(app) | = | [1,2] |
| π(consif) | = | [] |
| π(consif1) | = | [1] |
| π(consif2) | = | [2,1] |
| π(cons) | = | [] |
| π(cons1) | = | [1] |
| π(filter) | = | [] |
| π(filter1) | = | [1] |
| consif3(true,x,ys) | → | cons2(x,ys) | (12) |
| consif3(false,x,ys) | → | ys | (13) |
| filter2(f,nil) | → | nil | (14) |
| filter2(f,cons2(x,xs)) | → | consif3(app(f,x),x,filter2(f,xs)) | (15) |
| app(consif,y1) | → | consif1(y1) | (5) |
| app(consif1(x0),y1) | → | consif2(x0,y1) | (6) |
| app(consif2(x0,x1),y1) | → | consif3(x0,x1,y1) | (7) |
| app(cons,y1) | → | cons1(y1) | (8) |
| app(cons1(x0),y1) | → | cons2(x0,y1) | (9) |
| app(filter,y1) | → | filter1(y1) | (10) |
| app(filter1(x0),y1) | → | filter2(x0,y1) | (11) |
There are no rules in the TRS. Hence, it is terminating.