NO
The TRS could be proven non-terminating. The proof took 340 ms.
The following reduction sequence is a witness for non-termination:
f#(h(____x21)) →* f#(h(____x21))
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (7ms).
| – Problem 2 was processed with processor ForwardNarrowing (1ms).
| | – Problem 3 was processed with processor BackwardInstantiation (2ms).
| | | – Problem 4 was processed with processor BackwardInstantiation (1ms).
| | | | – Problem 5 was processed with processor BackwardInstantiation (3ms).
| | | | | – Problem 6 remains open; application of the following processors failed [ForwardInstantiation (2ms), Propagation (1ms)].
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| f#(h(x)) | → | f#(i(x)) | | f#(h(x)) | → | i#(x) |
Rewrite Rules
| f(h(x)) | → | f(i(x)) | | f(i(x)) | → | a |
| i(x) | → | h(x) |
Original Signature
Termination of terms over the following signature is verified: f, a, h, i
Strategy
The following SCCs where found
Problem 2: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| f(h(x)) | → | f(i(x)) | | f(i(x)) | → | a |
| i(x) | → | h(x) |
Original Signature
Termination of terms over the following signature is verified: f, a, h, i
Strategy
The right-hand side of the rule f
#(h(
x)) → f
#(i(
x)) 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 Terms | Irrelevant Terms |
|---|
| f#(h(_x21)) | |
Thus, the rule f
#(h(
x)) → f
#(i(
x)) is replaced by the following rules:
| f#(h(_x21)) → f#(h(_x21)) |
Problem 3: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| f#(h(_x21)) | → | f#(h(_x21)) |
Rewrite Rules
| f(h(x)) | → | f(i(x)) | | f(i(x)) | → | a |
| i(x) | → | h(x) |
Original Signature
Termination of terms over the following signature is verified: f, a, h, i
Strategy
Instantiation
For all potential predecessors l → r of the rule f
#(h(
_x21)) → f
#(h(
_x21)) on dependency pair chains it holds that:
- f#(h(_x21)) matches r,
- all variables of f#(h(_x21)) are embedded in constructor contexts, i.e., each subterm of f#(h(_x21)), containing a variable is rooted by a constructor symbol.
Thus, f
#(h(
_x21)) → f
#(h(
_x21)) is replaced by instances determined through the above matching. These instances are:
| f#(h(__x21)) → f#(h(__x21)) |
Problem 4: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| f#(h(__x21)) | → | f#(h(__x21)) |
Rewrite Rules
| f(h(x)) | → | f(i(x)) | | f(i(x)) | → | a |
| i(x) | → | h(x) |
Original Signature
Termination of terms over the following signature is verified: f, a, h, i
Strategy
Instantiation
For all potential predecessors l → r of the rule f
#(h(
__x21)) → f
#(h(
__x21)) on dependency pair chains it holds that:
- f#(h(__x21)) matches r,
- all variables of f#(h(__x21)) are embedded in constructor contexts, i.e., each subterm of f#(h(__x21)), containing a variable is rooted by a constructor symbol.
Thus, f
#(h(
__x21)) → f
#(h(
__x21)) is replaced by instances determined through the above matching. These instances are:
| f#(h(___x21)) → f#(h(___x21)) |
Problem 5: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| f#(h(___x21)) | → | f#(h(___x21)) |
Rewrite Rules
| f(h(x)) | → | f(i(x)) | | f(i(x)) | → | a |
| i(x) | → | h(x) |
Original Signature
Termination of terms over the following signature is verified: f, a, h, i
Strategy
Instantiation
For all potential predecessors l → r of the rule f
#(h(
___x21)) → f
#(h(
___x21)) on dependency pair chains it holds that:
- f#(h(___x21)) matches r,
- all variables of f#(h(___x21)) are embedded in constructor contexts, i.e., each subterm of f#(h(___x21)), containing a variable is rooted by a constructor symbol.
Thus, f
#(h(
___x21)) → f
#(h(
___x21)) is replaced by instances determined through the above matching. These instances are:
| f#(h(____x21)) → f#(h(____x21)) |