NO

The TRS could be proven non-terminating. The proof took 1363 ms.

The following reduction sequence is a witness for non-termination:

f#(g(0, 0)) →* f#(g(0, 0))

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (0ms).
 | – Problem 2 was processed with processor BackwardsNarrowing (1ms).
 |    | – Problem 3 was processed with processor BackwardsNarrowing (1ms).
 |    |    | – Problem 4 remains open; application of the following processors failed [BackwardsNarrowing (1ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (1ms), BackwardsNarrowing (0ms), BackwardInstantiation (0ms), ForwardInstantiation (0ms), Propagation (2ms)].

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

f#(s(x))g#(x, x)g#(0, 1)0#
f#(s(x))f#(g(x, x))

Rewrite Rules

f(s(x))f(g(x, x))g(0, 1)s(0)
01

Original Signature

Termination of terms over the following signature is verified: f, g, 1, 0, s

Strategy


The following SCCs where found

f#(s(x)) → f#(g(x, x))

Problem 2: BackwardsNarrowing



Dependency Pair Problem

Dependency Pairs

f#(s(x))f#(g(x, x))

Rewrite Rules

f(s(x))f(g(x, x))g(0, 1)s(0)
01

Original Signature

Termination of terms over the following signature is verified: f, g, 1, 0, s

Strategy


The left-hand side of the rule f#(s(x)) → f#(g(x, x)) is backward narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
f#(g(0, 1)) 
Thus, the rule f#(s(x)) → f#(g(x, x)) is replaced by the following rules:
f#(g(0, 1)) → f#(g(0, 0))

Problem 3: BackwardsNarrowing



Dependency Pair Problem

Dependency Pairs

f#(g(0, 1))f#(g(0, 0))

Rewrite Rules

f(s(x))f(g(x, x))g(0, 1)s(0)
01

Original Signature

Termination of terms over the following signature is verified: f, g, 1, 0, s

Strategy


The left-hand side of the rule f#(g(0, 1)) → f#(g(0, 0)) is backward narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
Relevant TermsIrrelevant Terms
f#(g(0, 0)) 
Thus, the rule f#(g(0, 1)) → f#(g(0, 0)) is replaced by the following rules:
f#(g(0, 0)) → f#(g(0, 0))