NO
The TRS could be proven non-terminating. The proof took 349 ms.
The following reduction sequence is a witness for non-termination:
f#(__x, __x) →* f#(__x, __x)
The following DP Processors were used
Problem 1 was processed with processor BackwardInstantiation (4ms).
| – Problem 2 was processed with processor ForwardInstantiation (3ms).
| | – Problem 3 was processed with processor BackwardInstantiation (3ms).
| | | – Problem 4 was processed with processor ForwardInstantiation (9ms).
| | | | – Problem 5 was processed with processor BackwardInstantiation (7ms).
| | | | | – Problem 6 was processed with processor ForwardInstantiation (16ms).
| | | | | | – Problem 7 remains open; application of the following processors failed [Propagation (26ms)].
Problem 1: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| f#(x, y) | → | f#(x, x) | | f#(s(x), y) | → | f#(y, x) |
Rewrite Rules
| f(x, y) | → | f(x, x) | | f(s(x), y) | → | f(y, x) |
Original Signature
Termination of terms over the following signature is verified: f, s
Strategy
Instantiation
For all potential predecessors l → r of the rule f
#(
x,
y) → f
#(
x,
x) on dependency pair chains it holds that:
- f#(x, y) matches r,
- all variables of f#(x, y) are embedded in constructor contexts, i.e., each subterm of f#(x, y), containing a variable is rooted by a constructor symbol.
Thus, f
#(
x,
y) → f
#(
x,
x) is replaced by instances determined through the above matching. These instances are:
| f#(_x, _x) → f#(_x, _x) | f#(_y, _x) → f#(_y, _y) |
Problem 2: ForwardInstantiation
Dependency Pair Problem
Dependency Pairs
| f#(_x, _x) | → | f#(_x, _x) | | f#(_y, _x) | → | f#(_y, _y) |
| f#(s(x), y) | → | f#(y, x) |
Rewrite Rules
| f(x, y) | → | f(x, x) | | f(s(x), y) | → | f(y, x) |
Original Signature
Termination of terms over the following signature is verified: f, s
Strategy
Instantiation
For all potential successors l → r of the rule f
#(s(
x),
y) → f
#(
y,
x) on dependency pair chains it holds that:
- f#(y, x) matches l,
- all variables of f#(y, x) are embedded in constructor contexts, i.e., each subterm of f#(y, x) containing a variable is rooted by a constructor symbol.
Thus, f
#(s(
x),
y) → f
#(
y,
x) is replaced by instances determined through the above matching. These instances are:
| f#(s(x), s(_x)) → f#(s(_x), x) | f#(s(x), y) → f#(y, x) |
| f#(s(x), x) → f#(x, x) |
Problem 3: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| f#(_x, _x) | → | f#(_x, _x) | | f#(_y, _x) | → | f#(_y, _y) |
| f#(s(x), s(_x)) | → | f#(s(_x), x) | | f#(s(x), y) | → | f#(y, x) |
| f#(s(x), x) | → | f#(x, x) |
Rewrite Rules
| f(x, y) | → | f(x, x) | | f(s(x), y) | → | f(y, x) |
Original Signature
Termination of terms over the following signature is verified: f, s
Strategy
Instantiation
For all potential predecessors l → r of the rule f
#(
_y,
_x) → f
#(
_y,
_y) on dependency pair chains it holds that:
- f#(_y, _x) matches r,
- all variables of f#(_y, _x) are embedded in constructor contexts, i.e., each subterm of f#(_y, _x), containing a variable is rooted by a constructor symbol.
Thus, f
#(
_y,
_x) → f
#(
_y,
_y) is replaced by instances determined through the above matching. These instances are:
| f#(__x, __x) → f#(__x, __x) | f#(__y, __y) → f#(__y, __y) |
| f#(y, x) → f#(y, y) | f#(x, x) → f#(x, x) |
| f#(s(___x), __x) → f#(s(___x), s(___x)) |
Problem 4: ForwardInstantiation
Dependency Pair Problem
Dependency Pairs
| f#(_x, _x) | → | f#(_x, _x) | | f#(__x, __x) | → | f#(__x, __x) |
| f#(__y, __y) | → | f#(__y, __y) | | f#(s(x), s(_x)) | → | f#(s(_x), x) |
| f#(y, x) | → | f#(y, y) | | f#(x, x) | → | f#(x, x) |
| f#(s(___x), __x) | → | f#(s(___x), s(___x)) | | f#(s(x), x) | → | f#(x, x) |
| f#(s(x), y) | → | f#(y, x) |
Rewrite Rules
| f(x, y) | → | f(x, x) | | f(s(x), y) | → | f(y, x) |
Original Signature
Termination of terms over the following signature is verified: f, s
Strategy
Instantiation
For all potential successors l → r of the rule f
#(s(
x),
y) → f
#(
y,
x) on dependency pair chains it holds that:
- f#(y, x) matches l,
- all variables of f#(y, x) are embedded in constructor contexts, i.e., each subterm of f#(y, x) containing a variable is rooted by a constructor symbol.
Thus, f
#(s(
x),
y) → f
#(
y,
x) is replaced by instances determined through the above matching. These instances are:
| f#(s(x), s(x)) → f#(s(x), x) | f#(s(x), s(___x)) → f#(s(___x), x) |
| f#(s(x), s(_x)) → f#(s(_x), x) | f#(s(s(__x)), s(_x)) → f#(s(_x), s(__x)) |
| f#(s(x), y) → f#(y, x) | f#(s(x), x) → f#(x, x) |
Problem 5: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| f#(s(x), s(x)) | → | f#(s(x), x) | | f#(_x, _x) | → | f#(_x, _x) |
| f#(s(x), s(___x)) | → | f#(s(___x), x) | | f#(__x, __x) | → | f#(__x, __x) |
| f#(__y, __y) | → | f#(__y, __y) | | f#(s(x), s(_x)) | → | f#(s(_x), x) |
| f#(y, x) | → | f#(y, y) | | f#(s(___x), __x) | → | f#(s(___x), s(___x)) |
| f#(x, x) | → | f#(x, x) | | f#(s(s(__x)), s(_x)) | → | f#(s(_x), s(__x)) |
| f#(s(x), x) | → | f#(x, x) | | f#(s(x), y) | → | f#(y, x) |
Rewrite Rules
| f(x, y) | → | f(x, x) | | f(s(x), y) | → | f(y, x) |
Original Signature
Termination of terms over the following signature is verified: f, s
Strategy
Instantiation
For all potential predecessors l → r of the rule f
#(
y,
x) → f
#(
y,
y) on dependency pair chains it holds that:
- f#(y, x) matches r,
- all variables of f#(y, x) are embedded in constructor contexts, i.e., each subterm of f#(y, x), containing a variable is rooted by a constructor symbol.
Thus, f
#(
y,
x) → f
#(
y,
y) is replaced by instances determined through the above matching. These instances are:
| f#(s(_x), _x) → f#(s(_x), s(_x)) | f#(s(___x), s(___x)) → f#(s(___x), s(___x)) |
| f#(s(__x), _x) → f#(s(__x), s(__x)) | f#(_x, _x) → f#(_x, _x) |
| f#(_y, _x) → f#(_y, _y) | f#(s(_x), s(__x)) → f#(s(_x), s(_x)) |
| f#(__x, __x) → f#(__x, __x) | f#(__y, __y) → f#(__y, __y) |
| f#(s(____x), _x) → f#(s(____x), s(____x)) | f#(_y, _y) → f#(_y, _y) |
Problem 6: ForwardInstantiation
Dependency Pair Problem
Dependency Pairs
| f#(s(__x), _x) | → | f#(s(__x), s(__x)) | | f#(__x, __x) | → | f#(__x, __x) |
| f#(s(s(__x)), s(_x)) | → | f#(s(_x), s(__x)) | | f#(s(___x), __x) | → | f#(s(___x), s(___x)) |
| f#(_y, _y) | → | f#(_y, _y) | | f#(s(x), y) | → | f#(y, x) |
| f#(s(x), s(x)) | → | f#(s(x), x) | | f#(s(_x), _x) | → | f#(s(_x), s(_x)) |
| f#(s(___x), s(___x)) | → | f#(s(___x), s(___x)) | | f#(s(x), s(___x)) | → | f#(s(___x), x) |
| f#(_x, _x) | → | f#(_x, _x) | | f#(s(_x), s(__x)) | → | f#(s(_x), s(_x)) |
| f#(_y, _x) | → | f#(_y, _y) | | f#(__y, __y) | → | f#(__y, __y) |
| f#(s(x), s(_x)) | → | f#(s(_x), x) | | f#(x, x) | → | f#(x, x) |
| f#(s(____x), _x) | → | f#(s(____x), s(____x)) | | f#(s(x), x) | → | f#(x, x) |
Rewrite Rules
| f(x, y) | → | f(x, x) | | f(s(x), y) | → | f(y, x) |
Original Signature
Termination of terms over the following signature is verified: f, s
Strategy
Instantiation
For all potential successors l → r of the rule f
#(s(
x),
y) → f
#(
y,
x) on dependency pair chains it holds that:
- f#(y, x) matches l,
- all variables of f#(y, x) are embedded in constructor contexts, i.e., each subterm of f#(y, x) containing a variable is rooted by a constructor symbol.
Thus, f
#(s(
x),
y) → f
#(
y,
x) is replaced by instances determined through the above matching. These instances are:
| f#(s(x), s(x)) → f#(s(x), x) | f#(s(s(_x)), s(_x)) → f#(s(_x), s(_x)) |
| f#(s(x), s(__x)) → f#(s(__x), x) | f#(s(s(___x)), s(___x)) → f#(s(___x), s(___x)) |
| f#(s(x), s(___x)) → f#(s(___x), x) | f#(s(x), s(____x)) → f#(s(____x), x) |
| f#(s(x), s(_x)) → f#(s(_x), x) | f#(s(s(__x)), s(_x)) → f#(s(_x), s(__x)) |
| f#(s(s(____x)), s(_x)) → f#(s(_x), s(____x)) | f#(s(s(_x)), s(s(__x))) → f#(s(s(__x)), s(_x)) |
| f#(s(x), y) → f#(y, x) | f#(s(x), x) → f#(x, x) |