YES
The TRS could be proven terminating. The proof took 2196 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (520ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (90ms).
| | – Problem 5 was processed with processor PolynomialLinearRange4 (22ms).
| – Problem 3 was processed with processor PolynomialLinearRange4 (625ms).
| | – Problem 6 was processed with processor DependencyGraph (8ms).
| | | – Problem 8 was processed with processor PolynomialLinearRange4 (17ms).
| | | | – Problem 10 was processed with processor PolynomialLinearRange4 (19ms).
| – Problem 4 was processed with processor PolynomialLinearRange4 (270ms).
| | – Problem 7 was processed with processor DependencyGraph (12ms).
| | | – Problem 9 was processed with processor PolynomialLinearRange4 (254ms).
| | | | – Problem 11 was processed with processor DependencyGraph (2ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U21#(tt, V1, V2) | → | U22#(isList(V1), V2) | | U22#(tt, V2) | → | isList#(V2) |
| U41#(tt, V1, V2) | → | isList#(V1) | | T(isPalListKind(x_1)) | → | T(x_1) |
| U22#(tt, V2) | → | U23#(isList(V2)) | | isList#(V) | → | isPalListKind#(V) |
| T(and(x_1, x_2)) | → | T(x_1) | | U41#(tt, V1, V2) | → | U42#(isList(V1), V2) |
| isNeList#(__(V1, V2)) | → | and#(isPalListKind(V1), isPalListKind(V2)) | | isNeList#(__(V1, V2)) | → | U51#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| T(isPal(x_1)) | → | T(x_1) | | U61#(tt, V) | → | isQid#(V) |
| isPalListKind#(__(V1, V2)) | → | and#(isPalListKind(V1), isPalListKind(V2)) | | T(isPalListKind(V2)) | → | isPalListKind#(V2) |
| isNeList#(V) | → | isPalListKind#(V) | | and#(tt, X) | → | T(X) |
| isNeList#(V) | → | U31#(isPalListKind(V), V) | | isNePal#(__(I, __(P, I))) | → | isQid#(I) |
| U42#(tt, V2) | → | isNeList#(V2) | | T(isPal(P)) | → | isPal#(P) |
| U71#(tt, V) | → | isNePal#(V) | | U21#(tt, V1, V2) | → | isList#(V1) |
| isNePal#(__(I, __(P, I))) | → | and#(isQid(I), isPalListKind(I)) | | U11#(tt, V) | → | U12#(isNeList(V)) |
| isList#(V) | → | U11#(isPalListKind(V), V) | | isPal#(V) | → | isPalListKind#(V) |
| T(isPalListKind(I)) | → | isPalListKind#(I) | | T(and(x_1, x_2)) | → | T(x_2) |
| U52#(tt, V2) | → | U53#(isList(V2)) | | U52#(tt, V2) | → | isList#(V2) |
| U71#(tt, V) | → | U72#(isNePal(V)) | | isList#(__(V1, V2)) | → | U21#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNePal#(V) | → | U61#(isPalListKind(V), V) | | U51#(tt, V1, V2) | → | isNeList#(V1) |
| U31#(tt, V) | → | U32#(isQid(V)) | | T(and(isPal(P), isPalListKind(P))) | → | and#(isPal(P), isPalListKind(P)) |
| isPalListKind#(__(V1, V2)) | → | isPalListKind#(V1) | | __#(__(X, Y), Z) | → | __#(Y, Z) |
| U11#(tt, V) | → | isNeList#(V) | | isNePal#(V) | → | isPalListKind#(V) |
| U31#(tt, V) | → | isQid#(V) | | U61#(tt, V) | → | U62#(isQid(V)) |
| T(isPalListKind(P)) | → | isPalListKind#(P) | | U51#(tt, V1, V2) | → | U52#(isNeList(V1), V2) |
| __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) | | isList#(__(V1, V2)) | → | isPalListKind#(V1) |
| isNeList#(__(V1, V2)) | → | U41#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | U42#(tt, V2) | → | U43#(isNeList(V2)) |
| isPal#(V) | → | U71#(isPalListKind(V), V) | | isList#(__(V1, V2)) | → | and#(isPalListKind(V1), isPalListKind(V2)) |
| isNeList#(__(V1, V2)) | → | isPalListKind#(V1) | | isNePal#(__(I, __(P, I))) | → | and#(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(V)) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(V1), V2) |
| U22(tt, V2) | → | U23(isList(V2)) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(V)) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(V1), V2) | | U42(tt, V2) | → | U43(isNeList(V2)) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(V1), V2) |
| U52(tt, V2) | → | U53(isList(V2)) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(V)) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(V)) | | U72(tt) | → | tt |
| and(tt, X) | → | X | | isList(V) | → | U11(isPalListKind(V), V) |
| isList(nil) | → | tt | | isList(__(V1, V2)) | → | U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(V) | → | U31(isPalListKind(V), V) | | isNeList(__(V1, V2)) | → | U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(__(V1, V2)) | → | U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | isNePal(V) | → | U61(isPalListKind(V), V) |
| isNePal(__(I, __(P, I))) | → | and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))) | | isPal(V) | → | U71(isPalListKind(V), V) |
| isPal(nil) | → | tt | | isPalListKind(a) | → | tt |
| isPalListKind(e) | → | tt | | isPalListKind(i) | → | tt |
| isPalListKind(nil) | → | tt | | isPalListKind(o) | → | tt |
| isPalListKind(u) | → | tt | | isPalListKind(__(V1, V2)) | → | and(isPalListKind(V1), isPalListKind(V2)) |
| 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, __, U62, U61, U43, U42, U41, isNePal, U23, U21, U22, e, isPalListKind, a, o, isPal, i, U71, and, U72, u, U51, tt, U53, U52, U11, U12, isQid, U31, U32, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U52#) = μ(U62) = μ(U41#) = μ(U61) = μ(U72#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U51#) = μ(and) = μ(U71) = μ(U72) = μ(U42#) = μ(U71#) = μ(U32#) = μ(U31) = μ(U32) = μ(U23#) = μ(and#) = μ(U43#) = μ(U43) = μ(U42) = μ(U41) = μ(U53#) = μ(U51) = μ(U53) = μ(U52) = μ(U11) = μ(U12) = {1}
μ(__#) = μ(__) = {1, 2}
The following SCCs where found
| isList#(__(V1, V2)) → U21#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | U22#(tt, V2) → isList#(V2) |
| U21#(tt, V1, V2) → U22#(isList(V1), V2) | U41#(tt, V1, V2) → isList#(V1) |
| U42#(tt, V2) → isNeList#(V2) | U51#(tt, V1, V2) → isNeList#(V1) |
| isNeList#(__(V1, V2)) → U41#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | U21#(tt, V1, V2) → isList#(V1) |
| U11#(tt, V) → isNeList#(V) | isList#(V) → U11#(isPalListKind(V), V) |
| U41#(tt, V1, V2) → U42#(isList(V1), V2) | isNeList#(__(V1, V2)) → U51#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| U52#(tt, V2) → isList#(V2) | U51#(tt, V1, V2) → U52#(isNeList(V1), V2) |
| and#(tt, X) → T(X) | T(isPalListKind(V2)) → isPalListKind#(V2) |
| T(isPalListKind(x_1)) → T(x_1) | T(and(isPal(P), isPalListKind(P))) → and#(isPal(P), isPalListKind(P)) |
| T(isPal(P)) → isPal#(P) | isPalListKind#(__(V1, V2)) → isPalListKind#(V1) |
| U71#(tt, V) → isNePal#(V) | T(and(x_1, x_2)) → T(x_1) |
| isPal#(V) → U71#(isPalListKind(V), V) | isNePal#(__(I, __(P, I))) → and#(isQid(I), isPalListKind(I)) |
| isPal#(V) → isPalListKind#(V) | isNePal#(V) → isPalListKind#(V) |
| T(isPalListKind(I)) → isPalListKind#(I) | T(isPal(x_1)) → T(x_1) |
| T(and(x_1, x_2)) → T(x_2) | isNePal#(__(I, __(P, I))) → and#(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))) |
| isPalListKind#(__(V1, V2)) → and#(isPalListKind(V1), isPalListKind(V2)) | T(isPalListKind(P)) → isPalListKind#(P) |
| __#(__(X, Y), Z) → __#(X, __(Y, Z)) | __#(__(X, Y), Z) → __#(Y, Z) |
Problem 2: 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, V) | → | U12(isNeList(V)) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(V1), V2) |
| U22(tt, V2) | → | U23(isList(V2)) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(V)) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(V1), V2) | | U42(tt, V2) | → | U43(isNeList(V2)) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(V1), V2) |
| U52(tt, V2) | → | U53(isList(V2)) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(V)) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(V)) | | U72(tt) | → | tt |
| and(tt, X) | → | X | | isList(V) | → | U11(isPalListKind(V), V) |
| isList(nil) | → | tt | | isList(__(V1, V2)) | → | U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(V) | → | U31(isPalListKind(V), V) | | isNeList(__(V1, V2)) | → | U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(__(V1, V2)) | → | U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | isNePal(V) | → | U61(isPalListKind(V), V) |
| isNePal(__(I, __(P, I))) | → | and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))) | | isPal(V) | → | U71(isPalListKind(V), V) |
| isPal(nil) | → | tt | | isPalListKind(a) | → | tt |
| isPalListKind(e) | → | tt | | isPalListKind(i) | → | tt |
| isPalListKind(nil) | → | tt | | isPalListKind(o) | → | tt |
| isPalListKind(u) | → | tt | | isPalListKind(__(V1, V2)) | → | and(isPalListKind(V1), isPalListKind(V2)) |
| 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, __, U62, U61, U43, U42, U41, isNePal, U23, U21, U22, e, isPalListKind, a, o, isPal, i, U71, and, U72, u, U51, tt, U53, U52, U11, U12, isQid, U31, U32, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U52#) = μ(U62) = μ(U41#) = μ(U61) = μ(U72#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U51#) = μ(U71) = μ(and) = μ(U42#) = μ(U72) = μ(U71#) = μ(U32#) = μ(U31) = μ(U32) = μ(U23#) = μ(and#) = μ(U43#) = μ(U43) = μ(U42) = μ(U41) = μ(U53#) = μ(U51) = μ(U53) = μ(U52) = μ(U11) = μ(U12) = {1}
μ(__#) = μ(__) = {1, 2}
Polynomial Interpretation
- U11(x,y): 0
- U12(x): 0
- U21(x,y,z): 0
- U22(x,y): 0
- U23(x): 0
- U31(x,y): 0
- U32(x): 0
- U41(x,y,z): 0
- U42(x,y): 0
- U43(x): 0
- U51(x,y,z): 0
- U52(x,y): 0
- U53(x): 0
- U61(x,y): 0
- U62(x): 0
- U71(x,y): 0
- U72(x): 0
- __(x,y): y + x + 1
- __#(x,y): y + x
- a: 0
- and(x,y): 0
- e: 0
- i: 0
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 0
- isPalListKind(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) | → | __#(Y, Z) |
Problem 5: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| __#(__(X, Y), Z) | → | __#(X, __(Y, Z)) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(V)) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(V1), V2) |
| U22(tt, V2) | → | U23(isList(V2)) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(V)) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(V1), V2) | | U42(tt, V2) | → | U43(isNeList(V2)) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(V1), V2) |
| U52(tt, V2) | → | U53(isList(V2)) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(V)) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(V)) | | U72(tt) | → | tt |
| and(tt, X) | → | X | | isList(V) | → | U11(isPalListKind(V), V) |
| isList(nil) | → | tt | | isList(__(V1, V2)) | → | U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(V) | → | U31(isPalListKind(V), V) | | isNeList(__(V1, V2)) | → | U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(__(V1, V2)) | → | U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | isNePal(V) | → | U61(isPalListKind(V), V) |
| isNePal(__(I, __(P, I))) | → | and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))) | | isPal(V) | → | U71(isPalListKind(V), V) |
| isPal(nil) | → | tt | | isPalListKind(a) | → | tt |
| isPalListKind(e) | → | tt | | isPalListKind(i) | → | tt |
| isPalListKind(nil) | → | tt | | isPalListKind(o) | → | tt |
| isPalListKind(u) | → | tt | | isPalListKind(__(V1, V2)) | → | and(isPalListKind(V1), isPalListKind(V2)) |
| 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, __, U62, U43, U61, U42, U41, isNePal, U23, U21, U22, e, isPalListKind, a, o, isPal, i, U71, and, U72, u, U51, tt, U53, U52, U11, U12, U31, isQid, U32, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U52#) = μ(U62) = μ(U41#) = μ(U61) = μ(U72#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U51#) = μ(and) = μ(U71) = μ(U72) = μ(U42#) = μ(U71#) = μ(U32#) = μ(U31) = μ(U32) = μ(U23#) = μ(and#) = μ(U43#) = μ(U43) = μ(U42) = μ(U41) = μ(U53#) = μ(U51) = μ(U53) = μ(U52) = μ(U11) = μ(U12) = {1}
μ(__#) = μ(__) = {1, 2}
Polynomial Interpretation
- U11(x,y): 0
- U12(x): 0
- U21(x,y,z): 0
- U22(x,y): 0
- U23(x): 0
- U31(x,y): 0
- U32(x): 0
- U41(x,y,z): 0
- U42(x,y): 0
- U43(x): 0
- U51(x,y,z): 0
- U52(x,y): 0
- U53(x): 0
- U61(x,y): 0
- U62(x): 0
- U71(x,y): 0
- U72(x): 0
- __(x,y): y + x + 1
- __#(x,y): 2x + 1
- a: 0
- and(x,y): 0
- e: 0
- i: 0
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 0
- isPalListKind(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)) |
Problem 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| T(isPalListKind(V2)) | → | isPalListKind#(V2) | | and#(tt, X) | → | T(X) |
| T(isPalListKind(x_1)) | → | T(x_1) | | T(and(isPal(P), isPalListKind(P))) | → | and#(isPal(P), isPalListKind(P)) |
| isPalListKind#(__(V1, V2)) | → | isPalListKind#(V1) | | T(isPal(P)) | → | isPal#(P) |
| U71#(tt, V) | → | isNePal#(V) | | T(and(x_1, x_2)) | → | T(x_1) |
| isPal#(V) | → | U71#(isPalListKind(V), V) | | isNePal#(__(I, __(P, I))) | → | and#(isQid(I), isPalListKind(I)) |
| isNePal#(V) | → | isPalListKind#(V) | | isPal#(V) | → | isPalListKind#(V) |
| T(isPalListKind(I)) | → | isPalListKind#(I) | | T(isPal(x_1)) | → | T(x_1) |
| T(and(x_1, x_2)) | → | T(x_2) | | isNePal#(__(I, __(P, I))) | → | and#(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))) |
| isPalListKind#(__(V1, V2)) | → | and#(isPalListKind(V1), isPalListKind(V2)) | | T(isPalListKind(P)) | → | isPalListKind#(P) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(V)) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(V1), V2) |
| U22(tt, V2) | → | U23(isList(V2)) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(V)) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(V1), V2) | | U42(tt, V2) | → | U43(isNeList(V2)) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(V1), V2) |
| U52(tt, V2) | → | U53(isList(V2)) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(V)) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(V)) | | U72(tt) | → | tt |
| and(tt, X) | → | X | | isList(V) | → | U11(isPalListKind(V), V) |
| isList(nil) | → | tt | | isList(__(V1, V2)) | → | U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(V) | → | U31(isPalListKind(V), V) | | isNeList(__(V1, V2)) | → | U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(__(V1, V2)) | → | U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | isNePal(V) | → | U61(isPalListKind(V), V) |
| isNePal(__(I, __(P, I))) | → | and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))) | | isPal(V) | → | U71(isPalListKind(V), V) |
| isPal(nil) | → | tt | | isPalListKind(a) | → | tt |
| isPalListKind(e) | → | tt | | isPalListKind(i) | → | tt |
| isPalListKind(nil) | → | tt | | isPalListKind(o) | → | tt |
| isPalListKind(u) | → | tt | | isPalListKind(__(V1, V2)) | → | and(isPalListKind(V1), isPalListKind(V2)) |
| 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, __, U62, U61, U43, U42, U41, isNePal, U23, U21, U22, e, isPalListKind, a, o, isPal, i, U71, and, U72, u, U51, tt, U53, U52, U11, U12, isQid, U31, U32, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U52#) = μ(U62) = μ(U41#) = μ(U61) = μ(U72#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U51#) = μ(U71) = μ(and) = μ(U42#) = μ(U72) = μ(U71#) = μ(U32#) = μ(U31) = μ(U32) = μ(U23#) = μ(and#) = μ(U43#) = μ(U43) = μ(U42) = μ(U41) = μ(U53#) = μ(U51) = μ(U53) = μ(U52) = μ(U11) = μ(U12) = {1}
μ(__#) = μ(__) = {1, 2}
Polynomial Interpretation
- T(x): x + 1
- U11(x,y): x
- U12(x): 0
- U21(x,y,z): 1
- U22(x,y): 1
- U23(x): 1
- U31(x,y): 2
- U32(x): 1
- U41(x,y,z): 2
- U42(x,y): 2
- U43(x): 0
- U51(x,y,z): 0
- U52(x,y): 0
- U53(x): 0
- U61(x,y): 0
- U62(x): 0
- U71(x,y): 2
- U71#(x,y): y + 3
- U72(x): 2
- __(x,y): y + 2x + 1
- a: 0
- and(x,y): y + x
- and#(x,y): y + 1
- e: 2
- i: 2
- isList(x): x
- isNeList(x): 2
- isNePal(x): x
- isNePal#(x): x + 1
- isPal(x): x + 2
- isPal#(x): x + 3
- isPalListKind(x): x
- isPalListKind#(x): x
- isQid(x): x
- nil: 0
- o: 2
- tt: 0
- u: 2
Standard Usable rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| isQid(u) | → | tt | | U21(tt, V1, V2) | → | U22(isList(V1), V2) |
| U53(tt) | → | tt | | isList(__(V1, V2)) | → | U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isPal(nil) | → | tt | | isPalListKind(e) | → | tt |
| isPal(V) | → | U71(isPalListKind(V), V) | | isPalListKind(a) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(V1), V2) | | U72(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(V)) | | U22(tt, V2) | → | U23(isList(V2)) |
| U32(tt) | → | tt | | U62(tt) | → | tt |
| isNePal(__(I, __(P, I))) | → | and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))) | | isNeList(V) | → | U31(isPalListKind(V), V) |
| isNeList(__(V1, V2)) | → | U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | isQid(o) | → | tt |
| isQid(i) | → | tt | | U43(tt) | → | tt |
| isQid(e) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(V1), V2) |
| U23(tt) | → | tt | | U12(tt) | → | tt |
| U11(tt, V) | → | U12(isNeList(V)) | | U61(tt, V) | → | U62(isQid(V)) |
| U71(tt, V) | → | U72(isNePal(V)) | | isPalListKind(nil) | → | tt |
| isPalListKind(u) | → | tt | | isPalListKind(o) | → | tt |
| U52(tt, V2) | → | U53(isList(V2)) | | isList(nil) | → | tt |
| isPalListKind(i) | → | tt | | isNeList(__(V1, V2)) | → | U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNePal(V) | → | U61(isPalListKind(V), V) | | isQid(a) | → | tt |
| and(tt, X) | → | X | | __(nil, X) | → | X |
| isPalListKind(__(V1, V2)) | → | and(isPalListKind(V1), isPalListKind(V2)) | | isList(V) | → | U11(isPalListKind(V), V) |
| U42(tt, V2) | → | U43(isNeList(V2)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| T(isPalListKind(V2)) | → | isPalListKind#(V2) | | T(and(isPal(P), isPalListKind(P))) | → | and#(isPal(P), isPalListKind(P)) |
| isPalListKind#(__(V1, V2)) | → | isPalListKind#(V1) | | U71#(tt, V) | → | isNePal#(V) |
| isNePal#(__(I, __(P, I))) | → | and#(isQid(I), isPalListKind(I)) | | isNePal#(V) | → | isPalListKind#(V) |
| isPal#(V) | → | isPalListKind#(V) | | T(isPalListKind(I)) | → | isPalListKind#(I) |
| T(isPal(x_1)) | → | T(x_1) | | T(isPalListKind(P)) | → | isPalListKind#(P) |
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| and#(tt, X) | → | T(X) | | T(isPalListKind(x_1)) | → | T(x_1) |
| T(isPal(P)) | → | isPal#(P) | | T(and(x_1, x_2)) | → | T(x_1) |
| T(and(x_1, x_2)) | → | T(x_2) | | isNePal#(__(I, __(P, I))) | → | and#(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))) |
| isPalListKind#(__(V1, V2)) | → | and#(isPalListKind(V1), isPalListKind(V2)) | | isPal#(V) | → | U71#(isPalListKind(V), V) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(V)) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(V1), V2) |
| U22(tt, V2) | → | U23(isList(V2)) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(V)) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(V1), V2) | | U42(tt, V2) | → | U43(isNeList(V2)) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(V1), V2) |
| U52(tt, V2) | → | U53(isList(V2)) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(V)) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(V)) | | U72(tt) | → | tt |
| and(tt, X) | → | X | | isList(V) | → | U11(isPalListKind(V), V) |
| isList(nil) | → | tt | | isList(__(V1, V2)) | → | U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(V) | → | U31(isPalListKind(V), V) | | isNeList(__(V1, V2)) | → | U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(__(V1, V2)) | → | U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | isNePal(V) | → | U61(isPalListKind(V), V) |
| isNePal(__(I, __(P, I))) | → | and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))) | | isPal(V) | → | U71(isPalListKind(V), V) |
| isPal(nil) | → | tt | | isPalListKind(a) | → | tt |
| isPalListKind(e) | → | tt | | isPalListKind(i) | → | tt |
| isPalListKind(nil) | → | tt | | isPalListKind(o) | → | tt |
| isPalListKind(u) | → | tt | | isPalListKind(__(V1, V2)) | → | and(isPalListKind(V1), isPalListKind(V2)) |
| 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, __, U62, U43, U61, U42, U41, isNePal, U23, U21, U22, e, isPalListKind, a, o, isPal, i, U71, and, U72, u, U51, tt, U53, U52, U11, U12, U31, isQid, U32, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U52#) = μ(U62) = μ(U41#) = μ(U61) = μ(U72#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U51#) = μ(and) = μ(U71) = μ(U72) = μ(U42#) = μ(U71#) = μ(U32#) = μ(U31) = μ(U32) = μ(U23#) = μ(and#) = μ(U43#) = μ(U43) = μ(U42) = μ(U41) = μ(U53#) = μ(U51) = μ(U53) = μ(U52) = μ(U11) = μ(U12) = {1}
μ(__#) = μ(__) = {1, 2}
The following SCCs where found
| T(isPalListKind(x_1)) → T(x_1) | T(and(x_1, x_2)) → T(x_1) |
| T(and(x_1, x_2)) → T(x_2) |
Problem 8: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| T(isPalListKind(x_1)) | → | T(x_1) | | T(and(x_1, x_2)) | → | T(x_1) |
| T(and(x_1, x_2)) | → | T(x_2) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(V)) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(V1), V2) |
| U22(tt, V2) | → | U23(isList(V2)) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(V)) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(V1), V2) | | U42(tt, V2) | → | U43(isNeList(V2)) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(V1), V2) |
| U52(tt, V2) | → | U53(isList(V2)) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(V)) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(V)) | | U72(tt) | → | tt |
| and(tt, X) | → | X | | isList(V) | → | U11(isPalListKind(V), V) |
| isList(nil) | → | tt | | isList(__(V1, V2)) | → | U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(V) | → | U31(isPalListKind(V), V) | | isNeList(__(V1, V2)) | → | U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(__(V1, V2)) | → | U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | isNePal(V) | → | U61(isPalListKind(V), V) |
| isNePal(__(I, __(P, I))) | → | and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))) | | isPal(V) | → | U71(isPalListKind(V), V) |
| isPal(nil) | → | tt | | isPalListKind(a) | → | tt |
| isPalListKind(e) | → | tt | | isPalListKind(i) | → | tt |
| isPalListKind(nil) | → | tt | | isPalListKind(o) | → | tt |
| isPalListKind(u) | → | tt | | isPalListKind(__(V1, V2)) | → | and(isPalListKind(V1), isPalListKind(V2)) |
| 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, __, U62, U43, U61, U42, U41, isNePal, U23, U21, U22, e, isPalListKind, a, o, isPal, i, U71, and, U72, u, U51, tt, U53, U52, U11, U12, U31, isQid, U32, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U52#) = μ(U62) = μ(U41#) = μ(U61) = μ(U72#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U51#) = μ(U71) = μ(and) = μ(U42#) = μ(U72) = μ(U71#) = μ(U32#) = μ(U31) = μ(U32) = μ(U23#) = μ(and#) = μ(U43#) = μ(U43) = μ(U42) = μ(U41) = μ(U53#) = μ(U51) = μ(U53) = μ(U52) = μ(U11) = μ(U12) = {1}
μ(__#) = μ(__) = {1, 2}
Polynomial Interpretation
- T(x): 3x
- U11(x,y): 0
- U12(x): 0
- U21(x,y,z): 0
- U22(x,y): 0
- U23(x): 0
- U31(x,y): 0
- U32(x): 0
- U41(x,y,z): 0
- U42(x,y): 0
- U43(x): 0
- U51(x,y,z): 0
- U52(x,y): 0
- U53(x): 0
- U61(x,y): 0
- U62(x): 0
- U71(x,y): 0
- U72(x): 0
- __(x,y): 0
- a: 0
- and(x,y): 3y + x + 1
- e: 0
- i: 0
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 0
- isPalListKind(x): 3x
- isQid(x): 0
- nil: 0
- o: 0
- tt: 0
- u: 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:
| T(and(x_1, x_2)) | → | T(x_1) | | T(and(x_1, x_2)) | → | T(x_2) |
Problem 10: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| T(isPalListKind(x_1)) | → | T(x_1) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(V)) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(V1), V2) |
| U22(tt, V2) | → | U23(isList(V2)) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(V)) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(V1), V2) | | U42(tt, V2) | → | U43(isNeList(V2)) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(V1), V2) |
| U52(tt, V2) | → | U53(isList(V2)) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(V)) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(V)) | | U72(tt) | → | tt |
| and(tt, X) | → | X | | isList(V) | → | U11(isPalListKind(V), V) |
| isList(nil) | → | tt | | isList(__(V1, V2)) | → | U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(V) | → | U31(isPalListKind(V), V) | | isNeList(__(V1, V2)) | → | U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(__(V1, V2)) | → | U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | isNePal(V) | → | U61(isPalListKind(V), V) |
| isNePal(__(I, __(P, I))) | → | and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))) | | isPal(V) | → | U71(isPalListKind(V), V) |
| isPal(nil) | → | tt | | isPalListKind(a) | → | tt |
| isPalListKind(e) | → | tt | | isPalListKind(i) | → | tt |
| isPalListKind(nil) | → | tt | | isPalListKind(o) | → | tt |
| isPalListKind(u) | → | tt | | isPalListKind(__(V1, V2)) | → | and(isPalListKind(V1), isPalListKind(V2)) |
| 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, __, U62, U61, U43, U42, U41, isNePal, U23, U21, U22, e, isPalListKind, a, o, isPal, i, U71, and, U72, u, U51, tt, U53, U52, U11, U12, isQid, U31, U32, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U52#) = μ(U62) = μ(U41#) = μ(U61) = μ(U72#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U51#) = μ(and) = μ(U71) = μ(U72) = μ(U42#) = μ(U71#) = μ(U32#) = μ(U31) = μ(U32) = μ(U23#) = μ(and#) = μ(U43#) = μ(U43) = μ(U42) = μ(U41) = μ(U53#) = μ(U51) = μ(U53) = μ(U52) = μ(U11) = μ(U12) = {1}
μ(__#) = μ(__) = {1, 2}
Polynomial Interpretation
- T(x): x + 1
- U11(x,y): 0
- U12(x): 0
- U21(x,y,z): 0
- U22(x,y): 0
- U23(x): 0
- U31(x,y): 0
- U32(x): 0
- U41(x,y,z): 0
- U42(x,y): 0
- U43(x): 0
- U51(x,y,z): 0
- U52(x,y): 0
- U53(x): 0
- U61(x,y): 0
- U62(x): 0
- U71(x,y): 0
- U72(x): 0
- __(x,y): 0
- a: 0
- and(x,y): 0
- e: 0
- i: 0
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 0
- isPalListKind(x): x + 1
- isQid(x): 0
- nil: 0
- o: 0
- tt: 0
- u: 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:
| T(isPalListKind(x_1)) | → | T(x_1) |
Problem 4: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isList#(__(V1, V2)) | → | U21#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | U41#(tt, V1, V2) | → | isList#(V1) |
| U21#(tt, V1, V2) | → | U22#(isList(V1), V2) | | U22#(tt, V2) | → | isList#(V2) |
| U51#(tt, V1, V2) | → | isNeList#(V1) | | U42#(tt, V2) | → | isNeList#(V2) |
| isNeList#(__(V1, V2)) | → | U41#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | U21#(tt, V1, V2) | → | isList#(V1) |
| isList#(V) | → | U11#(isPalListKind(V), V) | | U11#(tt, V) | → | isNeList#(V) |
| U41#(tt, V1, V2) | → | U42#(isList(V1), V2) | | isNeList#(__(V1, V2)) | → | U51#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| U52#(tt, V2) | → | isList#(V2) | | U51#(tt, V1, V2) | → | U52#(isNeList(V1), V2) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(V)) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(V1), V2) |
| U22(tt, V2) | → | U23(isList(V2)) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(V)) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(V1), V2) | | U42(tt, V2) | → | U43(isNeList(V2)) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(V1), V2) |
| U52(tt, V2) | → | U53(isList(V2)) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(V)) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(V)) | | U72(tt) | → | tt |
| and(tt, X) | → | X | | isList(V) | → | U11(isPalListKind(V), V) |
| isList(nil) | → | tt | | isList(__(V1, V2)) | → | U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(V) | → | U31(isPalListKind(V), V) | | isNeList(__(V1, V2)) | → | U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(__(V1, V2)) | → | U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | isNePal(V) | → | U61(isPalListKind(V), V) |
| isNePal(__(I, __(P, I))) | → | and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))) | | isPal(V) | → | U71(isPalListKind(V), V) |
| isPal(nil) | → | tt | | isPalListKind(a) | → | tt |
| isPalListKind(e) | → | tt | | isPalListKind(i) | → | tt |
| isPalListKind(nil) | → | tt | | isPalListKind(o) | → | tt |
| isPalListKind(u) | → | tt | | isPalListKind(__(V1, V2)) | → | and(isPalListKind(V1), isPalListKind(V2)) |
| 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, __, U62, U61, U43, U42, U41, isNePal, U23, U21, U22, e, isPalListKind, a, o, isPal, i, U71, and, U72, u, U51, tt, U53, U52, U11, U12, isQid, U31, U32, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U52#) = μ(U62) = μ(U41#) = μ(U61) = μ(U72#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U51#) = μ(U71) = μ(and) = μ(U42#) = μ(U72) = μ(U71#) = μ(U32#) = μ(U31) = μ(U32) = μ(U23#) = μ(and#) = μ(U43#) = μ(U43) = μ(U42) = μ(U41) = μ(U53#) = μ(U51) = μ(U53) = μ(U52) = μ(U11) = μ(U12) = {1}
μ(__#) = μ(__) = {1, 2}
Polynomial Interpretation
- U11(x,y): 1
- U11#(x,y): 2y
- U12(x): 1
- U21(x,y,z): 1
- U21#(x,y,z): 2z + 2y
- U22(x,y): 1
- U22#(x,y): 2y
- U23(x): 1
- U31(x,y): 1
- U32(x): 0
- U41(x,y,z): 1
- U41#(x,y,z): 2z + 2y + 2
- U42(x,y): 1
- U42#(x,y): 2y + 2
- U43(x): 0
- U51(x,y,z): 1
- U51#(x,y,z): 2z + 2y + 2
- U52(x,y): 1
- U52#(x,y): 2y + 2x
- U53(x): 0
- U61(x,y): 0
- U62(x): 0
- U71(x,y): 0
- U72(x): 0
- __(x,y): y + 2x + 1
- a: 3
- and(x,y): 2y
- e: 3
- i: 3
- isList(x): 2
- isList#(x): 2x
- isNeList(x): 1
- isNeList#(x): 2x
- isNePal(x): x
- isPal(x): 2
- isPalListKind(x): 0
- isQid(x): 3
- nil: 0
- o: 3
- tt: 0
- u: 3
Standard Usable rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| isQid(u) | → | tt | | U21(tt, V1, V2) | → | U22(isList(V1), V2) |
| U53(tt) | → | tt | | isList(__(V1, V2)) | → | U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isPal(nil) | → | tt | | isPalListKind(e) | → | tt |
| isPal(V) | → | U71(isPalListKind(V), V) | | isPalListKind(a) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(V1), V2) | | U72(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(V)) | | U22(tt, V2) | → | U23(isList(V2)) |
| U32(tt) | → | tt | | U62(tt) | → | tt |
| isNePal(__(I, __(P, I))) | → | and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))) | | isNeList(V) | → | U31(isPalListKind(V), V) |
| isNeList(__(V1, V2)) | → | U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | isQid(o) | → | tt |
| isQid(i) | → | tt | | U43(tt) | → | tt |
| isQid(e) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(V1), V2) |
| U23(tt) | → | tt | | U12(tt) | → | tt |
| U11(tt, V) | → | U12(isNeList(V)) | | U61(tt, V) | → | U62(isQid(V)) |
| U71(tt, V) | → | U72(isNePal(V)) | | isPalListKind(nil) | → | tt |
| isPalListKind(u) | → | tt | | isPalListKind(o) | → | tt |
| U52(tt, V2) | → | U53(isList(V2)) | | isList(nil) | → | tt |
| isPalListKind(i) | → | tt | | isNeList(__(V1, V2)) | → | U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNePal(V) | → | U61(isPalListKind(V), V) | | isQid(a) | → | tt |
| and(tt, X) | → | X | | __(nil, X) | → | X |
| isPalListKind(__(V1, V2)) | → | and(isPalListKind(V1), isPalListKind(V2)) | | isList(V) | → | U11(isPalListKind(V), V) |
| U42(tt, V2) | → | U43(isNeList(V2)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| isList#(__(V1, V2)) | → | U21#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | U41#(tt, V1, V2) | → | isList#(V1) |
| U51#(tt, V1, V2) | → | isNeList#(V1) | | U42#(tt, V2) | → | isNeList#(V2) |
Problem 7: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U22#(tt, V2) | → | isList#(V2) | | U21#(tt, V1, V2) | → | U22#(isList(V1), V2) |
| isNeList#(__(V1, V2)) | → | U41#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | U41#(tt, V1, V2) | → | U42#(isList(V1), V2) |
| isNeList#(__(V1, V2)) | → | U51#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | U21#(tt, V1, V2) | → | isList#(V1) |
| U51#(tt, V1, V2) | → | U52#(isNeList(V1), V2) | | U52#(tt, V2) | → | isList#(V2) |
| U11#(tt, V) | → | isNeList#(V) | | isList#(V) | → | U11#(isPalListKind(V), V) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(V)) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(V1), V2) |
| U22(tt, V2) | → | U23(isList(V2)) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(V)) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(V1), V2) | | U42(tt, V2) | → | U43(isNeList(V2)) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(V1), V2) |
| U52(tt, V2) | → | U53(isList(V2)) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(V)) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(V)) | | U72(tt) | → | tt |
| and(tt, X) | → | X | | isList(V) | → | U11(isPalListKind(V), V) |
| isList(nil) | → | tt | | isList(__(V1, V2)) | → | U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(V) | → | U31(isPalListKind(V), V) | | isNeList(__(V1, V2)) | → | U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(__(V1, V2)) | → | U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | isNePal(V) | → | U61(isPalListKind(V), V) |
| isNePal(__(I, __(P, I))) | → | and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))) | | isPal(V) | → | U71(isPalListKind(V), V) |
| isPal(nil) | → | tt | | isPalListKind(a) | → | tt |
| isPalListKind(e) | → | tt | | isPalListKind(i) | → | tt |
| isPalListKind(nil) | → | tt | | isPalListKind(o) | → | tt |
| isPalListKind(u) | → | tt | | isPalListKind(__(V1, V2)) | → | and(isPalListKind(V1), isPalListKind(V2)) |
| 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, __, U62, U43, U61, U42, U41, isNePal, U23, U21, U22, e, isPalListKind, a, o, isPal, i, U71, and, U72, u, U51, tt, U53, U52, U11, U12, U31, isQid, U32, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U52#) = μ(U62) = μ(U41#) = μ(U61) = μ(U72#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U51#) = μ(and) = μ(U71) = μ(U72) = μ(U42#) = μ(U71#) = μ(U32#) = μ(U31) = μ(U32) = μ(U23#) = μ(and#) = μ(U43#) = μ(U43) = μ(U42) = μ(U41) = μ(U53#) = μ(U51) = μ(U53) = μ(U52) = μ(U11) = μ(U12) = {1}
μ(__#) = μ(__) = {1, 2}
The following SCCs where found
| isNeList#(__(V1, V2)) → U51#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | U11#(tt, V) → isNeList#(V) |
| U51#(tt, V1, V2) → U52#(isNeList(V1), V2) | U52#(tt, V2) → isList#(V2) |
| isList#(V) → U11#(isPalListKind(V), V) |
Problem 9: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isNeList#(__(V1, V2)) | → | U51#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | U11#(tt, V) | → | isNeList#(V) |
| U51#(tt, V1, V2) | → | U52#(isNeList(V1), V2) | | U52#(tt, V2) | → | isList#(V2) |
| isList#(V) | → | U11#(isPalListKind(V), V) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(V)) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(V1), V2) |
| U22(tt, V2) | → | U23(isList(V2)) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(V)) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(V1), V2) | | U42(tt, V2) | → | U43(isNeList(V2)) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(V1), V2) |
| U52(tt, V2) | → | U53(isList(V2)) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(V)) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(V)) | | U72(tt) | → | tt |
| and(tt, X) | → | X | | isList(V) | → | U11(isPalListKind(V), V) |
| isList(nil) | → | tt | | isList(__(V1, V2)) | → | U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(V) | → | U31(isPalListKind(V), V) | | isNeList(__(V1, V2)) | → | U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(__(V1, V2)) | → | U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | isNePal(V) | → | U61(isPalListKind(V), V) |
| isNePal(__(I, __(P, I))) | → | and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))) | | isPal(V) | → | U71(isPalListKind(V), V) |
| isPal(nil) | → | tt | | isPalListKind(a) | → | tt |
| isPalListKind(e) | → | tt | | isPalListKind(i) | → | tt |
| isPalListKind(nil) | → | tt | | isPalListKind(o) | → | tt |
| isPalListKind(u) | → | tt | | isPalListKind(__(V1, V2)) | → | and(isPalListKind(V1), isPalListKind(V2)) |
| 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, __, U62, U43, U61, U42, U41, isNePal, U23, U21, U22, e, isPalListKind, a, o, isPal, i, U71, and, U72, u, U51, tt, U53, U52, U11, U12, U31, isQid, U32, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U52#) = μ(U62) = μ(U41#) = μ(U61) = μ(U72#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U51#) = μ(U71) = μ(and) = μ(U42#) = μ(U72) = μ(U71#) = μ(U32#) = μ(U31) = μ(U32) = μ(U23#) = μ(and#) = μ(U43#) = μ(U43) = μ(U42) = μ(U41) = μ(U53#) = μ(U51) = μ(U53) = μ(U52) = μ(U11) = μ(U12) = {1}
μ(__#) = μ(__) = {1, 2}
Polynomial Interpretation
- U11(x,y): 0
- U11#(x,y): y
- U12(x): 0
- U21(x,y,z): 0
- U22(x,y): 0
- U23(x): 0
- U31(x,y): y + x + 1
- U32(x): 0
- U41(x,y,z): x + 1
- U42(x,y): 1
- U43(x): 0
- U51(x,y,z): z + 2y
- U51#(x,y,z): z
- U52(x,y): y
- U52#(x,y): y
- U53(x): 0
- U61(x,y): y
- U62(x): x
- U71(x,y): 0
- U72(x): 0
- __(x,y): y + x + 1
- a: 0
- and(x,y): y
- e: 2
- i: 1
- isList(x): 0
- isList#(x): x
- isNeList(x): 2x + 1
- isNeList#(x): x
- isNePal(x): x
- isPal(x): x
- isPalListKind(x): x
- isQid(x): x
- nil: 0
- o: 0
- tt: 0
- u: 2
Standard Usable rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| isQid(u) | → | tt | | U21(tt, V1, V2) | → | U22(isList(V1), V2) |
| U53(tt) | → | tt | | isList(__(V1, V2)) | → | U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isPal(nil) | → | tt | | isPalListKind(e) | → | tt |
| isPal(V) | → | U71(isPalListKind(V), V) | | isPalListKind(a) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(V1), V2) | | U72(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(V)) | | U22(tt, V2) | → | U23(isList(V2)) |
| U32(tt) | → | tt | | U62(tt) | → | tt |
| isNePal(__(I, __(P, I))) | → | and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))) | | isNeList(V) | → | U31(isPalListKind(V), V) |
| isNeList(__(V1, V2)) | → | U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | isQid(o) | → | tt |
| isQid(i) | → | tt | | U43(tt) | → | tt |
| isQid(e) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(V1), V2) |
| U23(tt) | → | tt | | U12(tt) | → | tt |
| U11(tt, V) | → | U12(isNeList(V)) | | U61(tt, V) | → | U62(isQid(V)) |
| U71(tt, V) | → | U72(isNePal(V)) | | isPalListKind(nil) | → | tt |
| isPalListKind(u) | → | tt | | isPalListKind(o) | → | tt |
| U52(tt, V2) | → | U53(isList(V2)) | | isList(nil) | → | tt |
| isPalListKind(i) | → | tt | | isNeList(__(V1, V2)) | → | U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNePal(V) | → | U61(isPalListKind(V), V) | | isQid(a) | → | tt |
| and(tt, X) | → | X | | __(nil, X) | → | X |
| isPalListKind(__(V1, V2)) | → | and(isPalListKind(V1), isPalListKind(V2)) | | isList(V) | → | U11(isPalListKind(V), V) |
| U42(tt, V2) | → | U43(isNeList(V2)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| isNeList#(__(V1, V2)) | → | U51#(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
Problem 11: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isList#(V) | → | U11#(isPalListKind(V), V) | | U52#(tt, V2) | → | isList#(V2) |
| U51#(tt, V1, V2) | → | U52#(isNeList(V1), V2) | | U11#(tt, V) | → | isNeList#(V) |
Rewrite Rules
| __(__(X, Y), Z) | → | __(X, __(Y, Z)) | | __(X, nil) | → | X |
| __(nil, X) | → | X | | U11(tt, V) | → | U12(isNeList(V)) |
| U12(tt) | → | tt | | U21(tt, V1, V2) | → | U22(isList(V1), V2) |
| U22(tt, V2) | → | U23(isList(V2)) | | U23(tt) | → | tt |
| U31(tt, V) | → | U32(isQid(V)) | | U32(tt) | → | tt |
| U41(tt, V1, V2) | → | U42(isList(V1), V2) | | U42(tt, V2) | → | U43(isNeList(V2)) |
| U43(tt) | → | tt | | U51(tt, V1, V2) | → | U52(isNeList(V1), V2) |
| U52(tt, V2) | → | U53(isList(V2)) | | U53(tt) | → | tt |
| U61(tt, V) | → | U62(isQid(V)) | | U62(tt) | → | tt |
| U71(tt, V) | → | U72(isNePal(V)) | | U72(tt) | → | tt |
| and(tt, X) | → | X | | isList(V) | → | U11(isPalListKind(V), V) |
| isList(nil) | → | tt | | isList(__(V1, V2)) | → | U21(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(V) | → | U31(isPalListKind(V), V) | | isNeList(__(V1, V2)) | → | U41(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) |
| isNeList(__(V1, V2)) | → | U51(and(isPalListKind(V1), isPalListKind(V2)), V1, V2) | | isNePal(V) | → | U61(isPalListKind(V), V) |
| isNePal(__(I, __(P, I))) | → | and(and(isQid(I), isPalListKind(I)), and(isPal(P), isPalListKind(P))) | | isPal(V) | → | U71(isPalListKind(V), V) |
| isPal(nil) | → | tt | | isPalListKind(a) | → | tt |
| isPalListKind(e) | → | tt | | isPalListKind(i) | → | tt |
| isPalListKind(nil) | → | tt | | isPalListKind(o) | → | tt |
| isPalListKind(u) | → | tt | | isPalListKind(__(V1, V2)) | → | and(isPalListKind(V1), isPalListKind(V2)) |
| 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, __, U62, U61, U43, U42, U41, isNePal, U23, U21, U22, e, isPalListKind, a, o, isPal, i, U71, and, U72, u, U51, tt, U53, U52, U11, U12, isQid, U31, U32, nil
Strategy
Context-sensitive strategy:
μ(isNeList#) = μ(isPal) = μ(isQid) = μ(isList) = μ(isNePal#) = μ(isNeList) = μ(isPalListKind#) = μ(isQid#) = μ(T) = μ(isNePal) = μ(e) = μ(isPalListKind) = μ(a) = μ(o) = μ(isPal#) = μ(i) = μ(isList#) = μ(u) = μ(tt) = μ(nil) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U62#) = μ(U52#) = μ(U62) = μ(U41#) = μ(U61) = μ(U72#) = μ(U23) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U51#) = μ(and) = μ(U71) = μ(U72) = μ(U42#) = μ(U71#) = μ(U32#) = μ(U31) = μ(U32) = μ(U23#) = μ(and#) = μ(U43#) = μ(U43) = μ(U42) = μ(U41) = μ(U53#) = μ(U51) = μ(U53) = μ(U52) = μ(U11) = μ(U12) = {1}
μ(__#) = μ(__) = {1, 2}
There are no SCCs!