The rewrite relation of the following TRS is considered.
ack_in(0,n) | → | ack_out(s(n)) | (1) |
ack_in(s(m),0) | → | u11(ack_in(m,s(0))) | (2) |
u11(ack_out(n)) | → | ack_out(n) | (3) |
ack_in(s(m),s(n)) | → | u21(ack_in(s(m),n),m) | (4) |
u21(ack_out(n),m) | → | u22(ack_in(m,n)) | (5) |
u22(ack_out(n)) | → | ack_out(n) | (6) |
ack_in#(s(m),0) | → | ack_in#(m,s(0)) | (7) |
ack_in#(s(m),0) | → | u11#(ack_in(m,s(0))) | (8) |
ack_in#(s(m),s(n)) | → | ack_in#(s(m),n) | (9) |
ack_in#(s(m),s(n)) | → | u21#(ack_in(s(m),n),m) | (10) |
u21#(ack_out(n),m) | → | ack_in#(m,n) | (11) |
u21#(ack_out(n),m) | → | u22#(ack_in(m,n)) | (12) |
The dependency pairs are split into 1 component.
u21#(ack_out(n),m) | → | ack_in#(m,n) | (11) |
ack_in#(s(m),s(n)) | → | u21#(ack_in(s(m),n),m) | (10) |
ack_in#(s(m),s(n)) | → | ack_in#(s(m),n) | (9) |
ack_in#(s(m),0) | → | ack_in#(m,s(0)) | (7) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
u21#(ack_out(n),m) | → | ack_in#(m,n) | (11) |
2 | ≥ | 1 | |
1 | > | 2 | |
ack_in#(s(m),s(n)) | → | u21#(ack_in(s(m),n),m) | (10) |
1 | > | 2 | |
ack_in#(s(m),s(n)) | → | ack_in#(s(m),n) | (9) |
2 | > | 2 | |
1 | ≥ | 1 | |
ack_in#(s(m),0) | → | ack_in#(m,s(0)) | (7) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.