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

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

length1# →* length1#

The following DP Processors were used


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

Problem 1: Propagation



Dependency Pair Problem

Dependency Pairs

length1#length#length#length1#

Rewrite Rules

from(X)cons(X)length0
lengths(length1)length1length

Original Signature

Termination of terms over the following signature is verified: 0, s, length, from, length1, cons

Strategy


The dependency pairs length1# → length# and length# → length1# are consolidated into the rule length1# → length1# .

This is possible as

The dependency pairs length1# → length# and length# → length1# are consolidated into the rule length1# → length1# .

This is possible as

The dependency pairs length# → length1# and length1# → length# are consolidated into the rule length# → length# .

This is possible as

The dependency pairs length# → length1# and length1# → length# are consolidated into the rule length# → length# .

This is possible as


Summary

Removed Dependency PairsAdded Dependency Pairs
length1# → length#length1# → length1#
length# → length1#length# → length#