Consider the TRS R consisting of the rewrite rules

1: ack_in(0,n) -> ack_out(s(n))
2: ack_in(s(m),0) -> u11(ack_in(m,s(0)))
3: u11(ack_out(n)) -> ack_out(n)
4: ack_in(s(m),s(n)) -> u21(ack_in(s(m),n),m)
5: u21(ack_out(n),m) -> u22(ack_in(m,n))
6: u22(ack_out(n)) -> ack_out(n)

There are 6 dependency pairs:

7: ACK_IN(s(m),0) -> U11(ack_in(m,s(0)))
8: ACK_IN(s(m),0) -> ACK_IN(m,s(0))
9: 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)
11: U21(ack_out(n),m) -> U22(ack_in(m,n))
12: U21(ack_out(n),m) -> ACK_IN(m,n)

The approximated dependency graph contains one SCC:
{8-10,12}.

- Consider the SCC {8-10,12}.
By taking the polynomial interpretation
[0] = [ack_out](x) = [u22](x) = 1,
[u11](x) = x,
[ACK_IN](x,y) = [s](x) = [u21](x,y) = x + 1,
[ack_in](x,y) = x + y + 1
and [U21](x,y) = y + 1,
the rules in {2-4,6,10,12}
are weakly decreasing and
the rules in {1,5,8,9}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {10}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = x + 1
and [ACK_IN](x,y) = x + y + 1,
rule 10
is strictly decreasing.


Hence the TRS is terminating.