TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60003 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (223ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (1509ms).
| | – Problem 9 was processed with processor PolynomialLinearRange4iUR (759ms).
| | | – Problem 10 was processed with processor DependencyGraph (1ms).
| – Problem 4 was processed with processor SubtermCriterion (0ms).
| – Problem 5 was processed with processor SubtermCriterion (2ms).
| | – Problem 8 was processed with processor DependencyGraph (1ms).
| – Problem 6 was processed with processor ForwardInstantiation (8ms).
| | – Problem 11 remains open; application of the following processors failed [Propagation (10ms), ForwardNarrowing (1ms), BackwardInstantiation (7ms), ForwardInstantiation (6ms), Propagation (10ms)].
| – Problem 7 was processed with processor SubtermCriterion (1ms).
The following open problems remain:
Open Dependency Pair Problem 6
Dependency Pairs
| minIter#(nil, add(n, y), m) | → | minIter#(add(n, y), add(n, y), s(m)) | | if_min#(false, x, y, m) | → | minIter#(x, y, m) |
| minIter#(add(n, x), y, m) | → | if_min#(le(n, m), x, y, m) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | min(nil) | → | 0 |
| min(add(n, x)) | → | minIter(add(n, x), add(n, x), 0) | | minIter(nil, add(n, y), m) | → | minIter(add(n, y), add(n, y), s(m)) |
| minIter(add(n, x), y, m) | → | if_min(le(n, m), x, y, m) | | if_min(true, x, y, m) | → | m |
| if_min(false, x, y, m) | → | minIter(x, y, m) | | head(add(n, x)) | → | n |
| tail(add(n, x)) | → | x | | tail(nil) | → | nil |
| null(nil) | → | true | | null(add(n, x)) | → | false |
| rm(n, nil) | → | nil | | rm(n, add(m, x)) | → | if_rm(eq(n, m), n, add(m, x)) |
| if_rm(true, n, add(m, x)) | → | rm(n, x) | | if_rm(false, n, add(m, x)) | → | add(m, rm(n, x)) |
| minsort(nil, nil) | → | nil | | minsort(add(n, x), y) | → | if_minsort(eq(n, min(add(n, x))), add(n, x), y) |
| if_minsort(true, add(n, x), y) | → | add(n, minsort(app(rm(n, x), y), nil)) | | if_minsort(false, add(n, x), y) | → | minsort(x, add(n, y)) |
Original Signature
Termination of terms over the following signature is verified: minsort, min, app, rm, true, add, tail, minIter, if_min, 0, if_minsort, s, le, if_rm, false, head, null, eq, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| app#(add(n, x), y) | → | app#(x, y) | | rm#(n, add(m, x)) | → | eq#(n, m) |
| if_rm#(false, n, add(m, x)) | → | rm#(n, x) | | minsort#(add(n, x), y) | → | eq#(n, min(add(n, x))) |
| if_minsort#(true, add(n, x), y) | → | rm#(n, x) | | minsort#(add(n, x), y) | → | min#(add(n, x)) |
| if_min#(false, x, y, m) | → | minIter#(x, y, m) | | if_rm#(true, n, add(m, x)) | → | rm#(n, x) |
| min#(add(n, x)) | → | minIter#(add(n, x), add(n, x), 0) | | if_minsort#(true, add(n, x), y) | → | app#(rm(n, x), y) |
| minIter#(add(n, x), y, m) | → | if_min#(le(n, m), x, y, m) | | le#(s(x), s(y)) | → | le#(x, y) |
| minIter#(add(n, x), y, m) | → | le#(n, m) | | minIter#(nil, add(n, y), m) | → | minIter#(add(n, y), add(n, y), s(m)) |
| if_minsort#(true, add(n, x), y) | → | minsort#(app(rm(n, x), y), nil) | | minsort#(add(n, x), y) | → | if_minsort#(eq(n, min(add(n, x))), add(n, x), y) |
| rm#(n, add(m, x)) | → | if_rm#(eq(n, m), n, add(m, x)) | | eq#(s(x), s(y)) | → | eq#(x, y) |
| if_minsort#(false, add(n, x), y) | → | minsort#(x, add(n, y)) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | min(nil) | → | 0 |
| min(add(n, x)) | → | minIter(add(n, x), add(n, x), 0) | | minIter(nil, add(n, y), m) | → | minIter(add(n, y), add(n, y), s(m)) |
| minIter(add(n, x), y, m) | → | if_min(le(n, m), x, y, m) | | if_min(true, x, y, m) | → | m |
| if_min(false, x, y, m) | → | minIter(x, y, m) | | head(add(n, x)) | → | n |
| tail(add(n, x)) | → | x | | tail(nil) | → | nil |
| null(nil) | → | true | | null(add(n, x)) | → | false |
| rm(n, nil) | → | nil | | rm(n, add(m, x)) | → | if_rm(eq(n, m), n, add(m, x)) |
| if_rm(true, n, add(m, x)) | → | rm(n, x) | | if_rm(false, n, add(m, x)) | → | add(m, rm(n, x)) |
| minsort(nil, nil) | → | nil | | minsort(add(n, x), y) | → | if_minsort(eq(n, min(add(n, x))), add(n, x), y) |
| if_minsort(true, add(n, x), y) | → | add(n, minsort(app(rm(n, x), y), nil)) | | if_minsort(false, add(n, x), y) | → | minsort(x, add(n, y)) |
Original Signature
Termination of terms over the following signature is verified: minsort, min, app, rm, true, add, tail, minIter, if_min, 0, if_minsort, s, le, false, if_rm, head, null, nil, eq
Strategy
The following SCCs where found
| if_minsort#(true, add(n, x), y) → minsort#(app(rm(n, x), y), nil) | minsort#(add(n, x), y) → if_minsort#(eq(n, min(add(n, x))), add(n, x), y) |
| if_minsort#(false, add(n, x), y) → minsort#(x, add(n, y)) |
| le#(s(x), s(y)) → le#(x, y) |
| app#(add(n, x), y) → app#(x, y) |
| if_rm#(false, n, add(m, x)) → rm#(n, x) | rm#(n, add(m, x)) → if_rm#(eq(n, m), n, add(m, x)) |
| if_rm#(true, n, add(m, x)) → rm#(n, x) |
| minIter#(nil, add(n, y), m) → minIter#(add(n, y), add(n, y), s(m)) | if_min#(false, x, y, m) → minIter#(x, y, m) |
| minIter#(add(n, x), y, m) → if_min#(le(n, m), x, y, m) |
| eq#(s(x), s(y)) → eq#(x, y) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| app#(add(n, x), y) | → | app#(x, y) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | min(nil) | → | 0 |
| min(add(n, x)) | → | minIter(add(n, x), add(n, x), 0) | | minIter(nil, add(n, y), m) | → | minIter(add(n, y), add(n, y), s(m)) |
| minIter(add(n, x), y, m) | → | if_min(le(n, m), x, y, m) | | if_min(true, x, y, m) | → | m |
| if_min(false, x, y, m) | → | minIter(x, y, m) | | head(add(n, x)) | → | n |
| tail(add(n, x)) | → | x | | tail(nil) | → | nil |
| null(nil) | → | true | | null(add(n, x)) | → | false |
| rm(n, nil) | → | nil | | rm(n, add(m, x)) | → | if_rm(eq(n, m), n, add(m, x)) |
| if_rm(true, n, add(m, x)) | → | rm(n, x) | | if_rm(false, n, add(m, x)) | → | add(m, rm(n, x)) |
| minsort(nil, nil) | → | nil | | minsort(add(n, x), y) | → | if_minsort(eq(n, min(add(n, x))), add(n, x), y) |
| if_minsort(true, add(n, x), y) | → | add(n, minsort(app(rm(n, x), y), nil)) | | if_minsort(false, add(n, x), y) | → | minsort(x, add(n, y)) |
Original Signature
Termination of terms over the following signature is verified: minsort, min, app, rm, true, add, tail, minIter, if_min, 0, if_minsort, s, le, false, if_rm, head, null, nil, eq
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| app#(add(n, x), y) | → | app#(x, y) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| if_minsort#(true, add(n, x), y) | → | minsort#(app(rm(n, x), y), nil) | | minsort#(add(n, x), y) | → | if_minsort#(eq(n, min(add(n, x))), add(n, x), y) |
| if_minsort#(false, add(n, x), y) | → | minsort#(x, add(n, y)) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | min(nil) | → | 0 |
| min(add(n, x)) | → | minIter(add(n, x), add(n, x), 0) | | minIter(nil, add(n, y), m) | → | minIter(add(n, y), add(n, y), s(m)) |
| minIter(add(n, x), y, m) | → | if_min(le(n, m), x, y, m) | | if_min(true, x, y, m) | → | m |
| if_min(false, x, y, m) | → | minIter(x, y, m) | | head(add(n, x)) | → | n |
| tail(add(n, x)) | → | x | | tail(nil) | → | nil |
| null(nil) | → | true | | null(add(n, x)) | → | false |
| rm(n, nil) | → | nil | | rm(n, add(m, x)) | → | if_rm(eq(n, m), n, add(m, x)) |
| if_rm(true, n, add(m, x)) | → | rm(n, x) | | if_rm(false, n, add(m, x)) | → | add(m, rm(n, x)) |
| minsort(nil, nil) | → | nil | | minsort(add(n, x), y) | → | if_minsort(eq(n, min(add(n, x))), add(n, x), y) |
| if_minsort(true, add(n, x), y) | → | add(n, minsort(app(rm(n, x), y), nil)) | | if_minsort(false, add(n, x), y) | → | minsort(x, add(n, y)) |
Original Signature
Termination of terms over the following signature is verified: minsort, min, app, rm, true, add, tail, minIter, if_min, 0, if_minsort, s, le, false, if_rm, head, null, nil, eq
Strategy
Polynomial Interpretation
- 0: 2
- add(x,y): y + 1
- app(x,y): y + x
- eq(x,y): y
- false: 0
- head(x): 0
- if_min(x1,x2,x3,x4): 2x1
- if_minsort(x,y,z): 0
- if_minsort#(x,y,z): 2z + 2y
- if_rm(x,y,z): z
- le(x,y): x
- min(x): 0
- minIter(x,y,z): 0
- minsort(x,y): 0
- minsort#(x,y): 2y + 2x
- nil: 0
- null(x): 0
- rm(x,y): y
- s(x): 2
- tail(x): 0
- true: 0
Improved Usable rules
| app(nil, y) | → | y | | if_rm(false, n, add(m, x)) | → | add(m, rm(n, x)) |
| if_rm(true, n, add(m, x)) | → | rm(n, x) | | rm(n, add(m, x)) | → | if_rm(eq(n, m), n, add(m, x)) |
| rm(n, nil) | → | nil | | app(add(n, x), y) | → | add(n, app(x, y)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| if_minsort#(true, add(n, x), y) | → | minsort#(app(rm(n, x), y), nil) |
Problem 9: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| minsort#(add(n, x), y) | → | if_minsort#(eq(n, min(add(n, x))), add(n, x), y) | | if_minsort#(false, add(n, x), y) | → | minsort#(x, add(n, y)) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | min(nil) | → | 0 |
| min(add(n, x)) | → | minIter(add(n, x), add(n, x), 0) | | minIter(nil, add(n, y), m) | → | minIter(add(n, y), add(n, y), s(m)) |
| minIter(add(n, x), y, m) | → | if_min(le(n, m), x, y, m) | | if_min(true, x, y, m) | → | m |
| if_min(false, x, y, m) | → | minIter(x, y, m) | | head(add(n, x)) | → | n |
| tail(add(n, x)) | → | x | | tail(nil) | → | nil |
| null(nil) | → | true | | null(add(n, x)) | → | false |
| rm(n, nil) | → | nil | | rm(n, add(m, x)) | → | if_rm(eq(n, m), n, add(m, x)) |
| if_rm(true, n, add(m, x)) | → | rm(n, x) | | if_rm(false, n, add(m, x)) | → | add(m, rm(n, x)) |
| minsort(nil, nil) | → | nil | | minsort(add(n, x), y) | → | if_minsort(eq(n, min(add(n, x))), add(n, x), y) |
| if_minsort(true, add(n, x), y) | → | add(n, minsort(app(rm(n, x), y), nil)) | | if_minsort(false, add(n, x), y) | → | minsort(x, add(n, y)) |
Original Signature
Termination of terms over the following signature is verified: minsort, min, app, rm, true, add, tail, minIter, if_min, 0, if_minsort, s, le, if_rm, false, head, null, eq, nil
Strategy
Polynomial Interpretation
- 0: 0
- add(x,y): 3y + 3x + 1
- app(x,y): 0
- eq(x,y): y
- false: 0
- head(x): 0
- if_min(x1,x2,x3,x4): x4
- if_minsort(x,y,z): 0
- if_minsort#(x,y,z): y + 2x
- if_rm(x,y,z): 0
- le(x,y): 2
- min(x): x
- minIter(x,y,z): z
- minsort(x,y): 0
- minsort#(x,y): 3x
- nil: 3
- null(x): 0
- rm(x,y): 0
- s(x): x
- tail(x): 0
- true: 0
Improved Usable rules
| minIter(add(n, x), y, m) | → | if_min(le(n, m), x, y, m) | | min(nil) | → | 0 |
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), s(y)) | → | eq(x, y) | | minIter(nil, add(n, y), m) | → | minIter(add(n, y), add(n, y), s(m)) |
| if_min(true, x, y, m) | → | m | | eq(s(x), 0) | → | false |
| min(add(n, x)) | → | minIter(add(n, x), add(n, x), 0) | | if_min(false, x, y, m) | → | minIter(x, y, m) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| if_minsort#(false, add(n, x), y) | → | minsort#(x, add(n, y)) |
Problem 10: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| minsort#(add(n, x), y) | → | if_minsort#(eq(n, min(add(n, x))), add(n, x), y) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | min(nil) | → | 0 |
| min(add(n, x)) | → | minIter(add(n, x), add(n, x), 0) | | minIter(nil, add(n, y), m) | → | minIter(add(n, y), add(n, y), s(m)) |
| minIter(add(n, x), y, m) | → | if_min(le(n, m), x, y, m) | | if_min(true, x, y, m) | → | m |
| if_min(false, x, y, m) | → | minIter(x, y, m) | | head(add(n, x)) | → | n |
| tail(add(n, x)) | → | x | | tail(nil) | → | nil |
| null(nil) | → | true | | null(add(n, x)) | → | false |
| rm(n, nil) | → | nil | | rm(n, add(m, x)) | → | if_rm(eq(n, m), n, add(m, x)) |
| if_rm(true, n, add(m, x)) | → | rm(n, x) | | if_rm(false, n, add(m, x)) | → | add(m, rm(n, x)) |
| minsort(nil, nil) | → | nil | | minsort(add(n, x), y) | → | if_minsort(eq(n, min(add(n, x))), add(n, x), y) |
| if_minsort(true, add(n, x), y) | → | add(n, minsort(app(rm(n, x), y), nil)) | | if_minsort(false, add(n, x), y) | → | minsort(x, add(n, y)) |
Original Signature
Termination of terms over the following signature is verified: minsort, min, app, rm, true, add, tail, minIter, if_min, 0, if_minsort, s, le, false, if_rm, head, null, nil, eq
Strategy
There are no SCCs!
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| eq#(s(x), s(y)) | → | eq#(x, y) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | min(nil) | → | 0 |
| min(add(n, x)) | → | minIter(add(n, x), add(n, x), 0) | | minIter(nil, add(n, y), m) | → | minIter(add(n, y), add(n, y), s(m)) |
| minIter(add(n, x), y, m) | → | if_min(le(n, m), x, y, m) | | if_min(true, x, y, m) | → | m |
| if_min(false, x, y, m) | → | minIter(x, y, m) | | head(add(n, x)) | → | n |
| tail(add(n, x)) | → | x | | tail(nil) | → | nil |
| null(nil) | → | true | | null(add(n, x)) | → | false |
| rm(n, nil) | → | nil | | rm(n, add(m, x)) | → | if_rm(eq(n, m), n, add(m, x)) |
| if_rm(true, n, add(m, x)) | → | rm(n, x) | | if_rm(false, n, add(m, x)) | → | add(m, rm(n, x)) |
| minsort(nil, nil) | → | nil | | minsort(add(n, x), y) | → | if_minsort(eq(n, min(add(n, x))), add(n, x), y) |
| if_minsort(true, add(n, x), y) | → | add(n, minsort(app(rm(n, x), y), nil)) | | if_minsort(false, add(n, x), y) | → | minsort(x, add(n, y)) |
Original Signature
Termination of terms over the following signature is verified: minsort, min, app, rm, true, add, tail, minIter, if_min, 0, if_minsort, s, le, false, if_rm, head, null, nil, eq
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| eq#(s(x), s(y)) | → | eq#(x, y) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| if_rm#(false, n, add(m, x)) | → | rm#(n, x) | | rm#(n, add(m, x)) | → | if_rm#(eq(n, m), n, add(m, x)) |
| if_rm#(true, n, add(m, x)) | → | rm#(n, x) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | min(nil) | → | 0 |
| min(add(n, x)) | → | minIter(add(n, x), add(n, x), 0) | | minIter(nil, add(n, y), m) | → | minIter(add(n, y), add(n, y), s(m)) |
| minIter(add(n, x), y, m) | → | if_min(le(n, m), x, y, m) | | if_min(true, x, y, m) | → | m |
| if_min(false, x, y, m) | → | minIter(x, y, m) | | head(add(n, x)) | → | n |
| tail(add(n, x)) | → | x | | tail(nil) | → | nil |
| null(nil) | → | true | | null(add(n, x)) | → | false |
| rm(n, nil) | → | nil | | rm(n, add(m, x)) | → | if_rm(eq(n, m), n, add(m, x)) |
| if_rm(true, n, add(m, x)) | → | rm(n, x) | | if_rm(false, n, add(m, x)) | → | add(m, rm(n, x)) |
| minsort(nil, nil) | → | nil | | minsort(add(n, x), y) | → | if_minsort(eq(n, min(add(n, x))), add(n, x), y) |
| if_minsort(true, add(n, x), y) | → | add(n, minsort(app(rm(n, x), y), nil)) | | if_minsort(false, add(n, x), y) | → | minsort(x, add(n, y)) |
Original Signature
Termination of terms over the following signature is verified: minsort, min, app, rm, true, add, tail, minIter, if_min, 0, if_minsort, s, le, false, if_rm, head, null, nil, eq
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| if_rm#(false, n, add(m, x)) | → | rm#(n, x) | | if_rm#(true, n, add(m, x)) | → | rm#(n, x) |
Problem 8: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| rm#(n, add(m, x)) | → | if_rm#(eq(n, m), n, add(m, x)) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | min(nil) | → | 0 |
| min(add(n, x)) | → | minIter(add(n, x), add(n, x), 0) | | minIter(nil, add(n, y), m) | → | minIter(add(n, y), add(n, y), s(m)) |
| minIter(add(n, x), y, m) | → | if_min(le(n, m), x, y, m) | | if_min(true, x, y, m) | → | m |
| if_min(false, x, y, m) | → | minIter(x, y, m) | | head(add(n, x)) | → | n |
| tail(add(n, x)) | → | x | | tail(nil) | → | nil |
| null(nil) | → | true | | null(add(n, x)) | → | false |
| rm(n, nil) | → | nil | | rm(n, add(m, x)) | → | if_rm(eq(n, m), n, add(m, x)) |
| if_rm(true, n, add(m, x)) | → | rm(n, x) | | if_rm(false, n, add(m, x)) | → | add(m, rm(n, x)) |
| minsort(nil, nil) | → | nil | | minsort(add(n, x), y) | → | if_minsort(eq(n, min(add(n, x))), add(n, x), y) |
| if_minsort(true, add(n, x), y) | → | add(n, minsort(app(rm(n, x), y), nil)) | | if_minsort(false, add(n, x), y) | → | minsort(x, add(n, y)) |
Original Signature
Termination of terms over the following signature is verified: minsort, min, app, rm, true, add, tail, minIter, if_min, 0, if_minsort, s, le, if_rm, false, head, null, eq, nil
Strategy
There are no SCCs!
Problem 6: ForwardInstantiation
Dependency Pair Problem
Dependency Pairs
| minIter#(nil, add(n, y), m) | → | minIter#(add(n, y), add(n, y), s(m)) | | if_min#(false, x, y, m) | → | minIter#(x, y, m) |
| minIter#(add(n, x), y, m) | → | if_min#(le(n, m), x, y, m) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | min(nil) | → | 0 |
| min(add(n, x)) | → | minIter(add(n, x), add(n, x), 0) | | minIter(nil, add(n, y), m) | → | minIter(add(n, y), add(n, y), s(m)) |
| minIter(add(n, x), y, m) | → | if_min(le(n, m), x, y, m) | | if_min(true, x, y, m) | → | m |
| if_min(false, x, y, m) | → | minIter(x, y, m) | | head(add(n, x)) | → | n |
| tail(add(n, x)) | → | x | | tail(nil) | → | nil |
| null(nil) | → | true | | null(add(n, x)) | → | false |
| rm(n, nil) | → | nil | | rm(n, add(m, x)) | → | if_rm(eq(n, m), n, add(m, x)) |
| if_rm(true, n, add(m, x)) | → | rm(n, x) | | if_rm(false, n, add(m, x)) | → | add(m, rm(n, x)) |
| minsort(nil, nil) | → | nil | | minsort(add(n, x), y) | → | if_minsort(eq(n, min(add(n, x))), add(n, x), y) |
| if_minsort(true, add(n, x), y) | → | add(n, minsort(app(rm(n, x), y), nil)) | | if_minsort(false, add(n, x), y) | → | minsort(x, add(n, y)) |
Original Signature
Termination of terms over the following signature is verified: minsort, min, app, rm, true, add, tail, minIter, if_min, 0, if_minsort, s, le, false, if_rm, head, null, nil, eq
Strategy
Instantiation
For all potential successors l → r of the rule if_min
#(false,
x,
y,
m) → minIter
#(
x,
y,
m) on dependency pair chains it holds that:
- minIter#(x, y, m) matches l,
- all variables of minIter#(x, y, m) are embedded in constructor contexts, i.e., each subterm of minIter#(x, y, m) containing a variable is rooted by a constructor symbol.
Thus, if_min
#(false,
x,
y,
m) → minIter
#(
x,
y,
m) is replaced by instances determined through the above matching. These instances are:
| if_min#(false, add(_n, _x), y, m) → minIter#(add(_n, _x), y, m) | if_min#(false, nil, add(_n, _y), m) → minIter#(nil, add(_n, _y), m) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| le#(s(x), s(y)) | → | le#(x, y) |
Rewrite Rules
| eq(0, 0) | → | true | | eq(0, s(x)) | → | false |
| eq(s(x), 0) | → | false | | eq(s(x), s(y)) | → | eq(x, y) |
| le(0, y) | → | true | | le(s(x), 0) | → | false |
| le(s(x), s(y)) | → | le(x, y) | | app(nil, y) | → | y |
| app(add(n, x), y) | → | add(n, app(x, y)) | | min(nil) | → | 0 |
| min(add(n, x)) | → | minIter(add(n, x), add(n, x), 0) | | minIter(nil, add(n, y), m) | → | minIter(add(n, y), add(n, y), s(m)) |
| minIter(add(n, x), y, m) | → | if_min(le(n, m), x, y, m) | | if_min(true, x, y, m) | → | m |
| if_min(false, x, y, m) | → | minIter(x, y, m) | | head(add(n, x)) | → | n |
| tail(add(n, x)) | → | x | | tail(nil) | → | nil |
| null(nil) | → | true | | null(add(n, x)) | → | false |
| rm(n, nil) | → | nil | | rm(n, add(m, x)) | → | if_rm(eq(n, m), n, add(m, x)) |
| if_rm(true, n, add(m, x)) | → | rm(n, x) | | if_rm(false, n, add(m, x)) | → | add(m, rm(n, x)) |
| minsort(nil, nil) | → | nil | | minsort(add(n, x), y) | → | if_minsort(eq(n, min(add(n, x))), add(n, x), y) |
| if_minsort(true, add(n, x), y) | → | add(n, minsort(app(rm(n, x), y), nil)) | | if_minsort(false, add(n, x), y) | → | minsort(x, add(n, y)) |
Original Signature
Termination of terms over the following signature is verified: minsort, min, app, rm, true, add, tail, minIter, if_min, 0, if_minsort, s, le, false, if_rm, head, null, nil, eq
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| le#(s(x), s(y)) | → | le#(x, y) |