YES
The TRS could be proven terminating. The proof took 1082 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (188ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (271ms).
| | – Problem 5 was processed with processor DependencyGraph (15ms).
| | | – Problem 7 was processed with processor PolynomialLinearRange4 (85ms).
| | | | – Problem 8 was processed with processor DependencyGraph (0ms).
| – Problem 3 was processed with processor PolynomialLinearRange4 (94ms).
| – Problem 4 was processed with processor PolynomialLinearRange4 (176ms).
| | – Problem 6 was processed with processor DependencyGraph (0ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isNeList#(__(V1, V2)) | → | isNeList#(V1) | | U41#(tt, V2) | → | U42#(isNeList(V2)) |
| __#(__(X, Y), Z) | → | __#(Y, Z) | | U71#(tt, P) | → | U72#(isPal(P)) |
| isList#(V) | → | isNeList#(V) | | isNeList#(__(V1, V2)) | → | U41#(isList(V1), V2) |
| isList#(V) | → | U11#(isNeList(V)) | | isNeList#(V) | → | isQid#(V) |
| U41#(tt, V2) | → | isNeList#(V2) | | isNePal#(V) | → | isQid#(V) |
| U51#(tt, V2) | → | isList#(V2) | | U21#(tt, V2) | → | U22#(isList(V2)) |
| __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) | | isNePal#(__(I, __(P, I))) | → | isQid#(I) |
| isNeList#(__(V1, V2)) | → | U51#(isNeList(V1), V2) | | isList#(__(V1, V2)) | → | isList#(V1) |
| U21#(tt, V2) | → | isList#(V2) | | U51#(tt, V2) | → | U52#(isList(V2)) |
| isNeList#(__(V1, V2)) | → | isList#(V1) | | isList#(__(V1, V2)) | → | U21#(isList(V1), V2) |
| isNeList#(V) | → | U31#(isQid(V)) | | isNePal#(__(I, __(P, I))) | → | U71#(isQid(I), P) |
| isPal#(V) | → | U81#(isNePal(V)) | | isPal#(V) | → | isNePal#(V) |
| U71#(tt, P) | → | isPal#(P) | | isNePal#(V) | → | U61#(isQid(V)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt) | → | tt |
| U21(tt, V2) | → | U22(isList(V2)) | | U22(tt) | → | tt |
| U31(tt) | → | tt | | U41(tt, V2) | → | U42(isNeList(V2)) |
| U42(tt) | → | tt | | U51(tt, V2) | → | U52(isList(V2)) |
| U52(tt) | → | tt | | U61(tt) | → | tt |
| U71(tt, P) | → | U72(isPal(P)) | | U72(tt) | → | tt |
| U81(tt) | → | tt | | isList(V) | → | U11(isNeList(V)) |
| isList(nil) | → | tt | | isList(__(V1, V2)) | → | U21(isList(V1), V2) |
| isNeList(V) | → | U31(isQid(V)) | | isNeList(__(V1, V2)) | → | U41(isList(V1), V2) |
| isNeList(__(V1, V2)) | → | U51(isNeList(V1), V2) | | isNePal(V) | → | U61(isQid(V)) |
| isNePal(__(I, __(P, I))) | → | U71(isQid(I), P) | | isPal(V) | → | U81(isNePal(V)) |
| isPal(nil) | → | tt | | isQid(a) | → | tt |
| isQid(e) | → | tt | | isQid(i) | → | tt |
| isQid(o) | → | tt | | isQid(u) | → | tt |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, U21, U22, e, a, o, isPal, U71, i, U72, u, U51, tt, U52, U81, U11, U31, isQid, nil
Strategy
Context-sensitive strategy:
μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isQid#) = μ(T) = μ(isNePal) = μ(isNeList#) = μ(e) = μ(a) = μ(o) = μ(isPal#) = μ(isPal) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(isQid) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U81#) = μ(U52#) = μ(U41#) = μ(U61) = μ(U42) = μ(U41) = μ(U72#) = μ(U21) = μ(U22) = μ(U22#) = μ(U61#) = μ(U51#) = μ(U71) = μ(U42#) = μ(U72) = μ(U71#) = μ(U51) = μ(U52) = μ(U81) = μ(U11) = μ(U31) = {1}
μ(__) = μ(__#) = {1, 2}
The following SCCs where found
| isNePal#(__(I, __(P, I))) → U71#(isQid(I), P) | U71#(tt, P) → isPal#(P) |
| isPal#(V) → isNePal#(V) |
| isList#(V) → isNeList#(V) | isList#(__(V1, V2)) → U21#(isList(V1), V2) |
| isNeList#(__(V1, V2)) → U51#(isNeList(V1), V2) | isNeList#(__(V1, V2)) → U41#(isList(V1), V2) |
| isNeList#(__(V1, V2)) → isNeList#(V1) | isList#(__(V1, V2)) → isList#(V1) |
| U21#(tt, V2) → isList#(V2) | U41#(tt, V2) → isNeList#(V2) |
| isNeList#(__(V1, V2)) → isList#(V1) | U51#(tt, V2) → isList#(V2) |
| __#(__(X, Y), Z) → __#(X, __(Y, Z)) | __#(__(X, Y), Z) → __#(Y, Z) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isList#(V) | → | isNeList#(V) | | isList#(__(V1, V2)) | → | U21#(isList(V1), V2) |
| isNeList#(__(V1, V2)) | → | U51#(isNeList(V1), V2) | | isNeList#(__(V1, V2)) | → | U41#(isList(V1), V2) |
| isNeList#(__(V1, V2)) | → | isNeList#(V1) | | isList#(__(V1, V2)) | → | isList#(V1) |
| U21#(tt, V2) | → | isList#(V2) | | U41#(tt, V2) | → | isNeList#(V2) |
| isNeList#(__(V1, V2)) | → | isList#(V1) | | U51#(tt, V2) | → | isList#(V2) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt) | → | tt |
| U21(tt, V2) | → | U22(isList(V2)) | | U22(tt) | → | tt |
| U31(tt) | → | tt | | U41(tt, V2) | → | U42(isNeList(V2)) |
| U42(tt) | → | tt | | U51(tt, V2) | → | U52(isList(V2)) |
| U52(tt) | → | tt | | U61(tt) | → | tt |
| U71(tt, P) | → | U72(isPal(P)) | | U72(tt) | → | tt |
| U81(tt) | → | tt | | isList(V) | → | U11(isNeList(V)) |
| isList(nil) | → | tt | | isList(__(V1, V2)) | → | U21(isList(V1), V2) |
| isNeList(V) | → | U31(isQid(V)) | | isNeList(__(V1, V2)) | → | U41(isList(V1), V2) |
| isNeList(__(V1, V2)) | → | U51(isNeList(V1), V2) | | isNePal(V) | → | U61(isQid(V)) |
| isNePal(__(I, __(P, I))) | → | U71(isQid(I), P) | | isPal(V) | → | U81(isNePal(V)) |
| isPal(nil) | → | tt | | isQid(a) | → | tt |
| isQid(e) | → | tt | | isQid(i) | → | tt |
| isQid(o) | → | tt | | isQid(u) | → | tt |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, U21, U22, e, a, o, isPal, U71, i, U72, u, U51, tt, U52, U81, U11, U31, isQid, nil
Strategy
Context-sensitive strategy:
μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isQid#) = μ(T) = μ(isNePal) = μ(isNeList#) = μ(e) = μ(a) = μ(o) = μ(isPal#) = μ(isPal) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(isQid) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U81#) = μ(U52#) = μ(U41#) = μ(U61) = μ(U42) = μ(U41) = μ(U72#) = μ(U21) = μ(U22) = μ(U22#) = μ(U61#) = μ(U51#) = μ(U71) = μ(U72) = μ(U42#) = μ(U71#) = μ(U51) = μ(U81) = μ(U52) = μ(U11) = μ(U31) = {1}
μ(__) = μ(__#) = {1, 2}
Polynomial Interpretation
- U11(x): 2x
- U21(x,y): x
- U21#(x,y): 2y + x
- U22(x): 1
- U31(x): x
- U41(x,y): 2y
- U41#(x,y): 3y
- U42(x): x
- U51(x,y): y + x
- U51#(x,y): 3y
- U52(x): 1
- U61(x): 0
- U71(x,y): 0
- U72(x): 0
- U81(x): 0
- __(x,y): 2y + x
- a: 1
- e: 2
- i: 1
- isList(x): 2x
- isList#(x): 2x
- isNeList(x): x
- isNeList#(x): 2x
- isNePal(x): 0
- isPal(x): 0
- isQid(x): x
- nil: 1
- o: 2
- tt: 1
- u: 2
Standard Usable rules
| U11(tt) | → | tt | | isQid(i) | → | tt |
| isQid(e) | → | tt | | isNeList(__(V1, V2)) | → | U41(isList(V1), V2) |
| isQid(u) | → | tt | | U41(tt, V2) | → | U42(isNeList(V2)) |
| U31(tt) | → | tt | | U51(tt, V2) | → | U52(isList(V2)) |
| isNeList(V) | → | U31(isQid(V)) | | U21(tt, V2) | → | U22(isList(V2)) |
| isList(nil) | → | tt | | U42(tt) | → | tt |
| isNeList(__(V1, V2)) | → | U51(isNeList(V1), V2) | | isQid(a) | → | tt |
| isList(__(V1, V2)) | → | U21(isList(V1), V2) | | U22(tt) | → | tt |
| U52(tt) | → | tt | | isList(V) | → | U11(isNeList(V)) |
| isQid(o) | → | tt |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| U21#(tt, V2) | → | isList#(V2) |
Problem 5: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isList#(V) | → | isNeList#(V) | | isList#(__(V1, V2)) | → | U21#(isList(V1), V2) |
| isNeList#(__(V1, V2)) | → | isNeList#(V1) | | isNeList#(__(V1, V2)) | → | U41#(isList(V1), V2) |
| isNeList#(__(V1, V2)) | → | U51#(isNeList(V1), V2) | | isList#(__(V1, V2)) | → | isList#(V1) |
| U41#(tt, V2) | → | isNeList#(V2) | | isNeList#(__(V1, V2)) | → | isList#(V1) |
| U51#(tt, V2) | → | isList#(V2) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt) | → | tt |
| U21(tt, V2) | → | U22(isList(V2)) | | U22(tt) | → | tt |
| U31(tt) | → | tt | | U41(tt, V2) | → | U42(isNeList(V2)) |
| U42(tt) | → | tt | | U51(tt, V2) | → | U52(isList(V2)) |
| U52(tt) | → | tt | | U61(tt) | → | tt |
| U71(tt, P) | → | U72(isPal(P)) | | U72(tt) | → | tt |
| U81(tt) | → | tt | | isList(V) | → | U11(isNeList(V)) |
| isList(nil) | → | tt | | isList(__(V1, V2)) | → | U21(isList(V1), V2) |
| isNeList(V) | → | U31(isQid(V)) | | isNeList(__(V1, V2)) | → | U41(isList(V1), V2) |
| isNeList(__(V1, V2)) | → | U51(isNeList(V1), V2) | | isNePal(V) | → | U61(isQid(V)) |
| isNePal(__(I, __(P, I))) | → | U71(isQid(I), P) | | isPal(V) | → | U81(isNePal(V)) |
| isPal(nil) | → | tt | | isQid(a) | → | tt |
| isQid(e) | → | tt | | isQid(i) | → | tt |
| isQid(o) | → | tt | | isQid(u) | → | tt |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, U21, U22, e, a, o, isPal, U71, i, U72, u, U51, tt, U52, U81, U11, U31, isQid, nil
Strategy
Context-sensitive strategy:
μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isQid#) = μ(T) = μ(isNePal) = μ(isNeList#) = μ(e) = μ(a) = μ(o) = μ(isPal#) = μ(isPal) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(isQid) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U81#) = μ(U52#) = μ(U41#) = μ(U61) = μ(U42) = μ(U41) = μ(U72#) = μ(U21) = μ(U22) = μ(U22#) = μ(U61#) = μ(U51#) = μ(U71) = μ(U42#) = μ(U72) = μ(U71#) = μ(U51) = μ(U52) = μ(U81) = μ(U11) = μ(U31) = {1}
μ(__) = μ(__#) = {1, 2}
The following SCCs where found
| isList#(V) → isNeList#(V) | isNeList#(__(V1, V2)) → U41#(isList(V1), V2) |
| isNeList#(__(V1, V2)) → U51#(isNeList(V1), V2) | isNeList#(__(V1, V2)) → isNeList#(V1) |
| isList#(__(V1, V2)) → isList#(V1) | U41#(tt, V2) → isNeList#(V2) |
| isNeList#(__(V1, V2)) → isList#(V1) | U51#(tt, V2) → isList#(V2) |
Problem 7: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isList#(V) | → | isNeList#(V) | | isNeList#(__(V1, V2)) | → | U41#(isList(V1), V2) |
| isNeList#(__(V1, V2)) | → | U51#(isNeList(V1), V2) | | isNeList#(__(V1, V2)) | → | isNeList#(V1) |
| isList#(__(V1, V2)) | → | isList#(V1) | | U41#(tt, V2) | → | isNeList#(V2) |
| isNeList#(__(V1, V2)) | → | isList#(V1) | | U51#(tt, V2) | → | isList#(V2) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt) | → | tt |
| U21(tt, V2) | → | U22(isList(V2)) | | U22(tt) | → | tt |
| U31(tt) | → | tt | | U41(tt, V2) | → | U42(isNeList(V2)) |
| U42(tt) | → | tt | | U51(tt, V2) | → | U52(isList(V2)) |
| U52(tt) | → | tt | | U61(tt) | → | tt |
| U71(tt, P) | → | U72(isPal(P)) | | U72(tt) | → | tt |
| U81(tt) | → | tt | | isList(V) | → | U11(isNeList(V)) |
| isList(nil) | → | tt | | isList(__(V1, V2)) | → | U21(isList(V1), V2) |
| isNeList(V) | → | U31(isQid(V)) | | isNeList(__(V1, V2)) | → | U41(isList(V1), V2) |
| isNeList(__(V1, V2)) | → | U51(isNeList(V1), V2) | | isNePal(V) | → | U61(isQid(V)) |
| isNePal(__(I, __(P, I))) | → | U71(isQid(I), P) | | isPal(V) | → | U81(isNePal(V)) |
| isPal(nil) | → | tt | | isQid(a) | → | tt |
| isQid(e) | → | tt | | isQid(i) | → | tt |
| isQid(o) | → | tt | | isQid(u) | → | tt |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, U21, U22, e, a, o, isPal, U71, i, U72, u, U51, tt, U52, U81, U11, U31, isQid, nil
Strategy
Context-sensitive strategy:
μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isQid#) = μ(T) = μ(isNePal) = μ(isNeList#) = μ(e) = μ(a) = μ(o) = μ(isPal#) = μ(isPal) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(isQid) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U81#) = μ(U52#) = μ(U41#) = μ(U61) = μ(U42) = μ(U41) = μ(U72#) = μ(U21) = μ(U22) = μ(U22#) = μ(U61#) = μ(U51#) = μ(U71) = μ(U72) = μ(U42#) = μ(U71#) = μ(U51) = μ(U81) = μ(U52) = μ(U11) = μ(U31) = {1}
μ(__) = μ(__#) = {1, 2}
Polynomial Interpretation
- U11(x): 0
- U21(x,y): 0
- U22(x): 0
- U31(x): 0
- U41(x,y): 1
- U41#(x,y): y + 1
- U42(x): 1
- U51(x,y): 1
- U51#(x,y): y + x + 1
- U52(x): 1
- U61(x): 0
- U71(x,y): 0
- U72(x): 0
- U81(x): 0
- __(x,y): 2y + x + 2
- a: 3
- e: 3
- i: 0
- isList(x): 0
- isList#(x): x
- isNeList(x): 1
- isNeList#(x): x
- isNePal(x): 0
- isPal(x): 0
- isQid(x): 0
- nil: 0
- o: 3
- tt: 0
- u: 3
Standard Usable rules
| U11(tt) | → | tt | | isQid(i) | → | tt |
| isQid(e) | → | tt | | isNeList(__(V1, V2)) | → | U41(isList(V1), V2) |
| isQid(u) | → | tt | | U41(tt, V2) | → | U42(isNeList(V2)) |
| U31(tt) | → | tt | | U51(tt, V2) | → | U52(isList(V2)) |
| isNeList(V) | → | U31(isQid(V)) | | U21(tt, V2) | → | U22(isList(V2)) |
| isList(nil) | → | tt | | U42(tt) | → | tt |
| isNeList(__(V1, V2)) | → | U51(isNeList(V1), V2) | | isQid(a) | → | tt |
| isList(__(V1, V2)) | → | U21(isList(V1), V2) | | U22(tt) | → | tt |
| U52(tt) | → | tt | | isList(V) | → | U11(isNeList(V)) |
| isQid(o) | → | tt |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| isNeList#(__(V1, V2)) | → | isNeList#(V1) | | isNeList#(__(V1, V2)) | → | U41#(isList(V1), V2) |
| isList#(__(V1, V2)) | → | isList#(V1) | | U41#(tt, V2) | → | isNeList#(V2) |
| isNeList#(__(V1, V2)) | → | isList#(V1) | | U51#(tt, V2) | → | isList#(V2) |
Problem 8: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isList#(V) | → | isNeList#(V) | | isNeList#(__(V1, V2)) | → | U51#(isNeList(V1), V2) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt) | → | tt |
| U21(tt, V2) | → | U22(isList(V2)) | | U22(tt) | → | tt |
| U31(tt) | → | tt | | U41(tt, V2) | → | U42(isNeList(V2)) |
| U42(tt) | → | tt | | U51(tt, V2) | → | U52(isList(V2)) |
| U52(tt) | → | tt | | U61(tt) | → | tt |
| U71(tt, P) | → | U72(isPal(P)) | | U72(tt) | → | tt |
| U81(tt) | → | tt | | isList(V) | → | U11(isNeList(V)) |
| isList(nil) | → | tt | | isList(__(V1, V2)) | → | U21(isList(V1), V2) |
| isNeList(V) | → | U31(isQid(V)) | | isNeList(__(V1, V2)) | → | U41(isList(V1), V2) |
| isNeList(__(V1, V2)) | → | U51(isNeList(V1), V2) | | isNePal(V) | → | U61(isQid(V)) |
| isNePal(__(I, __(P, I))) | → | U71(isQid(I), P) | | isPal(V) | → | U81(isNePal(V)) |
| isPal(nil) | → | tt | | isQid(a) | → | tt |
| isQid(e) | → | tt | | isQid(i) | → | tt |
| isQid(o) | → | tt | | isQid(u) | → | tt |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, U21, U22, e, a, o, isPal, U71, i, U72, u, U51, tt, U52, U81, U11, U31, isQid, nil
Strategy
Context-sensitive strategy:
μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isQid#) = μ(T) = μ(isNePal) = μ(isNeList#) = μ(e) = μ(a) = μ(o) = μ(isPal#) = μ(isPal) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(isQid) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U81#) = μ(U52#) = μ(U41#) = μ(U61) = μ(U42) = μ(U41) = μ(U72#) = μ(U21) = μ(U22) = μ(U22#) = μ(U61#) = μ(U51#) = μ(U71) = μ(U42#) = μ(U72) = μ(U71#) = μ(U51) = μ(U52) = μ(U81) = μ(U11) = μ(U31) = {1}
μ(__) = μ(__#) = {1, 2}
There are no SCCs!
Problem 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) | | __#(__(X, Y), Z) | → | __#(Y, Z) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt) | → | tt |
| U21(tt, V2) | → | U22(isList(V2)) | | U22(tt) | → | tt |
| U31(tt) | → | tt | | U41(tt, V2) | → | U42(isNeList(V2)) |
| U42(tt) | → | tt | | U51(tt, V2) | → | U52(isList(V2)) |
| U52(tt) | → | tt | | U61(tt) | → | tt |
| U71(tt, P) | → | U72(isPal(P)) | | U72(tt) | → | tt |
| U81(tt) | → | tt | | isList(V) | → | U11(isNeList(V)) |
| isList(nil) | → | tt | | isList(__(V1, V2)) | → | U21(isList(V1), V2) |
| isNeList(V) | → | U31(isQid(V)) | | isNeList(__(V1, V2)) | → | U41(isList(V1), V2) |
| isNeList(__(V1, V2)) | → | U51(isNeList(V1), V2) | | isNePal(V) | → | U61(isQid(V)) |
| isNePal(__(I, __(P, I))) | → | U71(isQid(I), P) | | isPal(V) | → | U81(isNePal(V)) |
| isPal(nil) | → | tt | | isQid(a) | → | tt |
| isQid(e) | → | tt | | isQid(i) | → | tt |
| isQid(o) | → | tt | | isQid(u) | → | tt |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, U21, U22, e, a, o, isPal, U71, i, U72, u, U51, tt, U52, U81, U11, U31, isQid, nil
Strategy
Context-sensitive strategy:
μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isQid#) = μ(T) = μ(isNePal) = μ(isNeList#) = μ(e) = μ(a) = μ(o) = μ(isPal#) = μ(isPal) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(isQid) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U81#) = μ(U52#) = μ(U41#) = μ(U61) = μ(U42) = μ(U41) = μ(U72#) = μ(U21) = μ(U22) = μ(U22#) = μ(U61#) = μ(U51#) = μ(U71) = μ(U72) = μ(U42#) = μ(U71#) = μ(U51) = μ(U81) = μ(U52) = μ(U11) = μ(U31) = {1}
μ(__) = μ(__#) = {1, 2}
Polynomial Interpretation
- U11(x): 0
- U21(x,y): 0
- U22(x): 0
- U31(x): 0
- U41(x,y): 0
- U42(x): 0
- U51(x,y): 0
- U52(x): 0
- U61(x): 0
- U71(x,y): 0
- U72(x): 0
- U81(x): 0
- __(x,y): y + x + 1
- __#(x,y): 3x
- a: 0
- e: 0
- i: 0
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 0
- isQid(x): 0
- nil: 2
- o: 0
- tt: 0
- u: 0
Standard Usable rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) | | __#(__(X, Y), Z) | → | __#(Y, Z) |
Problem 4: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isNePal#(__(I, __(P, I))) | → | U71#(isQid(I), P) | | U71#(tt, P) | → | isPal#(P) |
| isPal#(V) | → | isNePal#(V) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt) | → | tt |
| U21(tt, V2) | → | U22(isList(V2)) | | U22(tt) | → | tt |
| U31(tt) | → | tt | | U41(tt, V2) | → | U42(isNeList(V2)) |
| U42(tt) | → | tt | | U51(tt, V2) | → | U52(isList(V2)) |
| U52(tt) | → | tt | | U61(tt) | → | tt |
| U71(tt, P) | → | U72(isPal(P)) | | U72(tt) | → | tt |
| U81(tt) | → | tt | | isList(V) | → | U11(isNeList(V)) |
| isList(nil) | → | tt | | isList(__(V1, V2)) | → | U21(isList(V1), V2) |
| isNeList(V) | → | U31(isQid(V)) | | isNeList(__(V1, V2)) | → | U41(isList(V1), V2) |
| isNeList(__(V1, V2)) | → | U51(isNeList(V1), V2) | | isNePal(V) | → | U61(isQid(V)) |
| isNePal(__(I, __(P, I))) | → | U71(isQid(I), P) | | isPal(V) | → | U81(isNePal(V)) |
| isPal(nil) | → | tt | | isQid(a) | → | tt |
| isQid(e) | → | tt | | isQid(i) | → | tt |
| isQid(o) | → | tt | | isQid(u) | → | tt |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, U21, U22, e, a, o, isPal, U71, i, U72, u, U51, tt, U52, U81, U11, U31, isQid, nil
Strategy
Context-sensitive strategy:
μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isQid#) = μ(T) = μ(isNePal) = μ(isNeList#) = μ(e) = μ(a) = μ(o) = μ(isPal#) = μ(isPal) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(isQid) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U81#) = μ(U52#) = μ(U41#) = μ(U61) = μ(U42) = μ(U41) = μ(U72#) = μ(U21) = μ(U22) = μ(U22#) = μ(U61#) = μ(U51#) = μ(U71) = μ(U72) = μ(U42#) = μ(U71#) = μ(U51) = μ(U81) = μ(U52) = μ(U11) = μ(U31) = {1}
μ(__) = μ(__#) = {1, 2}
Polynomial Interpretation
- U11(x): 0
- U21(x,y): 0
- U22(x): 0
- U31(x): 0
- U41(x,y): 0
- U42(x): 0
- U51(x,y): 0
- U52(x): 0
- U61(x): 0
- U71(x,y): 0
- U71#(x,y): 3y + x
- U72(x): 0
- U81(x): 0
- __(x,y): 2y + x
- a: 1
- e: 1
- i: 2
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isNePal#(x): 2x
- isPal(x): 0
- isPal#(x): 3x
- isQid(x): x
- nil: 0
- o: 1
- tt: 1
- u: 1
Standard Usable rules
| isQid(i) | → | tt | | isQid(e) | → | tt |
| isQid(u) | → | tt | | isQid(a) | → | tt |
| isQid(o) | → | tt |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isNePal#(__(I, __(P, I))) | → | U71#(isQid(I), P) | | isPal#(V) | → | isNePal#(V) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt) | → | tt |
| U21(tt, V2) | → | U22(isList(V2)) | | U22(tt) | → | tt |
| U31(tt) | → | tt | | U41(tt, V2) | → | U42(isNeList(V2)) |
| U42(tt) | → | tt | | U51(tt, V2) | → | U52(isList(V2)) |
| U52(tt) | → | tt | | U61(tt) | → | tt |
| U71(tt, P) | → | U72(isPal(P)) | | U72(tt) | → | tt |
| U81(tt) | → | tt | | isList(V) | → | U11(isNeList(V)) |
| isList(nil) | → | tt | | isList(__(V1, V2)) | → | U21(isList(V1), V2) |
| isNeList(V) | → | U31(isQid(V)) | | isNeList(__(V1, V2)) | → | U41(isList(V1), V2) |
| isNeList(__(V1, V2)) | → | U51(isNeList(V1), V2) | | isNePal(V) | → | U61(isQid(V)) |
| isNePal(__(I, __(P, I))) | → | U71(isQid(I), P) | | isPal(V) | → | U81(isNePal(V)) |
| isPal(nil) | → | tt | | isQid(a) | → | tt |
| isQid(e) | → | tt | | isQid(i) | → | tt |
| isQid(o) | → | tt | | isQid(u) | → | tt |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, U21, U22, e, a, o, isPal, U71, i, U72, u, U51, tt, U52, U81, U11, U31, isQid, nil
Strategy
Context-sensitive strategy:
μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isQid#) = μ(T) = μ(isNePal) = μ(isNeList#) = μ(e) = μ(a) = μ(o) = μ(isPal#) = μ(isPal) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(isQid) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U81#) = μ(U52#) = μ(U41#) = μ(U61) = μ(U42) = μ(U41) = μ(U72#) = μ(U21) = μ(U22) = μ(U22#) = μ(U61#) = μ(U51#) = μ(U71) = μ(U42#) = μ(U72) = μ(U71#) = μ(U51) = μ(U52) = μ(U81) = μ(U11) = μ(U31) = {1}
μ(__) = μ(__#) = {1, 2}
There are no SCCs!