Consider the TRS R consisting of the rewrite rules

1: average(s(x),y) -> average(x,s(y))
2: average(x,s(s(s(y)))) -> s(average(s(x),y))
3: average(0,0) -> 0
4: average(0,s(0)) -> 0
5: average(0,s(s(0))) -> s(0)

There are 2 dependency pairs:

6: AVERAGE(s(x),y) -> AVERAGE(x,s(y))
7: AVERAGE(x,s(s(s(y)))) -> AVERAGE(s(x),y)

The approximated dependency graph contains one SCC:
{6,7}.

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

- Consider the SCC {6}.
By taking the polynomial interpretation
[AVERAGE](x,y) = [s](x) = x + 1,
rule 6
is strictly decreasing.


Hence the TRS is terminating.