Consider the TRS R consisting of the rewrite rules

1: f(x,f(s(s(y)),f(z,w))) -> f(s(x),f(y,f(s(z),w)))
2: L(f(s(s(y)),f(z,w))) -> L(f(s(0),f(y,f(s(z),w))))
3: f(x,f(s(s(y)),nil)) -> f(s(x),f(y,f(s(0),nil)))

There are 10 dependency pairs:

4: F(x,f(s(s(y)),f(z,w))) -> F(s(x),f(y,f(s(z),w)))
5: F(x,f(s(s(y)),f(z,w))) -> F(y,f(s(z),w))
6: F(x,f(s(s(y)),f(z,w))) -> F(s(z),w)
7: L#(f(s(s(y)),f(z,w))) -> L#(f(s(0),f(y,f(s(z),w))))
8: L#(f(s(s(y)),f(z,w))) -> F(s(0),f(y,f(s(z),w)))
9: L#(f(s(s(y)),f(z,w))) -> F(y,f(s(z),w))
10: L#(f(s(s(y)),f(z,w))) -> F(s(z),w)
11: F(x,f(s(s(y)),nil)) -> F(s(x),f(y,f(s(0),nil)))
12: F(x,f(s(s(y)),nil)) -> F(y,f(s(0),nil))
13: F(x,f(s(s(y)),nil)) -> F(s(0),nil)

The approximated dependency graph contains 2 SCCs:
{4-6,11,12}
and {7}.

- Consider the SCC {4-6,11,12}.
The usable rules are {1,3}.
By taking the polynomial interpretation
[0] = 0,
[nil] = 1,
[s](x) = x + 1,
[f](x,y) = x + y
and [F](x,y) = x + y + 1,
the rules in {1,3,4,11}
are weakly decreasing and
the rules in {5,6,12}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {4,11}.
By taking the polynomial interpretation
[0] = 0,
[nil] = 1,
[s](x) = x + 1,
[f](x,y) = x + y
and [F](x,y) = y + 1,
the rules in {1,3}
are weakly decreasing and
the rules in {4,11}
are strictly decreasing.


- Consider the SCC {7}.
The usable rules are {1,3}.
By taking the polynomial interpretation
[0] = [nil] = 0,
[L#](x) = x,
[s](x) = x + 2
and [f](x,y) = x + y - 1,
we obtain a quasi-model of the usable rules.
Furthermore, dependency pair 7
is strictly decreasing.

Hence the TRS is terminating.