Consider the TRS R consisting of the rewrite rules

1: p(s(x)) -> x
2: fact(0) -> s(0)
3: fact(s(x)) -> s(x) * fact(p(s(x)))
4: 0 * y -> 0
5: s(x) * y -> (x * y) + y
6: x + 0 -> x
7: x + s(y) -> s(x + y)

There are 6 dependency pairs:

8: FACT(s(x)) -> s(x) *# fact(p(s(x)))
9: FACT(s(x)) -> FACT(p(s(x)))
10: FACT(s(x)) -> P(s(x))
11: s(x) *# y -> (x * y) +# y
12: s(x) *# y -> x *# y
13: x +# s(y) -> x +# y

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

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

- 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 {9}.
The usable rules are {1}.
By taking the polynomial interpretation
[FACT](x) = x,
[s](x) = x + 1
and [p](x) = x - 1,
we obtain a quasi-model of the usable rule.
Furthermore, dependency pair 9
is strictly decreasing.

Hence the TRS is terminating.