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

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

f#(f(f(f(___x)))) →* f#(f(f(f(___x))))

The following DP Processors were used


Problem 1 was processed with processor BackwardInstantiation (4ms).
 | – Problem 2 was processed with processor ForwardInstantiation (4ms).
 |    | – Problem 3 was processed with processor BackwardInstantiation (10ms).
 |    |    | – Problem 4 was processed with processor ForwardInstantiation (7ms).
 |    |    |    | – Problem 5 was processed with processor BackwardInstantiation (11ms).
 |    |    |    |    | – Problem 6 was processed with processor ForwardInstantiation (21ms).
 |    |    |    |    |    | – Problem 7 remains open; application of the following processors failed [Propagation (7ms)].

Problem 1: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

f#(x)f#(f(x))f#(x)f#(x)

Rewrite Rules

f(x)f(f(x))

Original Signature

Termination of terms over the following signature is verified: f

Strategy


Instantiation

For all potential predecessors l → r of the rule f#(x) → f#(f(x)) on dependency pair chains it holds that: Thus, f#(x) → f#(f(x)) is replaced by instances determined through the above matching. These instances are:
f#(_x) → f#(f(_x))f#(f(_x)) → f#(f(f(_x)))

Instantiation

For all potential predecessors l → r of the rule f#(x) → f#(x) on dependency pair chains it holds that: Thus, f#(x) → f#(x) is replaced by instances determined through the above matching. These instances are:
f#(_x) → f#(_x)f#(f(_x)) → f#(f(_x))

Problem 2: ForwardInstantiation



Dependency Pair Problem

Dependency Pairs

f#(_x)f#(_x)f#(_x)f#(f(_x))
f#(f(_x))f#(f(_x))f#(f(_x))f#(f(f(_x)))

Rewrite Rules

f(x)f(f(x))

Original Signature

Termination of terms over the following signature is verified: f

Strategy


Instantiation

For all potential successors l → r of the rule f#(_x) → f#(_x) on dependency pair chains it holds that: Thus, f#(_x) → f#(_x) is replaced by instances determined through the above matching. These instances are:
f#(_x) → f#(_x)f#(f(__x)) → f#(f(__x))

Problem 3: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

f#(_x)f#(f(_x))f#(_x)f#(_x)
f#(f(_x))f#(f(_x))f#(f(_x))f#(f(f(_x)))
f#(f(__x))f#(f(__x))

Rewrite Rules

f(x)f(f(x))

Original Signature

Termination of terms over the following signature is verified: f

Strategy


Instantiation

For all potential predecessors l → r of the rule f#(_x) → f#(_x) on dependency pair chains it holds that: Thus, f#(_x) → f#(_x) is replaced by instances determined through the above matching. These instances are:
f#(f(f(__x))) → f#(f(f(__x)))f#(__x) → f#(__x)
f#(f(__x)) → f#(f(__x))

Instantiation

For all potential predecessors l → r of the rule f#(_x) → f#(f(_x)) on dependency pair chains it holds that: Thus, f#(_x) → f#(f(_x)) is replaced by instances determined through the above matching. These instances are:
f#(f(f(__x))) → f#(f(f(f(__x))))f#(f(__x)) → f#(f(f(__x)))
f#(__x) → f#(f(__x))

Problem 4: ForwardInstantiation



Dependency Pair Problem

Dependency Pairs

f#(f(f(__x)))f#(f(f(f(__x))))f#(f(_x))f#(f(_x))
f#(f(_x))f#(f(f(_x)))f#(f(__x))f#(f(f(__x)))
f#(f(__x))f#(f(__x))f#(f(f(__x)))f#(f(f(__x)))
f#(__x)f#(__x)f#(__x)f#(f(__x))

Rewrite Rules

f(x)f(f(x))

Original Signature

Termination of terms over the following signature is verified: f

Strategy


Instantiation

For all potential successors l → r of the rule f#(__x) → f#(__x) on dependency pair chains it holds that: Thus, f#(__x) → f#(__x) is replaced by instances determined through the above matching. These instances are:
f#(f(___x)) → f#(f(___x))f#(f(_x)) → f#(f(_x))
f#(f(f(___x))) → f#(f(f(___x)))f#(__x) → f#(__x)

Problem 5: BackwardInstantiation



Dependency Pair Problem

Dependency Pairs

f#(f(f(__x)))f#(f(f(f(__x))))f#(f(___x))f#(f(___x))
f#(f(_x))f#(f(_x))f#(f(f(___x)))f#(f(f(___x)))
f#(f(__x))f#(f(f(__x)))f#(f(_x))f#(f(f(_x)))
f#(f(f(__x)))f#(f(f(__x)))f#(f(__x))f#(f(__x))
f#(__x)f#(__x)f#(__x)f#(f(__x))

Rewrite Rules

f(x)f(f(x))

Original Signature

Termination of terms over the following signature is verified: f

Strategy


Instantiation

For all potential predecessors l → r of the rule f#(__x) → f#(__x) on dependency pair chains it holds that: Thus, f#(__x) → f#(__x) is replaced by instances determined through the above matching. These instances are:
f#(f(f(f(___x)))) → f#(f(f(f(___x))))f#(f(___x)) → f#(f(___x))
f#(f(f(___x))) → f#(f(f(___x)))f#(f(_x)) → f#(f(_x))
f#(f(f(_x))) → f#(f(f(_x)))f#(___x) → f#(___x)

Instantiation

For all potential predecessors l → r of the rule f#(__x) → f#(f(__x)) on dependency pair chains it holds that: Thus, f#(__x) → f#(f(__x)) is replaced by instances determined through the above matching. These instances are:
f#(f(f(f(___x)))) → f#(f(f(f(f(___x)))))f#(f(___x)) → f#(f(f(___x)))
f#(___x) → f#(f(___x))f#(f(_x)) → f#(f(f(_x)))
f#(f(f(___x))) → f#(f(f(f(___x))))f#(f(f(_x))) → f#(f(f(f(_x))))

Problem 6: ForwardInstantiation



Dependency Pair Problem

Dependency Pairs

f#(f(f(f(___x))))f#(f(f(f(f(___x)))))f#(f(___x))f#(f(f(___x)))
f#(f(f(f(___x))))f#(f(f(f(___x))))f#(f(_x))f#(f(f(_x)))
f#(f(__x))f#(f(f(__x)))f#(f(f(_x)))f#(f(f(_x)))
f#(f(__x))f#(f(__x))f#(f(f(__x)))f#(f(f(__x)))
f#(f(f(___x)))f#(f(f(f(___x))))f#(f(f(__x)))f#(f(f(f(__x))))
f#(f(___x))f#(f(___x))f#(f(f(___x)))f#(f(f(___x)))
f#(f(_x))f#(f(_x))f#(___x)f#(f(___x))
f#(___x)f#(___x)f#(f(f(_x)))f#(f(f(f(_x))))

Rewrite Rules

f(x)f(f(x))

Original Signature

Termination of terms over the following signature is verified: f

Strategy


Instantiation

For all potential successors l → r of the rule f#(___x) → f#(___x) on dependency pair chains it holds that: Thus, f#(___x) → f#(___x) is replaced by instances determined through the above matching. These instances are:
f#(f(____x)) → f#(f(____x))f#(f(_x)) → f#(f(_x))
f#(f(f(____x))) → f#(f(f(____x)))f#(f(f(_x))) → f#(f(f(_x)))
f#(___x) → f#(___x)f#(f(f(__x))) → f#(f(f(__x)))
f#(f(__x)) → f#(f(__x))f#(f(f(f(____x)))) → f#(f(f(f(____x))))