TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60365 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (397ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (50ms).
| – Problem 3 was processed with processor PolynomialLinearRange4 (25ms).
| – Problem 4 was processed with processor PolynomialLinearRange4 (15ms).
| – Problem 5 was processed with processor PolynomialLinearRange4 (14ms).
| – Problem 6 was processed with processor PolynomialLinearRange4 (71ms).
| – Problem 7 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (8ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (6ms), PolynomialLinearRange8NegiUR (0ms), DependencyGraph (6ms), PolynomialLinearRange4 (715ms), DependencyGraph (5ms), PolynomialLinearRange4 (451ms), DependencyGraph (6ms), ReductionPairSAT (4774ms), DependencyGraph (14ms), SizeChangePrinciple (timeout)].
| – Problem 8 was processed with processor PolynomialLinearRange4 (14ms).
The following open problems remain:
Open Dependency Pair Problem 7
Dependency Pairs
| U182#(false, store, m) | → | process#(sndsplit(m, app(map_f(self, nil), store)), m) | | process#(store, m) | → | U171#(leq(m, length(store)), store, m) |
| U181#(false, store, m) | → | U182#(empty(fstsplit(m, app(map_f(self, nil), store))), store, m) | | U171#(true, store, m) | → | U172#(empty(fstsplit(m, store)), store, m) |
| U172#(false, store, m) | → | process#(app(map_f(self, nil), sndsplit(m, store)), m) | | process#(store, m) | → | U181#(leq(m, length(store)), store, m) |
Rewrite Rules
| fstsplit(0, x) | → | nil | | fstsplit(s(n), nil) | → | nil |
| fstsplit(s(n), cons(h, t)) | → | cons(h, fstsplit(n, t)) | | sndsplit(0, x) | → | x |
| sndsplit(s(n), nil) | → | nil | | sndsplit(s(n), cons(h, t)) | → | sndsplit(n, t) |
| empty(nil) | → | true | | empty(cons(h, t)) | → | false |
| leq(0, m) | → | true | | leq(s(n), 0) | → | false |
| leq(s(n), s(m)) | → | leq(n, m) | | length(nil) | → | 0 |
| length(cons(h, t)) | → | s(length(t)) | | app(nil, x) | → | x |
| app(cons(h, t), x) | → | cons(h, app(t, x)) | | map_f(pid, nil) | → | nil |
| map_f(pid, cons(h, t)) | → | app(f(pid, h), map_f(pid, t)) | | process(store, m) | → | U171(leq(m, length(store)), store, m) |
| U171(true, store, m) | → | U172(empty(fstsplit(m, store)), store, m) | | U172(false, store, m) | → | process(app(map_f(self, nil), sndsplit(m, store)), m) |
| process(store, m) | → | U181(leq(m, length(store)), store, m) | | U181(false, store, m) | → | U182(empty(fstsplit(m, app(map_f(self, nil), store))), store, m) |
| U182(false, store, m) | → | process(sndsplit(m, app(map_f(self, nil), store)), m) |
Original Signature
Termination of terms over the following signature is verified: f, app, map_f, leq, true, self, process, fstsplit, 0, s, sndsplit, empty, length, false, nil, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U181#(false, store, m) | → | app#(map_f(self, nil), store) | | process#(store, m) | → | leq#(m, length(store)) |
| U181#(false, store, m) | → | map_f#(self, nil) | | U171#(true, store, m) | → | empty#(fstsplit(m, store)) |
| U182#(false, store, m) | → | T(store) | | U172#(false, store, m) | → | T(m) |
| U172#(false, store, m) | → | app#(map_f(self, nil), sndsplit(m, store)) | | U172#(false, store, m) | → | process#(app(map_f(self, nil), sndsplit(m, store)), m) |
| leq#(s(n), s(m)) | → | leq#(n, m) | | U171#(true, store, m) | → | T(store) |
| U182#(false, store, m) | → | app#(map_f(self, nil), store) | | U181#(false, store, m) | → | T(m) |
| length#(cons(h, t)) | → | length#(t) | | U172#(false, store, m) | → | T(store) |
| U171#(true, store, m) | → | U172#(empty(fstsplit(m, store)), store, m) | | U182#(false, store, m) | → | sndsplit#(m, app(map_f(self, nil), store)) |
| process#(store, m) | → | U181#(leq(m, length(store)), store, m) | | U182#(false, store, m) | → | map_f#(self, nil) |
| U182#(false, store, m) | → | process#(sndsplit(m, app(map_f(self, nil), store)), m) | | process#(store, m) | → | U171#(leq(m, length(store)), store, m) |
| U181#(false, store, m) | → | U182#(empty(fstsplit(m, app(map_f(self, nil), store))), store, m) | | process#(store, m) | → | length#(store) |
| U181#(false, store, m) | → | fstsplit#(m, app(map_f(self, nil), store)) | | fstsplit#(s(n), cons(h, t)) | → | fstsplit#(n, t) |
| map_f#(pid, cons(h, t)) | → | app#(f(pid, h), map_f(pid, t)) | | U171#(true, store, m) | → | fstsplit#(m, store) |
| U172#(false, store, m) | → | map_f#(self, nil) | | U181#(false, store, m) | → | empty#(fstsplit(m, app(map_f(self, nil), store))) |
| U181#(false, store, m) | → | T(store) | | U171#(true, store, m) | → | T(m) |
| U172#(false, store, m) | → | sndsplit#(m, store) | | app#(cons(h, t), x) | → | app#(t, x) |
| U182#(false, store, m) | → | T(m) | | sndsplit#(s(n), cons(h, t)) | → | sndsplit#(n, t) |
| map_f#(pid, cons(h, t)) | → | map_f#(pid, t) |
Rewrite Rules
| fstsplit(0, x) | → | nil | | fstsplit(s(n), nil) | → | nil |
| fstsplit(s(n), cons(h, t)) | → | cons(h, fstsplit(n, t)) | | sndsplit(0, x) | → | x |
| sndsplit(s(n), nil) | → | nil | | sndsplit(s(n), cons(h, t)) | → | sndsplit(n, t) |
| empty(nil) | → | true | | empty(cons(h, t)) | → | false |
| leq(0, m) | → | true | | leq(s(n), 0) | → | false |
| leq(s(n), s(m)) | → | leq(n, m) | | length(nil) | → | 0 |
| length(cons(h, t)) | → | s(length(t)) | | app(nil, x) | → | x |
| app(cons(h, t), x) | → | cons(h, app(t, x)) | | map_f(pid, nil) | → | nil |
| map_f(pid, cons(h, t)) | → | app(f(pid, h), map_f(pid, t)) | | process(store, m) | → | U171(leq(m, length(store)), store, m) |
| U171(true, store, m) | → | U172(empty(fstsplit(m, store)), store, m) | | U172(false, store, m) | → | process(app(map_f(self, nil), sndsplit(m, store)), m) |
| process(store, m) | → | U181(leq(m, length(store)), store, m) | | U181(false, store, m) | → | U182(empty(fstsplit(m, app(map_f(self, nil), store))), store, m) |
| U182(false, store, m) | → | process(sndsplit(m, app(map_f(self, nil), store)), m) |
Original Signature
Termination of terms over the following signature is verified: f, app, map_f, leq, true, self, process, fstsplit, 0, s, sndsplit, empty, length, false, cons, nil
Strategy
Context-sensitive strategy:
μ(self) = μ(T) = μ(false) = μ(true) = μ(0) = μ(nil) = ∅
μ(U181) = μ(U182) = μ(length#) = μ(U181#) = μ(empty#) = μ(U171#) = μ(length) = μ(empty) = μ(U171) = μ(U172) = μ(U182#) = μ(U172#) = μ(s) = {1}
μ(leq#) = μ(map_f#) = μ(fstsplit) = μ(process#) = μ(fstsplit#) = μ(sndsplit) = μ(cons) = μ(f) = μ(app) = μ(app#) = μ(map_f) = μ(leq) = μ(process) = μ(sndsplit#) = {1, 2}
The following SCCs where found
| U182#(false, store, m) → process#(sndsplit(m, app(map_f(self, nil), store)), m) | U181#(false, store, m) → U182#(empty(fstsplit(m, app(map_f(self, nil), store))), store, m) |
| process#(store, m) → U171#(leq(m, length(store)), store, m) | U171#(true, store, m) → U172#(empty(fstsplit(m, store)), store, m) |
| U172#(false, store, m) → process#(app(map_f(self, nil), sndsplit(m, store)), m) | process#(store, m) → U181#(leq(m, length(store)), store, m) |
| fstsplit#(s(n), cons(h, t)) → fstsplit#(n, t) |
| length#(cons(h, t)) → length#(t) |
| app#(cons(h, t), x) → app#(t, x) |
| leq#(s(n), s(m)) → leq#(n, m) |
| sndsplit#(s(n), cons(h, t)) → sndsplit#(n, t) |
| map_f#(pid, cons(h, t)) → map_f#(pid, t) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| leq#(s(n), s(m)) | → | leq#(n, m) |
Rewrite Rules
| fstsplit(0, x) | → | nil | | fstsplit(s(n), nil) | → | nil |
| fstsplit(s(n), cons(h, t)) | → | cons(h, fstsplit(n, t)) | | sndsplit(0, x) | → | x |
| sndsplit(s(n), nil) | → | nil | | sndsplit(s(n), cons(h, t)) | → | sndsplit(n, t) |
| empty(nil) | → | true | | empty(cons(h, t)) | → | false |
| leq(0, m) | → | true | | leq(s(n), 0) | → | false |
| leq(s(n), s(m)) | → | leq(n, m) | | length(nil) | → | 0 |
| length(cons(h, t)) | → | s(length(t)) | | app(nil, x) | → | x |
| app(cons(h, t), x) | → | cons(h, app(t, x)) | | map_f(pid, nil) | → | nil |
| map_f(pid, cons(h, t)) | → | app(f(pid, h), map_f(pid, t)) | | process(store, m) | → | U171(leq(m, length(store)), store, m) |
| U171(true, store, m) | → | U172(empty(fstsplit(m, store)), store, m) | | U172(false, store, m) | → | process(app(map_f(self, nil), sndsplit(m, store)), m) |
| process(store, m) | → | U181(leq(m, length(store)), store, m) | | U181(false, store, m) | → | U182(empty(fstsplit(m, app(map_f(self, nil), store))), store, m) |
| U182(false, store, m) | → | process(sndsplit(m, app(map_f(self, nil), store)), m) |
Original Signature
Termination of terms over the following signature is verified: f, app, map_f, leq, true, self, process, fstsplit, 0, s, sndsplit, empty, length, false, cons, nil
Strategy
Context-sensitive strategy:
μ(self) = μ(T) = μ(false) = μ(true) = μ(0) = μ(nil) = ∅
μ(U181) = μ(U182) = μ(length#) = μ(empty#) = μ(U181#) = μ(U171#) = μ(length) = μ(empty) = μ(U171) = μ(U172) = μ(U182#) = μ(U172#) = μ(s) = {1}
μ(leq#) = μ(map_f#) = μ(fstsplit) = μ(process#) = μ(fstsplit#) = μ(sndsplit) = μ(cons) = μ(f) = μ(app) = μ(app#) = μ(map_f) = μ(leq) = μ(process) = μ(sndsplit#) = {1, 2}
Polynomial Interpretation
- 0: 0
- U171(x,y,z): 0
- U172(x,y,z): 0
- U181(x,y,z): 0
- U182(x,y,z): 0
- app(x,y): 0
- cons(x,y): 0
- empty(x): 0
- f(x,y): 0
- false: 0
- fstsplit(x,y): 0
- length(x): 0
- leq(x,y): 0
- leq#(x,y): x
- map_f(x,y): 0
- nil: 0
- process(x,y): 0
- s(x): 2x + 1
- self: 0
- sndsplit(x,y): 0
- 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:
| leq#(s(n), s(m)) | → | leq#(n, m) |
Problem 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| sndsplit#(s(n), cons(h, t)) | → | sndsplit#(n, t) |
Rewrite Rules
| fstsplit(0, x) | → | nil | | fstsplit(s(n), nil) | → | nil |
| fstsplit(s(n), cons(h, t)) | → | cons(h, fstsplit(n, t)) | | sndsplit(0, x) | → | x |
| sndsplit(s(n), nil) | → | nil | | sndsplit(s(n), cons(h, t)) | → | sndsplit(n, t) |
| empty(nil) | → | true | | empty(cons(h, t)) | → | false |
| leq(0, m) | → | true | | leq(s(n), 0) | → | false |
| leq(s(n), s(m)) | → | leq(n, m) | | length(nil) | → | 0 |
| length(cons(h, t)) | → | s(length(t)) | | app(nil, x) | → | x |
| app(cons(h, t), x) | → | cons(h, app(t, x)) | | map_f(pid, nil) | → | nil |
| map_f(pid, cons(h, t)) | → | app(f(pid, h), map_f(pid, t)) | | process(store, m) | → | U171(leq(m, length(store)), store, m) |
| U171(true, store, m) | → | U172(empty(fstsplit(m, store)), store, m) | | U172(false, store, m) | → | process(app(map_f(self, nil), sndsplit(m, store)), m) |
| process(store, m) | → | U181(leq(m, length(store)), store, m) | | U181(false, store, m) | → | U182(empty(fstsplit(m, app(map_f(self, nil), store))), store, m) |
| U182(false, store, m) | → | process(sndsplit(m, app(map_f(self, nil), store)), m) |
Original Signature
Termination of terms over the following signature is verified: f, app, map_f, leq, true, self, process, fstsplit, 0, s, sndsplit, empty, length, false, cons, nil
Strategy
Context-sensitive strategy:
μ(self) = μ(T) = μ(false) = μ(true) = μ(0) = μ(nil) = ∅
μ(U181) = μ(U182) = μ(length#) = μ(empty#) = μ(U181#) = μ(U171#) = μ(length) = μ(empty) = μ(U171) = μ(U172) = μ(U182#) = μ(U172#) = μ(s) = {1}
μ(leq#) = μ(map_f#) = μ(fstsplit) = μ(process#) = μ(fstsplit#) = μ(sndsplit) = μ(cons) = μ(f) = μ(app) = μ(app#) = μ(map_f) = μ(leq) = μ(process) = μ(sndsplit#) = {1, 2}
Polynomial Interpretation
- 0: 0
- U171(x,y,z): 0
- U172(x,y,z): 0
- U181(x,y,z): 0
- U182(x,y,z): 0
- app(x,y): 0
- cons(x,y): 3
- empty(x): 0
- f(x,y): 0
- false: 0
- fstsplit(x,y): 0
- length(x): 0
- leq(x,y): 0
- map_f(x,y): 0
- nil: 0
- process(x,y): 0
- s(x): 2x + 1
- self: 0
- sndsplit(x,y): 0
- sndsplit#(x,y): x + 1
- 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:
| sndsplit#(s(n), cons(h, t)) | → | sndsplit#(n, t) |
Problem 4: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| length#(cons(h, t)) | → | length#(t) |
Rewrite Rules
| fstsplit(0, x) | → | nil | | fstsplit(s(n), nil) | → | nil |
| fstsplit(s(n), cons(h, t)) | → | cons(h, fstsplit(n, t)) | | sndsplit(0, x) | → | x |
| sndsplit(s(n), nil) | → | nil | | sndsplit(s(n), cons(h, t)) | → | sndsplit(n, t) |
| empty(nil) | → | true | | empty(cons(h, t)) | → | false |
| leq(0, m) | → | true | | leq(s(n), 0) | → | false |
| leq(s(n), s(m)) | → | leq(n, m) | | length(nil) | → | 0 |
| length(cons(h, t)) | → | s(length(t)) | | app(nil, x) | → | x |
| app(cons(h, t), x) | → | cons(h, app(t, x)) | | map_f(pid, nil) | → | nil |
| map_f(pid, cons(h, t)) | → | app(f(pid, h), map_f(pid, t)) | | process(store, m) | → | U171(leq(m, length(store)), store, m) |
| U171(true, store, m) | → | U172(empty(fstsplit(m, store)), store, m) | | U172(false, store, m) | → | process(app(map_f(self, nil), sndsplit(m, store)), m) |
| process(store, m) | → | U181(leq(m, length(store)), store, m) | | U181(false, store, m) | → | U182(empty(fstsplit(m, app(map_f(self, nil), store))), store, m) |
| U182(false, store, m) | → | process(sndsplit(m, app(map_f(self, nil), store)), m) |
Original Signature
Termination of terms over the following signature is verified: f, app, map_f, leq, true, self, process, fstsplit, 0, s, sndsplit, empty, length, false, cons, nil
Strategy
Context-sensitive strategy:
μ(self) = μ(T) = μ(false) = μ(true) = μ(0) = μ(nil) = ∅
μ(U181) = μ(U182) = μ(length#) = μ(empty#) = μ(U181#) = μ(U171#) = μ(length) = μ(empty) = μ(U171) = μ(U172) = μ(U182#) = μ(U172#) = μ(s) = {1}
μ(leq#) = μ(map_f#) = μ(fstsplit) = μ(process#) = μ(fstsplit#) = μ(sndsplit) = μ(cons) = μ(f) = μ(app) = μ(app#) = μ(map_f) = μ(leq) = μ(process) = μ(sndsplit#) = {1, 2}
Polynomial Interpretation
- 0: 0
- U171(x,y,z): 0
- U172(x,y,z): 0
- U181(x,y,z): 0
- U182(x,y,z): 0
- app(x,y): 0
- cons(x,y): y + 1
- empty(x): 0
- f(x,y): 0
- false: 0
- fstsplit(x,y): 0
- length(x): 0
- length#(x): x
- leq(x,y): 0
- map_f(x,y): 0
- nil: 0
- process(x,y): 0
- s(x): 0
- self: 0
- sndsplit(x,y): 0
- 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:
| length#(cons(h, t)) | → | length#(t) |
Problem 5: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| fstsplit#(s(n), cons(h, t)) | → | fstsplit#(n, t) |
Rewrite Rules
| fstsplit(0, x) | → | nil | | fstsplit(s(n), nil) | → | nil |
| fstsplit(s(n), cons(h, t)) | → | cons(h, fstsplit(n, t)) | | sndsplit(0, x) | → | x |
| sndsplit(s(n), nil) | → | nil | | sndsplit(s(n), cons(h, t)) | → | sndsplit(n, t) |
| empty(nil) | → | true | | empty(cons(h, t)) | → | false |
| leq(0, m) | → | true | | leq(s(n), 0) | → | false |
| leq(s(n), s(m)) | → | leq(n, m) | | length(nil) | → | 0 |
| length(cons(h, t)) | → | s(length(t)) | | app(nil, x) | → | x |
| app(cons(h, t), x) | → | cons(h, app(t, x)) | | map_f(pid, nil) | → | nil |
| map_f(pid, cons(h, t)) | → | app(f(pid, h), map_f(pid, t)) | | process(store, m) | → | U171(leq(m, length(store)), store, m) |
| U171(true, store, m) | → | U172(empty(fstsplit(m, store)), store, m) | | U172(false, store, m) | → | process(app(map_f(self, nil), sndsplit(m, store)), m) |
| process(store, m) | → | U181(leq(m, length(store)), store, m) | | U181(false, store, m) | → | U182(empty(fstsplit(m, app(map_f(self, nil), store))), store, m) |
| U182(false, store, m) | → | process(sndsplit(m, app(map_f(self, nil), store)), m) |
Original Signature
Termination of terms over the following signature is verified: f, app, map_f, leq, true, self, process, fstsplit, 0, s, sndsplit, empty, length, false, cons, nil
Strategy
Context-sensitive strategy:
μ(self) = μ(T) = μ(false) = μ(true) = μ(0) = μ(nil) = ∅
μ(U181) = μ(U182) = μ(length#) = μ(empty#) = μ(U181#) = μ(U171#) = μ(length) = μ(empty) = μ(U171) = μ(U172) = μ(U182#) = μ(U172#) = μ(s) = {1}
μ(leq#) = μ(map_f#) = μ(fstsplit) = μ(process#) = μ(fstsplit#) = μ(sndsplit) = μ(cons) = μ(f) = μ(app) = μ(app#) = μ(map_f) = μ(leq) = μ(process) = μ(sndsplit#) = {1, 2}
Polynomial Interpretation
- 0: 0
- U171(x,y,z): 0
- U172(x,y,z): 0
- U181(x,y,z): 0
- U182(x,y,z): 0
- app(x,y): 0
- cons(x,y): 2y + 3
- empty(x): 0
- f(x,y): 0
- false: 0
- fstsplit(x,y): 0
- fstsplit#(x,y): x + 1
- length(x): 0
- leq(x,y): 0
- map_f(x,y): 0
- nil: 0
- process(x,y): 0
- s(x): x + 2
- self: 0
- sndsplit(x,y): 0
- 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:
| fstsplit#(s(n), cons(h, t)) | → | fstsplit#(n, t) |
Problem 6: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| map_f#(pid, cons(h, t)) | → | map_f#(pid, t) |
Rewrite Rules
| fstsplit(0, x) | → | nil | | fstsplit(s(n), nil) | → | nil |
| fstsplit(s(n), cons(h, t)) | → | cons(h, fstsplit(n, t)) | | sndsplit(0, x) | → | x |
| sndsplit(s(n), nil) | → | nil | | sndsplit(s(n), cons(h, t)) | → | sndsplit(n, t) |
| empty(nil) | → | true | | empty(cons(h, t)) | → | false |
| leq(0, m) | → | true | | leq(s(n), 0) | → | false |
| leq(s(n), s(m)) | → | leq(n, m) | | length(nil) | → | 0 |
| length(cons(h, t)) | → | s(length(t)) | | app(nil, x) | → | x |
| app(cons(h, t), x) | → | cons(h, app(t, x)) | | map_f(pid, nil) | → | nil |
| map_f(pid, cons(h, t)) | → | app(f(pid, h), map_f(pid, t)) | | process(store, m) | → | U171(leq(m, length(store)), store, m) |
| U171(true, store, m) | → | U172(empty(fstsplit(m, store)), store, m) | | U172(false, store, m) | → | process(app(map_f(self, nil), sndsplit(m, store)), m) |
| process(store, m) | → | U181(leq(m, length(store)), store, m) | | U181(false, store, m) | → | U182(empty(fstsplit(m, app(map_f(self, nil), store))), store, m) |
| U182(false, store, m) | → | process(sndsplit(m, app(map_f(self, nil), store)), m) |
Original Signature
Termination of terms over the following signature is verified: f, app, map_f, leq, true, self, process, fstsplit, 0, s, sndsplit, empty, length, false, cons, nil
Strategy
Context-sensitive strategy:
μ(self) = μ(T) = μ(false) = μ(true) = μ(0) = μ(nil) = ∅
μ(U181) = μ(U182) = μ(length#) = μ(empty#) = μ(U181#) = μ(U171#) = μ(length) = μ(empty) = μ(U171) = μ(U172) = μ(U182#) = μ(U172#) = μ(s) = {1}
μ(leq#) = μ(map_f#) = μ(fstsplit) = μ(process#) = μ(fstsplit#) = μ(sndsplit) = μ(cons) = μ(f) = μ(app) = μ(app#) = μ(map_f) = μ(leq) = μ(process) = μ(sndsplit#) = {1, 2}
Polynomial Interpretation
- 0: 0
- U171(x,y,z): 0
- U172(x,y,z): 0
- U181(x,y,z): 0
- U182(x,y,z): 0
- app(x,y): 0
- cons(x,y): y + 1
- empty(x): 0
- f(x,y): 0
- false: 0
- fstsplit(x,y): 0
- length(x): 0
- leq(x,y): 0
- map_f(x,y): 0
- map_f#(x,y): 2y + x + 1
- nil: 0
- process(x,y): 0
- s(x): 0
- self: 0
- sndsplit(x,y): 0
- 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:
| map_f#(pid, cons(h, t)) | → | map_f#(pid, t) |
Problem 8: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| app#(cons(h, t), x) | → | app#(t, x) |
Rewrite Rules
| fstsplit(0, x) | → | nil | | fstsplit(s(n), nil) | → | nil |
| fstsplit(s(n), cons(h, t)) | → | cons(h, fstsplit(n, t)) | | sndsplit(0, x) | → | x |
| sndsplit(s(n), nil) | → | nil | | sndsplit(s(n), cons(h, t)) | → | sndsplit(n, t) |
| empty(nil) | → | true | | empty(cons(h, t)) | → | false |
| leq(0, m) | → | true | | leq(s(n), 0) | → | false |
| leq(s(n), s(m)) | → | leq(n, m) | | length(nil) | → | 0 |
| length(cons(h, t)) | → | s(length(t)) | | app(nil, x) | → | x |
| app(cons(h, t), x) | → | cons(h, app(t, x)) | | map_f(pid, nil) | → | nil |
| map_f(pid, cons(h, t)) | → | app(f(pid, h), map_f(pid, t)) | | process(store, m) | → | U171(leq(m, length(store)), store, m) |
| U171(true, store, m) | → | U172(empty(fstsplit(m, store)), store, m) | | U172(false, store, m) | → | process(app(map_f(self, nil), sndsplit(m, store)), m) |
| process(store, m) | → | U181(leq(m, length(store)), store, m) | | U181(false, store, m) | → | U182(empty(fstsplit(m, app(map_f(self, nil), store))), store, m) |
| U182(false, store, m) | → | process(sndsplit(m, app(map_f(self, nil), store)), m) |
Original Signature
Termination of terms over the following signature is verified: f, app, map_f, leq, true, self, process, fstsplit, 0, s, sndsplit, empty, length, false, cons, nil
Strategy
Context-sensitive strategy:
μ(self) = μ(T) = μ(false) = μ(true) = μ(0) = μ(nil) = ∅
μ(U181) = μ(U182) = μ(length#) = μ(empty#) = μ(U181#) = μ(U171#) = μ(length) = μ(empty) = μ(U171) = μ(U172) = μ(U182#) = μ(U172#) = μ(s) = {1}
μ(leq#) = μ(map_f#) = μ(fstsplit) = μ(process#) = μ(fstsplit#) = μ(sndsplit) = μ(cons) = μ(f) = μ(app) = μ(app#) = μ(map_f) = μ(leq) = μ(process) = μ(sndsplit#) = {1, 2}
Polynomial Interpretation
- 0: 0
- U171(x,y,z): 0
- U172(x,y,z): 0
- U181(x,y,z): 0
- U182(x,y,z): 0
- app(x,y): 0
- app#(x,y): y + x + 1
- cons(x,y): 2y + 2
- empty(x): 0
- f(x,y): 0
- false: 0
- fstsplit(x,y): 0
- length(x): 0
- leq(x,y): 0
- map_f(x,y): 0
- nil: 0
- process(x,y): 0
- s(x): 0
- self: 0
- sndsplit(x,y): 0
- 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:
| app#(cons(h, t), x) | → | app#(t, x) |