TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60018 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (44ms).
| – Problem 2 was processed with processor SubtermCriterion (2ms).
| – Problem 3 was processed with processor SubtermCriterion (0ms).
| – Problem 4 was processed with processor BackwardInstantiation (2ms).
| | – Problem 5 was processed with processor BackwardInstantiation (4ms).
| | | – Problem 6 was processed with processor Propagation (1ms).
| | | | – Problem 7 remains open; application of the following processors failed [ForwardNarrowing (1ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (1ms)].
The following open problems remain:
Open Dependency Pair Problem 4
Dependency Pairs
| 1024_1#(x) | → | if#(lt(x, 10), x) | | if#(true, x) | → | 1024_1#(s(x)) |
Rewrite Rules
| 1024 | → | 1024_1(0) | | 1024_1(x) | → | if(lt(x, 10), x) |
| if(true, x) | → | double(1024_1(s(x))) | | if(false, x) | → | s(0) |
| lt(0, s(y)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | 10 | → | double(s(double(s(s(0))))) |
Original Signature
Termination of terms over the following signature is verified: 10, 0, s, if, false, true, lt, double, 1024, 1024_1
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| 1024# | → | 1024_1#(0) | | 1024_1#(x) | → | if#(lt(x, 10), x) |
| 1024_1#(x) | → | lt#(x, 10) | | if#(true, x) | → | 1024_1#(s(x)) |
| double#(s(x)) | → | double#(x) | | lt#(s(x), s(y)) | → | lt#(x, y) |
| 10# | → | double#(s(s(0))) | | if#(true, x) | → | double#(1024_1(s(x))) |
| 10# | → | double#(s(double(s(s(0))))) | | 1024_1#(x) | → | 10# |
Rewrite Rules
| 1024 | → | 1024_1(0) | | 1024_1(x) | → | if(lt(x, 10), x) |
| if(true, x) | → | double(1024_1(s(x))) | | if(false, x) | → | s(0) |
| lt(0, s(y)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | 10 | → | double(s(double(s(s(0))))) |
Original Signature
Termination of terms over the following signature is verified: 10, 0, s, if, true, false, lt, double, 1024, 1024_1
Strategy
The following SCCs where found
| 1024_1#(x) → if#(lt(x, 10), x) | if#(true, x) → 1024_1#(s(x)) |
| double#(s(x)) → double#(x) |
| lt#(s(x), s(y)) → lt#(x, y) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| double#(s(x)) | → | double#(x) |
Rewrite Rules
| 1024 | → | 1024_1(0) | | 1024_1(x) | → | if(lt(x, 10), x) |
| if(true, x) | → | double(1024_1(s(x))) | | if(false, x) | → | s(0) |
| lt(0, s(y)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | 10 | → | double(s(double(s(s(0))))) |
Original Signature
Termination of terms over the following signature is verified: 10, 0, s, if, true, false, lt, double, 1024, 1024_1
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| double#(s(x)) | → | double#(x) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| lt#(s(x), s(y)) | → | lt#(x, y) |
Rewrite Rules
| 1024 | → | 1024_1(0) | | 1024_1(x) | → | if(lt(x, 10), x) |
| if(true, x) | → | double(1024_1(s(x))) | | if(false, x) | → | s(0) |
| lt(0, s(y)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | 10 | → | double(s(double(s(s(0))))) |
Original Signature
Termination of terms over the following signature is verified: 10, 0, s, if, true, false, lt, double, 1024, 1024_1
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| lt#(s(x), s(y)) | → | lt#(x, y) |
Problem 4: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| 1024_1#(x) | → | if#(lt(x, 10), x) | | if#(true, x) | → | 1024_1#(s(x)) |
Rewrite Rules
| 1024 | → | 1024_1(0) | | 1024_1(x) | → | if(lt(x, 10), x) |
| if(true, x) | → | double(1024_1(s(x))) | | if(false, x) | → | s(0) |
| lt(0, s(y)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | 10 | → | double(s(double(s(s(0))))) |
Original Signature
Termination of terms over the following signature is verified: 10, 0, s, if, true, false, lt, double, 1024, 1024_1
Strategy
Instantiation
For all potential predecessors l → r of the rule 1024_1
#(
x) → if
#(lt(
x, 10),
x) on dependency pair chains it holds that:
- 1024_1#(x) matches r,
- all variables of 1024_1#(x) are embedded in constructor contexts, i.e., each subterm of 1024_1#(x), containing a variable is rooted by a constructor symbol.
Thus, 1024_1
#(
x) → if
#(lt(
x, 10),
x) is replaced by instances determined through the above matching. These instances are:
| 1024_1#(s(_x)) → if#(lt(s(_x), 10), s(_x)) |
Problem 5: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| 1024_1#(s(_x)) | → | if#(lt(s(_x), 10), s(_x)) | | if#(true, x) | → | 1024_1#(s(x)) |
Rewrite Rules
| 1024 | → | 1024_1(0) | | 1024_1(x) | → | if(lt(x, 10), x) |
| if(true, x) | → | double(1024_1(s(x))) | | if(false, x) | → | s(0) |
| lt(0, s(y)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | 10 | → | double(s(double(s(s(0))))) |
Original Signature
Termination of terms over the following signature is verified: 10, 0, s, if, false, true, lt, double, 1024, 1024_1
Strategy
Instantiation
For all potential predecessors l → r of the rule 1024_1
#(s(
_x)) → if
#(lt(s(
_x), 10), s(
_x)) on dependency pair chains it holds that:
- 1024_1#(s(_x)) matches r,
- all variables of 1024_1#(s(_x)) are embedded in constructor contexts, i.e., each subterm of 1024_1#(s(_x)), containing a variable is rooted by a constructor symbol.
Thus, 1024_1
#(s(
_x)) → if
#(lt(s(
_x), 10), s(
_x)) is replaced by instances determined through the above matching. These instances are:
| 1024_1#(s(x)) → if#(lt(s(x), 10), s(x)) |
Problem 6: Propagation
Dependency Pair Problem
Dependency Pairs
| if#(true, x) | → | 1024_1#(s(x)) | | 1024_1#(s(x)) | → | if#(lt(s(x), 10), s(x)) |
Rewrite Rules
| 1024 | → | 1024_1(0) | | 1024_1(x) | → | if(lt(x, 10), x) |
| if(true, x) | → | double(1024_1(s(x))) | | if(false, x) | → | s(0) |
| lt(0, s(y)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | 10 | → | double(s(double(s(s(0))))) |
Original Signature
Termination of terms over the following signature is verified: 10, 0, s, if, true, false, lt, double, 1024, 1024_1
Strategy
The dependency pairs if
#(true,
x) → 1024_1
#(s(
x)) and 1024_1
#(s(
x)) → if
#(lt(s(
x), 10), s(
x)) are consolidated into the rule if
#(true,
x) → if
#(lt(s(
x), 10), s(
x)) .
This is possible as
- all subterms of 1024_1#(s(x)) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in 1024_1#(s(x)), but non-replacing in both if#(true, x) and if#(lt(s(x), 10), s(x))
The dependency pairs if
#(true,
x) → 1024_1
#(s(
x)) and 1024_1
#(s(
x)) → if
#(lt(s(
x), 10), s(
x)) are consolidated into the rule if
#(true,
x) → if
#(lt(s(
x), 10), s(
x)) .
This is possible as
- all subterms of 1024_1#(s(x)) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in 1024_1#(s(x)), but non-replacing in both if#(true, x) and if#(lt(s(x), 10), s(x))
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| if#(true, x) → 1024_1#(s(x)) | if#(true, x) → if#(lt(s(x), 10), s(x)) |
| 1024_1#(s(x)) → if#(lt(s(x), 10), s(x)) | |