YES
The TRS could be proven terminating. The proof took 649 ms.
The following DP Processors were used
Problem 1 was processed with processor BackwardInstantiation (3ms).
| – Problem 2 was processed with processor BackwardInstantiation (1ms).
| | – Problem 5 was processed with processor Propagation (2ms).
| – Problem 3 was processed with processor BackwardsNarrowing (42ms).
| | – Problem 4 was processed with processor BackwardInstantiation (9ms).
Problem 1: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| g#(0, 1, x) | → | f#(x, x, x) | | f#(x, y, z) | → | g#(x, y, z) |
Rewrite Rules
| f(x, y, z) | → | g(x, y, z) | | g(0, 1, x) | → | f(x, x, x) |
Original Signature
Termination of terms over the following signature is verified: f, g, 1, 0
Strategy
Instantiation
For all potential predecessors l → r of the rule f
#(
x,
y,
z) → g
#(
x,
y,
z) on dependency pair chains it holds that:
- f#(x, y, z) matches r,
- all variables of f#(x, y, z) are embedded in constructor contexts, i.e., each subterm of f#(x, y, z), containing a variable is rooted by a constructor symbol.
Thus, f
#(
x,
y,
z) → g
#(
x,
y,
z) is replaced by instances determined through the above matching. These instances are:
| f#(_x, _x, _x) → g#(_x, _x, _x) |
Problem 2: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| g#(0, 1, x) | → | f#(x, x, x) | | f#(_x, _x, _x) | → | g#(_x, _x, _x) |
Rewrite Rules
| f(x, y, z) | → | g(x, y, z) | | g(0, 1, x) | → | f(x, x, x) |
Original Signature
Termination of terms over the following signature is verified: f, g, 1, 0
Strategy
Instantiation
For all potential predecessors l → r of the rule f
#(
_x,
_x,
_x) → g
#(
_x,
_x,
_x) on dependency pair chains it holds that:
- f#(_x, _x, _x) matches r,
- all variables of f#(_x, _x, _x) are embedded in constructor contexts, i.e., each subterm of f#(_x, _x, _x), containing a variable is rooted by a constructor symbol.
Thus, f
#(
_x,
_x,
_x) → g
#(
_x,
_x,
_x) is replaced by instances determined through the above matching. These instances are:
| f#(x, x, x) → g#(x, x, x) |
Problem 5: Propagation
Dependency Pair Problem
Dependency Pairs
| g#(0, 1, x) | → | f#(x, x, x) | | f#(x, x, x) | → | g#(x, x, x) |
Rewrite Rules
| f(x, y, z) | → | g(x, y, z) | | g(0, 1, x) | → | f(x, x, x) |
Original Signature
Termination of terms over the following signature is verified: f, g, 1, 0
Strategy
The dependency pairs g
#(0, 1,
x) → f
#(
x,
x,
x) and f
#(
x,
x,
x) → g
#(
x,
x,
x) are consolidated into the rule g
#(0, 1,
x) → g
#(
x,
x,
x) .
This is possible as
- all subterms of f#(x, x, x) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in f#(x, x, x), but non-replacing in both g#(0, 1, x) and g#(x, x, x)
The dependency pairs g
#(0, 1,
x) → f
#(
x,
x,
x) and f
#(
x,
x,
x) → g
#(
x,
x,
x) are consolidated into the rule g
#(0, 1,
x) → g
#(
x,
x,
x) .
This is possible as
- all subterms of f#(x, x, x) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in f#(x, x, x), but non-replacing in both g#(0, 1, x) and g#(x, x, x)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| g#(0, 1, x) → f#(x, x, x) | g#(0, 1, x) → g#(x, x, x) |
| f#(x, x, x) → g#(x, x, x) | |
Problem 3: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| g#(0, 1, x) | → | f#(x, x, x) | | f#(_x, _x, _x) | → | g#(_x, _x, _x) |
Rewrite Rules
| f(x, y, z) | → | g(x, y, z) | | g(0, 1, x) | → | f(x, x, x) |
Original Signature
Termination of terms over the following signature is verified: f, g, 1, 0
Strategy
The left-hand side of the rule g
#(0, 1,
x) → f
#(
x,
x,
x) is backward 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 |
|---|
Thus, the rule g
#(0, 1,
x) → f
#(
x,
x,
x) is deleted.
Problem 4: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| f#(_x, _x, _x) | → | g#(_x, _x, _x) |
Rewrite Rules
| f(x, y, z) | → | g(x, y, z) | | g(0, 1, x) | → | f(x, x, x) |
Original Signature
Termination of terms over the following signature is verified: f, g, 1, 0
Strategy
Instantiation
For all potential predecessors l → r of the rule f
#(
_x,
_x,
_x) → g
#(
_x,
_x,
_x) on dependency pair chains it holds that:
- f#(_x, _x, _x) matches r,
- all variables of f#(_x, _x, _x) are embedded in constructor contexts, i.e., each subterm of f#(_x, _x, _x), containing a variable is rooted by a constructor symbol.
Thus, f
#(
_x,
_x,
_x) → g
#(
_x,
_x,
_x) is replaced by instances determined through the above matching. These instances are: