The rewrite relation of the following TRS is considered.
| app(app(app(compose,f),g),x) | → | app(g,app(f,x)) | (1) |
| app(reverse,l) | → | app(app(reverse2,l),nil) | (2) |
| app(app(reverse2,nil),l) | → | l | (3) |
| app(app(reverse2,app(app(cons,x),xs)),l) | → | app(app(reverse2,xs),app(app(cons,x),l)) | (4) |
| app(hd,app(app(cons,x),xs)) | → | x | (5) |
| app(tl,app(app(cons,x),xs)) | → | xs | (6) |
| last | → | app(app(compose,hd),reverse) | (7) |
| init | → | app(app(compose,reverse),app(app(compose,tl),reverse)) | (8) |
We uncurry the binary symbol app in combination with the following symbol map which also determines the applicative arities of these symbols.
| compose | is mapped to | compose, | compose1(x1), | compose2(x1, x2), | compose3(x1, x2, x3) |
| reverse | is mapped to | reverse, | reverse1(x1) | ||
| reverse2 | is mapped to | reverse2, | reverse21(x1), | reverse22(x1, x2) | |
| nil | is mapped to | nil | |||
| cons | is mapped to | cons, | cons1(x1), | cons2(x1, x2) | |
| hd | is mapped to | hd, | hd1(x1) | ||
| tl | is mapped to | tl, | tl1(x1) | ||
| last | is mapped to | last | |||
| init | is mapped to | init |
| compose3(f,g,x) | → | app(g,app(f,x)) | (19) |
| reverse1(l) | → | reverse22(l,nil) | (20) |
| reverse22(nil,l) | → | l | (21) |
| reverse22(cons2(x,xs),l) | → | reverse22(xs,cons2(x,l)) | (22) |
| hd1(cons2(x,xs)) | → | x | (23) |
| tl1(cons2(x,xs)) | → | xs | (24) |
| last | → | compose2(hd,reverse) | (25) |
| init | → | compose2(reverse,compose2(tl,reverse)) | (26) |
| app(compose,y1) | → | compose1(y1) | (9) |
| app(compose1(x0),y1) | → | compose2(x0,y1) | (10) |
| app(compose2(x0,x1),y1) | → | compose3(x0,x1,y1) | (11) |
| app(reverse,y1) | → | reverse1(y1) | (12) |
| app(reverse2,y1) | → | reverse21(y1) | (13) |
| app(reverse21(x0),y1) | → | reverse22(x0,y1) | (14) |
| app(cons,y1) | → | cons1(y1) | (15) |
| app(cons1(x0),y1) | → | cons2(x0,y1) | (16) |
| app(hd,y1) | → | hd1(y1) | (17) |
| app(tl,y1) | → | tl1(y1) | (18) |
| prec(nil) | = | 12 | weight(nil) | = | 1 | ||||
| prec(last) | = | 19 | weight(last) | = | 4 | ||||
| prec(hd) | = | 3 | weight(hd) | = | 1 | ||||
| prec(reverse) | = | 0 | weight(reverse) | = | 2 | ||||
| prec(init) | = | 6 | weight(init) | = | 7 | ||||
| prec(tl) | = | 15 | weight(tl) | = | 1 | ||||
| prec(compose) | = | 9 | weight(compose) | = | 1 | ||||
| prec(reverse2) | = | 1 | weight(reverse2) | = | 2 | ||||
| prec(cons) | = | 17 | weight(cons) | = | 2 | ||||
| prec(reverse1) | = | 16 | weight(reverse1) | = | 1 | ||||
| prec(hd1) | = | 2 | weight(hd1) | = | 1 | ||||
| prec(tl1) | = | 8 | weight(tl1) | = | 1 | ||||
| prec(compose1) | = | 10 | weight(compose1) | = | 1 | ||||
| prec(reverse21) | = | 14 | weight(reverse21) | = | 1 | ||||
| prec(cons1) | = | 18 | weight(cons1) | = | 1 | ||||
| prec(compose3) | = | 7 | weight(compose3) | = | 1 | ||||
| prec(app) | = | 11 | weight(app) | = | 0 | ||||
| prec(reverse22) | = | 13 | weight(reverse22) | = | 0 | ||||
| prec(cons2) | = | 5 | weight(cons2) | = | 0 | ||||
| prec(compose2) | = | 4 | weight(compose2) | = | 1 |
| compose3(f,g,x) | → | app(g,app(f,x)) | (19) |
| reverse1(l) | → | reverse22(l,nil) | (20) |
| reverse22(nil,l) | → | l | (21) |
| reverse22(cons2(x,xs),l) | → | reverse22(xs,cons2(x,l)) | (22) |
| hd1(cons2(x,xs)) | → | x | (23) |
| tl1(cons2(x,xs)) | → | xs | (24) |
| last | → | compose2(hd,reverse) | (25) |
| init | → | compose2(reverse,compose2(tl,reverse)) | (26) |
| app(compose,y1) | → | compose1(y1) | (9) |
| app(compose1(x0),y1) | → | compose2(x0,y1) | (10) |
| app(compose2(x0,x1),y1) | → | compose3(x0,x1,y1) | (11) |
| app(reverse,y1) | → | reverse1(y1) | (12) |
| app(reverse2,y1) | → | reverse21(y1) | (13) |
| app(reverse21(x0),y1) | → | reverse22(x0,y1) | (14) |
| app(cons,y1) | → | cons1(y1) | (15) |
| app(cons1(x0),y1) | → | cons2(x0,y1) | (16) |
| app(hd,y1) | → | hd1(y1) | (17) |
| app(tl,y1) | → | tl1(y1) | (18) |
There are no rules in the TRS. Hence, it is terminating.