Consider the TRS R consisting of the rewrite rules

1: x - 0 -> x
2: 0 - s(y) -> 0
3: s(x) - s(y) -> x - y
4: lt(x,0) -> false
5: lt(0,s(y)) -> true
6: lt(s(x),s(y)) -> lt(x,y)
7: if(true,x,y) -> x
8: if(false,x,y) -> y
9: div(x,0) -> 0
10: div(0,y) -> 0
11: div(s(x),s(y)) -> if(lt(x,y),0,s(div(x - y,s(y))))

There are 6 dependency pairs:

12: s(x) -# s(y) -> x -# y
13: LT(s(x),s(y)) -> LT(x,y)
14: DIV(s(x),s(y)) -> IF(lt(x,y),0,s(div(x - y,s(y))))
15: DIV(s(x),s(y)) -> LT(x,y)
16: DIV(s(x),s(y)) -> DIV(x - y,s(y))
17: DIV(s(x),s(y)) -> x -# y

The approximated dependency graph contains 3 SCCs:
{12},
{13}
and {16}.

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

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

- Consider the SCC {16}.
The usable rules are {1-3}.
By taking the polynomial interpretation
[0] = 1,
[-](x,y) = x,
[s](x) = x + 1
and [DIV](x,y) = x + y + 1,
the rules in {1,2}
are weakly decreasing and
the rules in {3,16}
are strictly decreasing.

Hence the TRS is terminating.