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

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

f#(0) →* f#(0)

The following DP Processors were used


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

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

f#(s(0))f#(p(s(0)))f#(s(0))p#(s(0))
f#(0)f#(s(0))

Rewrite Rules

f(0)cons(0, f(s(0)))f(s(0))f(p(s(0)))
p(s(0))0

Original Signature

Termination of terms over the following signature is verified: f, 0, s, p, cons

Strategy


Parameters


The following SCCs where found

f#(s(0)) → f#(p(s(0)))f#(0) → f#(s(0))

Problem 2: ForwardNarrowing



Dependency Pair Problem

Dependency Pairs

f#(s(0))f#(p(s(0)))f#(0)f#(s(0))

Rewrite Rules

f(0)cons(0, f(s(0)))f(s(0))f(p(s(0)))
p(s(0))0

Original Signature

Termination of terms over the following signature is verified: f, 0, s, p, cons

Strategy


Parameters


The right-hand side of the rule f#(s(0)) → f#(p(s(0))) is 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#(0) 
Thus, the rule f#(s(0)) → f#(p(s(0))) is replaced by the following rules:
f#(s(0)) → f#(0)

Problem 3: Propagation



Dependency Pair Problem

Dependency Pairs

f#(s(0))f#(0)f#(0)f#(s(0))

Rewrite Rules

f(0)cons(0, f(s(0)))f(s(0))f(p(s(0)))
p(s(0))0

Original Signature

Termination of terms over the following signature is verified: f, 0, s, p, cons

Strategy


The dependency pairs f#(s(0)) → f#(0) and f#(0) → f#(s(0)) are consolidated into the rule f#(s(0)) → f#(s(0)) .

This is possible as

The dependency pairs f#(s(0)) → f#(0) and f#(0) → f#(s(0)) are consolidated into the rule f#(s(0)) → f#(s(0)) .

This is possible as

The dependency pairs f#(0) → f#(s(0)) and f#(s(0)) → f#(0) are consolidated into the rule f#(0) → f#(0) .

This is possible as

The dependency pairs f#(0) → f#(s(0)) and f#(s(0)) → f#(0) are consolidated into the rule f#(0) → f#(0) .

This is possible as


Summary

Removed Dependency PairsAdded Dependency Pairs
f#(s(0)) → f#(0)f#(0) → f#(0)
f#(0) → f#(s(0))f#(s(0)) → f#(s(0))