TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60137 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (52ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| | – Problem 5 was processed with processor PolynomialLinearRange4iUR (77ms).
| – Problem 4 was processed with processor BackwardInstantiation (2ms).
| | – Problem 6 was processed with processor BackwardInstantiation (1ms).
| | | – Problem 7 was processed with processor Propagation (3ms).
| | | | – Problem 8 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
| d#(x) | → | if#(le(x, nr), x) | | if#(true, x) | → | d#(s(x)) |
Rewrite Rules
| numbers | → | d(0) | | d(x) | → | if(le(x, nr), x) |
| if(true, x) | → | cons(x, d(s(x))) | | if(false, x) | → | nil |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | nr | → | ack(s(s(s(s(s(s(0)))))), 0) |
| ack(0, x) | → | s(x) | | ack(s(x), 0) | → | ack(x, s(0)) |
| ack(s(x), s(y)) | → | ack(x, ack(s(x), y)) |
Original Signature
Termination of terms over the following signature is verified: d, nr, 0, s, le, numbers, ack, if, false, true, nil, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| numbers# | → | d#(0) | | le#(s(x), s(y)) | → | le#(x, y) |
| d#(x) | → | if#(le(x, nr), x) | | ack#(s(x), s(y)) | → | ack#(x, ack(s(x), y)) |
| ack#(s(x), s(y)) | → | ack#(s(x), y) | | ack#(s(x), 0) | → | ack#(x, s(0)) |
| nr# | → | ack#(s(s(s(s(s(s(0)))))), 0) | | d#(x) | → | le#(x, nr) |
| if#(true, x) | → | d#(s(x)) | | d#(x) | → | nr# |
Rewrite Rules
| numbers | → | d(0) | | d(x) | → | if(le(x, nr), x) |
| if(true, x) | → | cons(x, d(s(x))) | | if(false, x) | → | nil |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | nr | → | ack(s(s(s(s(s(s(0)))))), 0) |
| ack(0, x) | → | s(x) | | ack(s(x), 0) | → | ack(x, s(0)) |
| ack(s(x), s(y)) | → | ack(x, ack(s(x), y)) |
Original Signature
Termination of terms over the following signature is verified: d, 0, nr, le, s, numbers, if, ack, true, false, cons, nil
Strategy
The following SCCs where found
| d#(x) → if#(le(x, nr), x) | if#(true, x) → d#(s(x)) |
| le#(s(x), s(y)) → le#(x, y) |
| ack#(s(x), s(y)) → ack#(s(x), y) | ack#(s(x), s(y)) → ack#(x, ack(s(x), y)) |
| ack#(s(x), 0) → ack#(x, s(0)) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| le#(s(x), s(y)) | → | le#(x, y) |
Rewrite Rules
| numbers | → | d(0) | | d(x) | → | if(le(x, nr), x) |
| if(true, x) | → | cons(x, d(s(x))) | | if(false, x) | → | nil |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | nr | → | ack(s(s(s(s(s(s(0)))))), 0) |
| ack(0, x) | → | s(x) | | ack(s(x), 0) | → | ack(x, s(0)) |
| ack(s(x), s(y)) | → | ack(x, ack(s(x), y)) |
Original Signature
Termination of terms over the following signature is verified: d, 0, nr, le, s, numbers, if, ack, true, false, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| le#(s(x), s(y)) | → | le#(x, y) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| ack#(s(x), s(y)) | → | ack#(s(x), y) | | ack#(s(x), s(y)) | → | ack#(x, ack(s(x), y)) |
| ack#(s(x), 0) | → | ack#(x, s(0)) |
Rewrite Rules
| numbers | → | d(0) | | d(x) | → | if(le(x, nr), x) |
| if(true, x) | → | cons(x, d(s(x))) | | if(false, x) | → | nil |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | nr | → | ack(s(s(s(s(s(s(0)))))), 0) |
| ack(0, x) | → | s(x) | | ack(s(x), 0) | → | ack(x, s(0)) |
| ack(s(x), s(y)) | → | ack(x, ack(s(x), y)) |
Original Signature
Termination of terms over the following signature is verified: d, 0, nr, le, s, numbers, if, ack, true, false, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| ack#(s(x), s(y)) | → | ack#(x, ack(s(x), y)) | | ack#(s(x), 0) | → | ack#(x, s(0)) |
Problem 5: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| ack#(s(x), s(y)) | → | ack#(s(x), y) |
Rewrite Rules
| numbers | → | d(0) | | d(x) | → | if(le(x, nr), x) |
| if(true, x) | → | cons(x, d(s(x))) | | if(false, x) | → | nil |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | nr | → | ack(s(s(s(s(s(s(0)))))), 0) |
| ack(0, x) | → | s(x) | | ack(s(x), 0) | → | ack(x, s(0)) |
| ack(s(x), s(y)) | → | ack(x, ack(s(x), y)) |
Original Signature
Termination of terms over the following signature is verified: d, nr, 0, s, le, numbers, ack, if, false, true, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- ack(x,y): 0
- ack#(x,y): y
- cons(x,y): 0
- d(x): 0
- false: 0
- if(x,y): 0
- le(x,y): 0
- nil: 0
- nr: 0
- numbers: 0
- s(x): 2x + 2
- true: 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| ack#(s(x), s(y)) | → | ack#(s(x), y) |
Problem 4: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| d#(x) | → | if#(le(x, nr), x) | | if#(true, x) | → | d#(s(x)) |
Rewrite Rules
| numbers | → | d(0) | | d(x) | → | if(le(x, nr), x) |
| if(true, x) | → | cons(x, d(s(x))) | | if(false, x) | → | nil |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | nr | → | ack(s(s(s(s(s(s(0)))))), 0) |
| ack(0, x) | → | s(x) | | ack(s(x), 0) | → | ack(x, s(0)) |
| ack(s(x), s(y)) | → | ack(x, ack(s(x), y)) |
Original Signature
Termination of terms over the following signature is verified: d, 0, nr, le, s, numbers, if, ack, true, false, cons, nil
Strategy
Instantiation
For all potential predecessors l → r of the rule d
#(
x) → if
#(le(
x, nr),
x) on dependency pair chains it holds that:
- d#(x) matches r,
- all variables of d#(x) are embedded in constructor contexts, i.e., each subterm of d#(x), containing a variable is rooted by a constructor symbol.
Thus, d
#(
x) → if
#(le(
x, nr),
x) is replaced by instances determined through the above matching. These instances are:
| d#(s(_x)) → if#(le(s(_x), nr), s(_x)) |
Problem 6: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| d#(s(_x)) | → | if#(le(s(_x), nr), s(_x)) | | if#(true, x) | → | d#(s(x)) |
Rewrite Rules
| numbers | → | d(0) | | d(x) | → | if(le(x, nr), x) |
| if(true, x) | → | cons(x, d(s(x))) | | if(false, x) | → | nil |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | nr | → | ack(s(s(s(s(s(s(0)))))), 0) |
| ack(0, x) | → | s(x) | | ack(s(x), 0) | → | ack(x, s(0)) |
| ack(s(x), s(y)) | → | ack(x, ack(s(x), y)) |
Original Signature
Termination of terms over the following signature is verified: d, nr, 0, s, le, numbers, ack, if, false, true, nil, cons
Strategy
Instantiation
For all potential predecessors l → r of the rule d
#(s(
_x)) → if
#(le(s(
_x), nr), s(
_x)) on dependency pair chains it holds that:
- d#(s(_x)) matches r,
- all variables of d#(s(_x)) are embedded in constructor contexts, i.e., each subterm of d#(s(_x)), containing a variable is rooted by a constructor symbol.
Thus, d
#(s(
_x)) → if
#(le(s(
_x), nr), s(
_x)) is replaced by instances determined through the above matching. These instances are:
| d#(s(x)) → if#(le(s(x), nr), s(x)) |
Problem 7: Propagation
Dependency Pair Problem
Dependency Pairs
| d#(s(x)) | → | if#(le(s(x), nr), s(x)) | | if#(true, x) | → | d#(s(x)) |
Rewrite Rules
| numbers | → | d(0) | | d(x) | → | if(le(x, nr), x) |
| if(true, x) | → | cons(x, d(s(x))) | | if(false, x) | → | nil |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | nr | → | ack(s(s(s(s(s(s(0)))))), 0) |
| ack(0, x) | → | s(x) | | ack(s(x), 0) | → | ack(x, s(0)) |
| ack(s(x), s(y)) | → | ack(x, ack(s(x), y)) |
Original Signature
Termination of terms over the following signature is verified: d, 0, nr, le, s, numbers, if, ack, true, false, cons, nil
Strategy
The dependency pairs if
#(true,
x) → d
#(s(
x)) and d
#(s(
x)) → if
#(le(s(
x), nr), s(
x)) are consolidated into the rule if
#(true,
x) → if
#(le(s(
x), nr), s(
x)) .
This is possible as
- all subterms of d#(s(x)) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in d#(s(x)), but non-replacing in both if#(true, x) and if#(le(s(x), nr), s(x))
The dependency pairs if
#(true,
x) → d
#(s(
x)) and d
#(s(
x)) → if
#(le(s(
x), nr), s(
x)) are consolidated into the rule if
#(true,
x) → if
#(le(s(
x), nr), s(
x)) .
This is possible as
- all subterms of d#(s(x)) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in d#(s(x)), but non-replacing in both if#(true, x) and if#(le(s(x), nr), s(x))
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| d#(s(x)) → if#(le(s(x), nr), s(x)) | if#(true, x) → if#(le(s(x), nr), s(x)) |
| if#(true, x) → d#(s(x)) | |