The rewrite relation of the following TRS is considered.
| app(app(plus,0),y) | → | y | (1) |
| app(app(plus,app(s,x)),y) | → | app(s,app(app(plus,x),y)) | (2) |
| app(app(times,0),y) | → | 0 | (3) |
| app(app(times,app(s,x)),y) | → | app(app(plus,app(app(times,x),y)),y) | (4) |
| app(app(map,f),nil) | → | nil | (5) |
| app(app(map,f),app(app(cons,x),xs)) | → | app(app(cons,app(f,x)),app(app(map,f),xs)) | (6) |
| inc | → | app(map,app(plus,app(s,0))) | (7) |
| double | → | app(map,app(times,app(s,app(s,0)))) | (8) |
We uncurry the binary symbol app in combination with the following symbol map which also determines the applicative arities of these symbols.
| plus | is mapped to | plus, | plus1(x1), | plus2(x1, x2) |
| 0 | is mapped to | 0 | ||
| s | is mapped to | s, | s1(x1) | |
| times | is mapped to | times, | times1(x1), | times2(x1, x2) |
| map | is mapped to | map, | map1(x1), | map2(x1, x2) |
| nil | is mapped to | nil | ||
| cons | is mapped to | cons, | cons1(x1), | cons2(x1, x2) |
| inc | is mapped to | inc | ||
| double | is mapped to | double |
| plus2(0,y) | → | y | (18) |
| plus2(s1(x),y) | → | s1(plus2(x,y)) | (19) |
| times2(0,y) | → | 0 | (20) |
| times2(s1(x),y) | → | plus2(times2(x,y),y) | (21) |
| map2(f,nil) | → | nil | (22) |
| map2(f,cons2(x,xs)) | → | cons2(app(f,x),map2(f,xs)) | (23) |
| inc | → | map1(plus1(s1(0))) | (24) |
| double | → | map1(times1(s1(s1(0)))) | (25) |
| app(plus,y1) | → | plus1(y1) | (9) |
| app(plus1(x0),y1) | → | plus2(x0,y1) | (10) |
| app(s,y1) | → | s1(y1) | (11) |
| app(times,y1) | → | times1(y1) | (12) |
| app(times1(x0),y1) | → | times2(x0,y1) | (13) |
| app(map,y1) | → | map1(y1) | (14) |
| app(map1(x0),y1) | → | map2(x0,y1) | (15) |
| app(cons,y1) | → | cons1(y1) | (16) |
| app(cons1(x0),y1) | → | cons2(x0,y1) | (17) |
| prec(plus2) | = | 1 | stat(plus2) | = | mul | |
| prec(0) | = | 2 | stat(0) | = | mul | |
| prec(s1) | = | 0 | stat(s1) | = | mul | |
| prec(times2) | = | 3 | stat(times2) | = | mul | |
| prec(map2) | = | 5 | stat(map2) | = | lex | |
| prec(nil) | = | 6 | stat(nil) | = | mul | |
| prec(cons2) | = | 4 | stat(cons2) | = | mul | |
| prec(app) | = | 5 | stat(app) | = | lex | |
| prec(inc) | = | 7 | stat(inc) | = | mul | |
| prec(map1) | = | 5 | stat(map1) | = | lex | |
| prec(plus1) | = | 5 | stat(plus1) | = | lex | |
| prec(double) | = | 8 | stat(double) | = | mul | |
| prec(plus) | = | 9 | stat(plus) | = | mul | |
| prec(s) | = | 10 | stat(s) | = | mul | |
| prec(times) | = | 11 | stat(times) | = | mul | |
| prec(map) | = | 12 | stat(map) | = | mul | |
| prec(cons) | = | 0 | stat(cons) | = | mul | |
| prec(cons1) | = | 0 | stat(cons1) | = | lex |
| π(plus2) | = | [1,2] |
| π(0) | = | [] |
| π(s1) | = | [1] |
| π(times2) | = | [1,2] |
| π(map2) | = | [2,1] |
| π(nil) | = | [] |
| π(cons2) | = | [1,2] |
| π(app) | = | [2,1] |
| π(inc) | = | [] |
| π(map1) | = | [1] |
| π(plus1) | = | [1] |
| π(double) | = | [] |
| π(times1) | = | 1 |
| π(plus) | = | [] |
| π(s) | = | [] |
| π(times) | = | [] |
| π(map) | = | [] |
| π(cons) | = | [] |
| π(cons1) | = | [1] |
| plus2(0,y) | → | y | (18) |
| plus2(s1(x),y) | → | s1(plus2(x,y)) | (19) |
| times2(0,y) | → | 0 | (20) |
| times2(s1(x),y) | → | plus2(times2(x,y),y) | (21) |
| map2(f,nil) | → | nil | (22) |
| map2(f,cons2(x,xs)) | → | cons2(app(f,x),map2(f,xs)) | (23) |
| inc | → | map1(plus1(s1(0))) | (24) |
| double | → | map1(times1(s1(s1(0)))) | (25) |
| app(plus,y1) | → | plus1(y1) | (9) |
| app(plus1(x0),y1) | → | plus2(x0,y1) | (10) |
| app(s,y1) | → | s1(y1) | (11) |
| app(times,y1) | → | times1(y1) | (12) |
| app(times1(x0),y1) | → | times2(x0,y1) | (13) |
| app(map,y1) | → | map1(y1) | (14) |
| app(map1(x0),y1) | → | map2(x0,y1) | (15) |
| app(cons,y1) | → | cons1(y1) | (16) |
| app(cons1(x0),y1) | → | cons2(x0,y1) | (17) |
There are no rules in the TRS. Hence, it is terminating.