Term Rewriting System R:
[x]
f(g(x), s(0)) -> f(g(x), g(x))
g(s(x)) -> s(g(x))
g(0) -> 0

Termination of R to be shown.

R
Dependency Pair Analysis

R contains the following Dependency Pairs:

F(g(x), s(0)) -> F(g(x), g(x))
G(s(x)) -> G(x)

Furthermore, R contains two SCCs.

R
DPs
→DP Problem 1
Polynomial Ordering
→DP Problem 2
Remaining

Dependency Pair:

G(s(x)) -> G(x)

Rules:

f(g(x), s(0)) -> f(g(x), g(x))
g(s(x)) -> s(g(x))
g(0) -> 0

The following dependency pair can be strictly oriented:

G(s(x)) -> G(x)

Additionally, the following rules can be oriented:

f(g(x), s(0)) -> f(g(x), g(x))
g(s(x)) -> s(g(x))
g(0) -> 0

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(0) =  0 POL(g(x1)) =  x1 POL(G(x1)) =  x1 POL(s(x1)) =  1 + x1 POL(f(x1, x2)) =  0

resulting in one new DP problem.

R
DPs
→DP Problem 1
Polo
→DP Problem 3
Dependency Graph
→DP Problem 2
Remaining

Dependency Pair:

Rules:

f(g(x), s(0)) -> f(g(x), g(x))
g(s(x)) -> s(g(x))
g(0) -> 0

Using the Dependency Graph resulted in no new DP problems.

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Remaining Obligation(s)

The following remains to be proven:
Dependency Pair:

F(g(x), s(0)) -> F(g(x), g(x))

Rules:

f(g(x), s(0)) -> f(g(x), g(x))
g(s(x)) -> s(g(x))
g(0) -> 0

Termination of R could not be shown.
Duration:
0:00 minutes