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
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:
- f#(x) matches r,
- all variables of f#(x) are embedded in constructor contexts, i.e., each subterm of f#(x), containing a variable is rooted by a constructor symbol.
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:
- f#(x) matches r,
- all variables of f#(x) are embedded in constructor contexts, i.e., each subterm of f#(x), containing a variable is rooted by a constructor symbol.
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
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:
- f#(_x) matches l,
- all variables of f#(_x) are embedded in constructor contexts, i.e., each subterm of f#(_x) containing a variable is rooted by a constructor symbol.
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
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:
- f#(_x) matches r,
- all variables of f#(_x) are embedded in constructor contexts, i.e., each subterm of f#(_x), containing a variable is rooted by a constructor symbol.
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:
- f#(_x) matches r,
- all variables of f#(_x) are embedded in constructor contexts, i.e., each subterm of f#(_x), containing a variable is rooted by a constructor symbol.
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
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:
- f#(__x) matches l,
- all variables of f#(__x) are embedded in constructor contexts, i.e., each subterm of f#(__x) containing a variable is rooted by a constructor symbol.
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
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:
- f#(__x) matches r,
- all variables of f#(__x) are embedded in constructor contexts, i.e., each subterm of f#(__x), containing a variable is rooted by a constructor symbol.
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:
- f#(__x) matches r,
- all variables of f#(__x) are embedded in constructor contexts, i.e., each subterm of f#(__x), containing a variable is rooted by a constructor symbol.
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
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:
- f#(___x) matches l,
- all variables of f#(___x) are embedded in constructor contexts, i.e., each subterm of f#(___x) containing a variable is rooted by a constructor symbol.
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)))) |