Consider the TRS R consisting of the rewrite rules

1: x : x -> e
2: x : e -> x
3: i(x : y) -> y : x
4: (x : y) : z -> x : (z : i(y))
5: e : x -> i(x)
6: i(i(x)) -> x
7: i(e) -> e
8: x : (y : i(x)) -> i(y)
9: x : (y : (i(x) : z)) -> i(z) : y
10: i(x) : (y : x) -> i(y)
11: i(x) : (y : (x : z)) -> i(z) : y

There are 11 dependency pairs:

12: I(x : y) -> y :# x
13: (x : y) :# z -> x :# (z : i(y))
14: (x : y) :# z -> z :# i(y)
15: (x : y) :# z -> I(y)
16: e :# x -> I(x)
17: x :# (y : i(x)) -> I(y)
18: x :# (y : (i(x) : z)) -> i(z) :# y
19: x :# (y : (i(x) : z)) -> I(z)
20: i(x) :# (y : x) -> I(y)
21: i(x) :# (y : (x : z)) -> i(z) :# y
22: i(x) :# (y : (x : z)) -> I(z)

The approximated dependency graph contains one SCC:
{12-22}.

- Consider the SCC {12-22}.
By taking the polynomial interpretation
[e] = 1,
[i](x) = x,
[I](x) = x + 1
and [:](x,y) = [:#](x,y) = x + y + 1,
the rules in {1,3,4,6,7,13}
are weakly decreasing and
the rules in {2,5,8-12,14-22}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {13}.
By taking the polynomial interpretation
[e] = 1,
[i](x) = x,
[:#](x,y) = x + 1
and [:](x,y) = x + y + 1,
the rules in {1,3,4,6,7}
are weakly decreasing and
the rules in {2,5,8-11,13}
are strictly decreasing.


Hence the TRS is terminating.