The rewrite relation of the following TRS is considered.
ap(f,x) | → | x | (1) |
ap(ap(ap(g,x),y),ap(s,z)) | → | ap(ap(ap(g,x),y),ap(ap(x,y),0)) | (2) |
We uncurry the binary symbol ap in combination with the following symbol map which also determines the applicative arities of these symbols.
f | is mapped to | f, | f1(x1) | ||
g | is mapped to | g, | g1(x1), | g2(x1, x2), | g3(x1, x2, x3) |
s | is mapped to | s, | s1(x1) | ||
0 | is mapped to | 0 |
f1(x) | → | x | (8) |
g3(x,y,s1(z)) | → | g3(x,y,ap(ap(x,y),0)) | (9) |
ap(f,y1) | → | f1(y1) | (3) |
ap(g,y1) | → | g1(y1) | (4) |
ap(g1(x0),y1) | → | g2(x0,y1) | (5) |
ap(g2(x0,x1),y1) | → | g3(x0,x1,y1) | (6) |
ap(s,y1) | → | s1(y1) | (7) |
f1(x0) |
g3(x0,x1,s1(x2)) |
ap(f,x0) |
ap(g,x0) |
ap(g1(x0),x1) |
ap(g2(x0,x1),x2) |
ap(s,x0) |
g3#(x,y,s1(z)) | → | g3#(x,y,ap(ap(x,y),0)) | (10) |
g3#(x,y,s1(z)) | → | ap#(ap(x,y),0) | (11) |
g3#(x,y,s1(z)) | → | ap#(x,y) | (12) |
ap#(f,y1) | → | f1#(y1) | (13) |
ap#(g2(x0,x1),y1) | → | g3#(x0,x1,y1) | (14) |
ap#(f,y1) | → | f1#(y1) | (13) |
g3#(x,y,s1(z)) | → | ap#(ap(x,y),0) | (11) |
ap#(g2(x0,x1),y1) | → | g3#(x0,x1,y1) | (14) |
g3#(x,y,s1(z)) | → | ap#(x,y) | (12) |
g3#(f,x0,s1(y2)) | → | g3#(f,x0,ap(f1(x0),0)) | (15) |
g3#(g,x0,s1(y2)) | → | g3#(g,x0,ap(g1(x0),0)) | (16) |
g3#(g1(x0),x1,s1(y2)) | → | g3#(g1(x0),x1,ap(g2(x0,x1),0)) | (17) |
g3#(g2(x0,x1),x2,s1(y2)) | → | g3#(g2(x0,x1),x2,ap(g3(x0,x1,x2),0)) | (18) |
g3#(s,x0,s1(y2)) | → | g3#(s,x0,ap(s1(x0),0)) | (19) |
g3#(g,x0,s1(y2)) | → | g3#(g,x0,ap(g1(x0),0)) | (16) |
g3#(g1(x0),x1,s1(y2)) | → | g3#(g1(x0),x1,ap(g2(x0,x1),0)) | (17) |
g3#(g2(x0,x1),x2,s1(y2)) | → | g3#(g2(x0,x1),x2,ap(g3(x0,x1,x2),0)) | (18) |
g3#(s,x0,s1(y2)) | → | g3#(s,x0,ap(s1(x0),0)) | (19) |
→ |
t0 | = | g3#(f,s,ap(s,0)) |
→R | g3#(f,s,s1(0)) | |
→P | g3#(f,s,ap(s,0)) | |
= | t2 |