YES
The TRS could be proven terminating. The proof took 44255 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (1115ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (341ms).
| | – Problem 7 was processed with processor PolynomialLinearRange4 (266ms).
| | | – Problem 8 was processed with processor PolynomialLinearRange4 (287ms).
| | | | – Problem 9 was processed with processor PolynomialLinearRange4 (242ms).
| | | | | – Problem 10 was processed with processor DependencyGraph (15ms).
| | | | | | – Problem 11 was processed with processor PolynomialLinearRange4 (136ms).
| | | | | | – Problem 12 was processed with processor PolynomialLinearRange4 (32ms).
| | | | | | | – Problem 13 was processed with processor PolynomialLinearRange4 (32ms).
| | | | | | | | – Problem 14 was processed with processor PolynomialLinearRange4 (44ms).
| | | | | | | | | – Problem 15 was processed with processor PolynomialLinearRange4 (61ms).
| | | | | | | | | | – Problem 16 was processed with processor PolynomialLinearRange4 (19ms).
| | | | | | | | | | | – Problem 17 was processed with processor PolynomialLinearRange4 (48ms).
| | | | | | | | | | | | – Problem 18 was processed with processor ReductionPairSAT (45ms).
| | | | | | | | | | | | | – Problem 19 was processed with processor ReductionPairSAT (90ms).
| | | | | | | | | | | | | | – Problem 20 was processed with processor ReductionPairSAT (61ms).
| | | | | | | | | | | | | | | – Problem 21 was processed with processor ReductionPairSAT (152ms).
| – Problem 3 was processed with processor SubtermCriterion (3ms).
| | – Problem 5 was processed with processor DependencyGraph (1ms).
| – Problem 4 was processed with processor SubtermCriterion (2ms).
| | – Problem 6 was processed with processor DependencyGraph (18ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a____#(__(X, Y), Z) | → | mark#(Y) | | mark#(U31(X)) | → | a__U31#(mark(X)) |
| a____#(__(X, Y), Z) | → | a____#(mark(Y), mark(Z)) | | a__U71#(tt, P) | → | a__isPal#(P) |
| mark#(U72(X)) | → | a__U72#(mark(X)) | | a__isList#(__(V1, V2)) | → | a__U21#(a__isList(V1), V2) |
| a____#(__(X, Y), Z) | → | mark#(X) | | mark#(isList(X)) | → | a__isList#(X) |
| a__isNeList#(__(V1, V2)) | → | a__isList#(V1) | | a__isNeList#(V) | → | a__U31#(a__isQid(V)) |
| mark#(U81(X)) | → | mark#(X) | | mark#(U41(X1, X2)) | → | a__U41#(mark(X1), X2) |
| a__isNePal#(__(I, __(P, I))) | → | a__U71#(a__isQid(I), P) | | a__isNeList#(__(V1, V2)) | → | a__U41#(a__isList(V1), V2) |
| mark#(__(X1, X2)) | → | mark#(X2) | | mark#(U71(X1, X2)) | → | a__U71#(mark(X1), X2) |
| a__isList#(V) | → | a__isNeList#(V) | | mark#(U72(X)) | → | mark#(X) |
| a__isNeList#(V) | → | a__isQid#(V) | | a__isPal#(V) | → | a__isNePal#(V) |
| a__isNePal#(V) | → | a__U61#(a__isQid(V)) | | a__U71#(tt, P) | → | a__U72#(a__isPal(P)) |
| a__isList#(__(V1, V2)) | → | a__isList#(V1) | | mark#(U52(X)) | → | mark#(X) |
| mark#(U71(X1, X2)) | → | mark#(X1) | | a__U21#(tt, V2) | → | a__U22#(a__isList(V2)) |
| a__isNePal#(__(I, __(P, I))) | → | a__isQid#(I) | | a__isPal#(V) | → | a__U81#(a__isNePal(V)) |
| mark#(U42(X)) | → | a__U42#(mark(X)) | | mark#(U31(X)) | → | mark#(X) |
| mark#(__(X1, X2)) | → | mark#(X1) | | mark#(isNePal(X)) | → | a__isNePal#(X) |
| a__U21#(tt, V2) | → | a__isList#(V2) | | mark#(__(X1, X2)) | → | a____#(mark(X1), mark(X2)) |
| mark#(U11(X)) | → | mark#(X) | | a____#(nil, X) | → | mark#(X) |
| mark#(U21(X1, X2)) | → | mark#(X1) | | mark#(U42(X)) | → | mark#(X) |
| mark#(U51(X1, X2)) | → | mark#(X1) | | a____#(X, nil) | → | mark#(X) |
| a____#(__(X, Y), Z) | → | mark#(Z) | | a__isList#(V) | → | a__U11#(a__isNeList(V)) |
| a____#(__(X, Y), Z) | → | a____#(mark(X), a____(mark(Y), mark(Z))) | | mark#(U22(X)) | → | a__U22#(mark(X)) |
| a__isNePal#(V) | → | a__isQid#(V) | | a__U41#(tt, V2) | → | a__U42#(a__isNeList(V2)) |
| a__U41#(tt, V2) | → | a__isNeList#(V2) | | mark#(U41(X1, X2)) | → | mark#(X1) |
| mark#(U61(X)) | → | a__U61#(mark(X)) | | mark#(U61(X)) | → | mark#(X) |
| mark#(U51(X1, X2)) | → | a__U51#(mark(X1), X2) | | a__U51#(tt, V2) | → | a__U52#(a__isList(V2)) |
| mark#(isQid(X)) | → | a__isQid#(X) | | a__U51#(tt, V2) | → | a__isList#(V2) |
| a__isNeList#(__(V1, V2)) | → | a__isNeList#(V1) | | mark#(U22(X)) | → | mark#(X) |
| mark#(U21(X1, X2)) | → | a__U21#(mark(X1), X2) | | mark#(isNeList(X)) | → | a__isNeList#(X) |
| mark#(U11(X)) | → | a__U11#(mark(X)) | | mark#(isPal(X)) | → | a__isPal#(X) |
| mark#(U52(X)) | → | a__U52#(mark(X)) | | mark#(U81(X)) | → | a__U81#(mark(X)) |
| a__isNeList#(__(V1, V2)) | → | a__U51#(a__isNeList(V1), V2) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a____, isList, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, i, U71, a__isList, U72, u, U51, tt, U52, U81, a__isPal, a__U31, U11, a__U81, a__U11, U31, isQid, a__U61, nil
Strategy
The following SCCs where found
| a__isNeList#(__(V1, V2)) → a__isList#(V1) | a__U21#(tt, V2) → a__isList#(V2) |
| a__U51#(tt, V2) → a__isList#(V2) | a__isNeList#(__(V1, V2)) → a__isNeList#(V1) |
| a__isList#(__(V1, V2)) → a__isList#(V1) | a__isList#(__(V1, V2)) → a__U21#(a__isList(V1), V2) |
| a__isNeList#(__(V1, V2)) → a__U41#(a__isList(V1), V2) | a__U41#(tt, V2) → a__isNeList#(V2) |
| a__isNeList#(__(V1, V2)) → a__U51#(a__isNeList(V1), V2) | a__isList#(V) → a__isNeList#(V) |
| a____#(__(X, Y), Z) → mark#(Y) | mark#(__(X1, X2)) → a____#(mark(X1), mark(X2)) |
| a____#(__(X, Y), Z) → a____#(mark(Y), mark(Z)) | mark#(U11(X)) → mark#(X) |
| mark#(U42(X)) → mark#(X) | a____#(nil, X) → mark#(X) |
| mark#(U21(X1, X2)) → mark#(X1) | mark#(U52(X)) → mark#(X) |
| a____#(__(X, Y), Z) → mark#(X) | a____#(X, nil) → mark#(X) |
| mark#(U51(X1, X2)) → mark#(X1) | mark#(U71(X1, X2)) → mark#(X1) |
| a____#(__(X, Y), Z) → mark#(Z) | mark#(U22(X)) → mark#(X) |
| a____#(__(X, Y), Z) → a____#(mark(X), a____(mark(Y), mark(Z))) | mark#(U81(X)) → mark#(X) |
| mark#(U31(X)) → mark#(X) | mark#(__(X1, X2)) → mark#(X1) |
| mark#(U41(X1, X2)) → mark#(X1) | mark#(U61(X)) → mark#(X) |
| mark#(__(X1, X2)) → mark#(X2) | mark#(U72(X)) → mark#(X) |
| a__isPal#(V) → a__isNePal#(V) | a__isNePal#(__(I, __(P, I))) → a__U71#(a__isQid(I), P) |
| a__U71#(tt, P) → a__isPal#(P) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| a____#(__(X, Y), Z) | → | mark#(Y) | | a____#(__(X, Y), Z) | → | a____#(mark(Y), mark(Z)) |
| mark#(__(X1, X2)) | → | a____#(mark(X1), mark(X2)) | | mark#(U11(X)) | → | mark#(X) |
| mark#(U21(X1, X2)) | → | mark#(X1) | | a____#(nil, X) | → | mark#(X) |
| mark#(U42(X)) | → | mark#(X) | | mark#(U52(X)) | → | mark#(X) |
| a____#(__(X, Y), Z) | → | mark#(X) | | mark#(U51(X1, X2)) | → | mark#(X1) |
| a____#(X, nil) | → | mark#(X) | | mark#(U71(X1, X2)) | → | mark#(X1) |
| a____#(__(X, Y), Z) | → | mark#(Z) | | mark#(U22(X)) | → | mark#(X) |
| a____#(__(X, Y), Z) | → | a____#(mark(X), a____(mark(Y), mark(Z))) | | mark#(U81(X)) | → | mark#(X) |
| mark#(U31(X)) | → | mark#(X) | | mark#(__(X1, X2)) | → | mark#(X1) |
| mark#(U41(X1, X2)) | → | mark#(X1) | | mark#(U61(X)) | → | mark#(X) |
| mark#(__(X1, X2)) | → | mark#(X2) | | mark#(U72(X)) | → | mark#(X) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a____, isList, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, i, U71, a__isList, U72, u, U51, tt, U52, U81, a__isPal, a__U31, U11, a__U81, a__U11, U31, isQid, a__U61, nil
Strategy
Polynomial Interpretation
- U11(x): x
- U21(x,y): y + x
- U22(x): x
- U31(x): x
- U41(x,y): y + x
- U42(x): x
- U51(x,y): y + x
- U52(x): x
- U61(x): x
- U71(x,y): y + x
- U72(x): x
- U81(x): x + 1
- __(x,y): y + x
- a: 1
- a__U11(x): x
- a__U21(x,y): y + x
- a__U22(x): x
- a__U31(x): x
- a__U41(x,y): y + x
- a__U42(x): x
- a__U51(x,y): y + x
- a__U52(x): x
- a__U61(x): x
- a__U71(x,y): y + x
- a__U72(x): x
- a__U81(x): x + 1
- a____(x,y): y + x
- a____#(x,y): 2y + 2x
- a__isList(x): x + 1
- a__isNeList(x): x + 1
- a__isNePal(x): x
- a__isPal(x): x + 1
- a__isQid(x): x
- e: 2
- i: 1
- isList(x): x + 1
- isNeList(x): x + 1
- isNePal(x): x
- isPal(x): x + 1
- isQid(x): x
- mark(x): x
- mark#(x): 2x
- nil: 0
- o: 1
- tt: 1
- u: 1
Standard Usable rules
| a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) | | mark(isQid(X)) | → | a__isQid(X) |
| mark(a) | → | a | | mark(isNePal(X)) | → | a__isNePal(X) |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a____(nil, X) | → | mark(X) | | a__U81(X) | → | U81(X) |
| mark(i) | → | i | | mark(o) | → | o |
| mark(U22(X)) | → | a__U22(mark(X)) | | a__isQid(e) | → | tt |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | a__isQid(a) | → | tt |
| a__U41(X1, X2) | → | U41(X1, X2) | | a__U22(X) | → | U22(X) |
| mark(tt) | → | tt | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| mark(U42(X)) | → | a__U42(mark(X)) | | mark(isPal(X)) | → | a__isPal(X) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__U61(X) | → | U61(X) |
| mark(U52(X)) | → | a__U52(mark(X)) | | a__isList(nil) | → | tt |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | a__isQid(X) | → | isQid(X) |
| mark(U72(X)) | → | a__U72(mark(X)) | | a__isNeList(V) | → | a__U31(a__isQid(V)) |
| a__U72(X) | → | U72(X) | | a__U31(X) | → | U31(X) |
| a__U11(tt) | → | tt | | mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) |
| a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) | | a__isQid(o) | → | tt |
| a__U71(X1, X2) | → | U71(X1, X2) | | mark(U31(X)) | → | a__U31(mark(X)) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__U11(X) | → | U11(X) |
| a__isNePal(V) | → | a__U61(a__isQid(V)) | | a__isList(X) | → | isList(X) |
| a__isPal(nil) | → | tt | | a__U81(tt) | → | tt |
| a__U22(tt) | → | tt | | a__U31(tt) | → | tt |
| a__isNePal(X) | → | isNePal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(U11(X)) | → | a__U11(mark(X)) | | mark(nil) | → | nil |
| a__U51(X1, X2) | → | U51(X1, X2) | | mark(U61(X)) | → | a__U61(mark(X)) |
| a__isQid(i) | → | tt | | mark(isList(X)) | → | a__isList(X) |
| a__U72(tt) | → | tt | | a__U21(X1, X2) | → | U21(X1, X2) |
| mark(u) | → | u | | a__U21(tt, V2) | → | a__U22(a__isList(V2)) |
| a__isList(V) | → | a__U11(a__isNeList(V)) | | mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) |
| a__isPal(X) | → | isPal(X) | | mark(e) | → | e |
| a____(X, nil) | → | mark(X) | | a__U61(tt) | → | tt |
| a____(X1, X2) | → | __(X1, X2) | | a__U42(X) | → | U42(X) |
| a__isNeList(X) | → | isNeList(X) | | a__isQid(u) | → | tt |
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) | | a__U52(X) | → | U52(X) |
| a__U52(tt) | → | tt | | a__U42(tt) | → | tt |
| mark(isNeList(X)) | → | a__isNeList(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
Problem 7: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| a____#(__(X, Y), Z) | → | mark#(Y) | | a____#(__(X, Y), Z) | → | a____#(mark(Y), mark(Z)) |
| mark#(__(X1, X2)) | → | a____#(mark(X1), mark(X2)) | | mark#(U11(X)) | → | mark#(X) |
| mark#(U21(X1, X2)) | → | mark#(X1) | | a____#(nil, X) | → | mark#(X) |
| mark#(U42(X)) | → | mark#(X) | | mark#(U52(X)) | → | mark#(X) |
| a____#(__(X, Y), Z) | → | mark#(X) | | mark#(U51(X1, X2)) | → | mark#(X1) |
| a____#(X, nil) | → | mark#(X) | | mark#(U71(X1, X2)) | → | mark#(X1) |
| a____#(__(X, Y), Z) | → | mark#(Z) | | mark#(U22(X)) | → | mark#(X) |
| a____#(__(X, Y), Z) | → | a____#(mark(X), a____(mark(Y), mark(Z))) | | mark#(U31(X)) | → | mark#(X) |
| mark#(U41(X1, X2)) | → | mark#(X1) | | mark#(__(X1, X2)) | → | mark#(X1) |
| mark#(U61(X)) | → | mark#(X) | | mark#(__(X1, X2)) | → | mark#(X2) |
| mark#(U72(X)) | → | mark#(X) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isList, a____, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, U71, i, a__isList, U72, u, U51, tt, U81, U52, a__isPal, U11, a__U31, a__U81, isQid, U31, a__U11, a__U61, nil
Strategy
Polynomial Interpretation
- U11(x): x
- U21(x,y): 2x
- U22(x): x
- U31(x): x
- U41(x,y): 2x
- U42(x): x
- U51(x,y): 2x
- U52(x): x
- U61(x): x
- U71(x,y): x + 1
- U72(x): x
- U81(x): 0
- __(x,y): y + x
- a: 3
- a__U11(x): x
- a__U21(x,y): 2x
- a__U22(x): x
- a__U31(x): x
- a__U41(x,y): 2x
- a__U42(x): x
- a__U51(x,y): 2x
- a__U52(x): x
- a__U61(x): x
- a__U71(x,y): x + 1
- a__U72(x): x
- a__U81(x): 0
- a____(x,y): y + x
- a____#(x,y): y + x
- a__isList(x): 0
- a__isNeList(x): 0
- a__isNePal(x): 3
- a__isPal(x): 0
- a__isQid(x): 0
- e: 1
- i: 3
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 3
- isPal(x): 0
- isQid(x): 0
- mark(x): x
- mark#(x): x
- nil: 0
- o: 1
- tt: 0
- u: 1
Standard Usable rules
| a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) | | mark(isQid(X)) | → | a__isQid(X) |
| mark(a) | → | a | | mark(isNePal(X)) | → | a__isNePal(X) |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a____(nil, X) | → | mark(X) | | a__U81(X) | → | U81(X) |
| mark(i) | → | i | | mark(o) | → | o |
| mark(U22(X)) | → | a__U22(mark(X)) | | a__isQid(e) | → | tt |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | a__isQid(a) | → | tt |
| a__U41(X1, X2) | → | U41(X1, X2) | | a__U22(X) | → | U22(X) |
| mark(tt) | → | tt | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| mark(U42(X)) | → | a__U42(mark(X)) | | mark(isPal(X)) | → | a__isPal(X) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__U61(X) | → | U61(X) |
| mark(U52(X)) | → | a__U52(mark(X)) | | a__isList(nil) | → | tt |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | a__isQid(X) | → | isQid(X) |
| mark(U72(X)) | → | a__U72(mark(X)) | | a__isNeList(V) | → | a__U31(a__isQid(V)) |
| a__U72(X) | → | U72(X) | | a__U31(X) | → | U31(X) |
| a__U11(tt) | → | tt | | mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) |
| a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) | | a__isQid(o) | → | tt |
| a__U71(X1, X2) | → | U71(X1, X2) | | mark(U31(X)) | → | a__U31(mark(X)) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__U11(X) | → | U11(X) |
| a__isNePal(V) | → | a__U61(a__isQid(V)) | | a__isList(X) | → | isList(X) |
| a__isPal(nil) | → | tt | | a__U81(tt) | → | tt |
| a__U22(tt) | → | tt | | a__U31(tt) | → | tt |
| a__isNePal(X) | → | isNePal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(U11(X)) | → | a__U11(mark(X)) | | mark(nil) | → | nil |
| a__U51(X1, X2) | → | U51(X1, X2) | | mark(U61(X)) | → | a__U61(mark(X)) |
| a__isQid(i) | → | tt | | mark(isList(X)) | → | a__isList(X) |
| a__U72(tt) | → | tt | | a__U21(X1, X2) | → | U21(X1, X2) |
| mark(u) | → | u | | a__U21(tt, V2) | → | a__U22(a__isList(V2)) |
| a__isList(V) | → | a__U11(a__isNeList(V)) | | mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) |
| a__isPal(X) | → | isPal(X) | | mark(e) | → | e |
| a____(X, nil) | → | mark(X) | | a__U61(tt) | → | tt |
| a____(X1, X2) | → | __(X1, X2) | | a__U42(X) | → | U42(X) |
| a__isNeList(X) | → | isNeList(X) | | a__isQid(u) | → | tt |
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) | | a__U52(X) | → | U52(X) |
| a__U52(tt) | → | tt | | a__U42(tt) | → | tt |
| mark(isNeList(X)) | → | a__isNeList(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(U71(X1, X2)) | → | mark#(X1) |
Problem 8: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| a____#(__(X, Y), Z) | → | mark#(Y) | | a____#(__(X, Y), Z) | → | a____#(mark(Y), mark(Z)) |
| mark#(__(X1, X2)) | → | a____#(mark(X1), mark(X2)) | | mark#(U11(X)) | → | mark#(X) |
| mark#(U21(X1, X2)) | → | mark#(X1) | | a____#(nil, X) | → | mark#(X) |
| mark#(U42(X)) | → | mark#(X) | | mark#(U52(X)) | → | mark#(X) |
| a____#(__(X, Y), Z) | → | mark#(X) | | mark#(U51(X1, X2)) | → | mark#(X1) |
| a____#(X, nil) | → | mark#(X) | | a____#(__(X, Y), Z) | → | mark#(Z) |
| mark#(U22(X)) | → | mark#(X) | | a____#(__(X, Y), Z) | → | a____#(mark(X), a____(mark(Y), mark(Z))) |
| mark#(U31(X)) | → | mark#(X) | | mark#(__(X1, X2)) | → | mark#(X1) |
| mark#(U41(X1, X2)) | → | mark#(X1) | | mark#(U61(X)) | → | mark#(X) |
| mark#(__(X1, X2)) | → | mark#(X2) | | mark#(U72(X)) | → | mark#(X) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a____, isList, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, i, U71, a__isList, U72, u, U51, tt, U52, U81, a__isPal, a__U31, U11, a__U81, a__U11, U31, isQid, a__U61, nil
Strategy
Polynomial Interpretation
- U11(x): x
- U21(x,y): 2x
- U22(x): 2x
- U31(x): 2x
- U41(x,y): x
- U42(x): 2x
- U51(x,y): x
- U52(x): x
- U61(x): x
- U71(x,y): 0
- U72(x): x
- U81(x): 0
- __(x,y): y + x
- a: 2
- a__U11(x): x
- a__U21(x,y): 2x
- a__U22(x): 2x
- a__U31(x): 2x
- a__U41(x,y): x
- a__U42(x): 2x
- a__U51(x,y): x
- a__U52(x): x
- a__U61(x): x
- a__U71(x,y): 0
- a__U72(x): x
- a__U81(x): 0
- a____(x,y): y + x
- a____#(x,y): y + x
- a__isList(x): 0
- a__isNeList(x): 0
- a__isNePal(x): 0
- a__isPal(x): 0
- a__isQid(x): 0
- e: 1
- i: 1
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 0
- isQid(x): 0
- mark(x): x
- mark#(x): x
- nil: 2
- o: 2
- tt: 0
- u: 1
Standard Usable rules
| a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) | | mark(isQid(X)) | → | a__isQid(X) |
| mark(a) | → | a | | mark(isNePal(X)) | → | a__isNePal(X) |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a____(nil, X) | → | mark(X) | | a__U81(X) | → | U81(X) |
| mark(i) | → | i | | mark(o) | → | o |
| mark(U22(X)) | → | a__U22(mark(X)) | | a__isQid(e) | → | tt |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | a__isQid(a) | → | tt |
| a__U41(X1, X2) | → | U41(X1, X2) | | a__U22(X) | → | U22(X) |
| mark(tt) | → | tt | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| mark(U42(X)) | → | a__U42(mark(X)) | | mark(isPal(X)) | → | a__isPal(X) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__U61(X) | → | U61(X) |
| mark(U52(X)) | → | a__U52(mark(X)) | | a__isList(nil) | → | tt |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | a__isQid(X) | → | isQid(X) |
| mark(U72(X)) | → | a__U72(mark(X)) | | a__isNeList(V) | → | a__U31(a__isQid(V)) |
| a__U72(X) | → | U72(X) | | a__U31(X) | → | U31(X) |
| a__U11(tt) | → | tt | | mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) |
| a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) | | a__isQid(o) | → | tt |
| a__U71(X1, X2) | → | U71(X1, X2) | | mark(U31(X)) | → | a__U31(mark(X)) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__U11(X) | → | U11(X) |
| a__isNePal(V) | → | a__U61(a__isQid(V)) | | a__isList(X) | → | isList(X) |
| a__isPal(nil) | → | tt | | a__U81(tt) | → | tt |
| a__U22(tt) | → | tt | | a__U31(tt) | → | tt |
| a__isNePal(X) | → | isNePal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(U11(X)) | → | a__U11(mark(X)) | | mark(nil) | → | nil |
| a__U51(X1, X2) | → | U51(X1, X2) | | mark(U61(X)) | → | a__U61(mark(X)) |
| a__isQid(i) | → | tt | | mark(isList(X)) | → | a__isList(X) |
| a__U72(tt) | → | tt | | a__U21(X1, X2) | → | U21(X1, X2) |
| mark(u) | → | u | | a__U21(tt, V2) | → | a__U22(a__isList(V2)) |
| a__isList(V) | → | a__U11(a__isNeList(V)) | | mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) |
| a__isPal(X) | → | isPal(X) | | mark(e) | → | e |
| a____(X, nil) | → | mark(X) | | a__U61(tt) | → | tt |
| a____(X1, X2) | → | __(X1, X2) | | a__U42(X) | → | U42(X) |
| a__isNeList(X) | → | isNeList(X) | | a__isQid(u) | → | tt |
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) | | a__U52(X) | → | U52(X) |
| a__U52(tt) | → | tt | | a__U42(tt) | → | tt |
| mark(isNeList(X)) | → | a__isNeList(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| a____#(nil, X) | → | mark#(X) | | a____#(X, nil) | → | mark#(X) |
Problem 9: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| a____#(__(X, Y), Z) | → | mark#(Y) | | a____#(__(X, Y), Z) | → | a____#(mark(Y), mark(Z)) |
| mark#(__(X1, X2)) | → | a____#(mark(X1), mark(X2)) | | mark#(U11(X)) | → | mark#(X) |
| mark#(U21(X1, X2)) | → | mark#(X1) | | mark#(U42(X)) | → | mark#(X) |
| mark#(U52(X)) | → | mark#(X) | | a____#(__(X, Y), Z) | → | mark#(X) |
| mark#(U51(X1, X2)) | → | mark#(X1) | | a____#(__(X, Y), Z) | → | mark#(Z) |
| mark#(U22(X)) | → | mark#(X) | | a____#(__(X, Y), Z) | → | a____#(mark(X), a____(mark(Y), mark(Z))) |
| mark#(U31(X)) | → | mark#(X) | | mark#(U41(X1, X2)) | → | mark#(X1) |
| mark#(__(X1, X2)) | → | mark#(X1) | | mark#(U61(X)) | → | mark#(X) |
| mark#(__(X1, X2)) | → | mark#(X2) | | mark#(U72(X)) | → | mark#(X) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isList, a____, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, U71, i, a__isList, U72, u, U51, tt, U81, U52, a__isPal, U11, a__U31, a__U81, isQid, U31, a__U11, a__U61, nil
Strategy
Polynomial Interpretation
- U11(x): 2x
- U21(x,y): x
- U22(x): x
- U31(x): x
- U41(x,y): 2x
- U42(x): 2x
- U51(x,y): x
- U52(x): x
- U61(x): 2x
- U71(x,y): y
- U72(x): x
- U81(x): 0
- __(x,y): y + x + 1
- a: 2
- a__U11(x): 2x
- a__U21(x,y): x
- a__U22(x): x
- a__U31(x): x
- a__U41(x,y): 2x
- a__U42(x): 2x
- a__U51(x,y): x
- a__U52(x): x
- a__U61(x): 2x
- a__U71(x,y): y
- a__U72(x): x
- a__U81(x): 0
- a____(x,y): y + x + 1
- a____#(x,y): 2y + 2x
- a__isList(x): 0
- a__isNeList(x): 0
- a__isNePal(x): x
- a__isPal(x): 0
- a__isQid(x): 0
- e: 0
- i: 1
- isList(x): 0
- isNeList(x): 0
- isNePal(x): x
- isPal(x): 0
- isQid(x): 0
- mark(x): x
- mark#(x): 2x
- nil: 1
- o: 3
- tt: 0
- u: 1
Standard Usable rules
| a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) | | mark(isQid(X)) | → | a__isQid(X) |
| mark(a) | → | a | | mark(isNePal(X)) | → | a__isNePal(X) |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a____(nil, X) | → | mark(X) | | a__U81(X) | → | U81(X) |
| mark(i) | → | i | | mark(o) | → | o |
| mark(U22(X)) | → | a__U22(mark(X)) | | a__isQid(e) | → | tt |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | a__isQid(a) | → | tt |
| a__U41(X1, X2) | → | U41(X1, X2) | | a__U22(X) | → | U22(X) |
| mark(tt) | → | tt | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| mark(U42(X)) | → | a__U42(mark(X)) | | mark(isPal(X)) | → | a__isPal(X) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__U61(X) | → | U61(X) |
| mark(U52(X)) | → | a__U52(mark(X)) | | a__isList(nil) | → | tt |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | a__isQid(X) | → | isQid(X) |
| mark(U72(X)) | → | a__U72(mark(X)) | | a__isNeList(V) | → | a__U31(a__isQid(V)) |
| a__U72(X) | → | U72(X) | | a__U31(X) | → | U31(X) |
| a__U11(tt) | → | tt | | mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) |
| a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) | | a__isQid(o) | → | tt |
| a__U71(X1, X2) | → | U71(X1, X2) | | mark(U31(X)) | → | a__U31(mark(X)) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__U11(X) | → | U11(X) |
| a__isNePal(V) | → | a__U61(a__isQid(V)) | | a__isList(X) | → | isList(X) |
| a__isPal(nil) | → | tt | | a__U81(tt) | → | tt |
| a__U22(tt) | → | tt | | a__U31(tt) | → | tt |
| a__isNePal(X) | → | isNePal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(U11(X)) | → | a__U11(mark(X)) | | mark(nil) | → | nil |
| a__U51(X1, X2) | → | U51(X1, X2) | | mark(U61(X)) | → | a__U61(mark(X)) |
| a__isQid(i) | → | tt | | mark(isList(X)) | → | a__isList(X) |
| a__U72(tt) | → | tt | | a__U21(X1, X2) | → | U21(X1, X2) |
| mark(u) | → | u | | a__U21(tt, V2) | → | a__U22(a__isList(V2)) |
| a__isList(V) | → | a__U11(a__isNeList(V)) | | mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) |
| a__isPal(X) | → | isPal(X) | | mark(e) | → | e |
| a____(X, nil) | → | mark(X) | | a__U61(tt) | → | tt |
| a____(X1, X2) | → | __(X1, X2) | | a__U42(X) | → | U42(X) |
| a__isNeList(X) | → | isNeList(X) | | a__isQid(u) | → | tt |
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) | | a__U52(X) | → | U52(X) |
| a__U52(tt) | → | tt | | a__U42(tt) | → | tt |
| mark(isNeList(X)) | → | a__isNeList(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| a____#(__(X, Y), Z) | → | mark#(Y) | | a____#(__(X, Y), Z) | → | a____#(mark(Y), mark(Z)) |
| mark#(__(X1, X2)) | → | a____#(mark(X1), mark(X2)) | | a____#(__(X, Y), Z) | → | mark#(X) |
| a____#(__(X, Y), Z) | → | mark#(Z) | | mark#(__(X1, X2)) | → | mark#(X1) |
| mark#(__(X1, X2)) | → | mark#(X2) |
Problem 10: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(U22(X)) | → | mark#(X) | | a____#(__(X, Y), Z) | → | a____#(mark(X), a____(mark(Y), mark(Z))) |
| mark#(U31(X)) | → | mark#(X) | | mark#(U11(X)) | → | mark#(X) |
| mark#(U42(X)) | → | mark#(X) | | mark#(U21(X1, X2)) | → | mark#(X1) |
| mark#(U41(X1, X2)) | → | mark#(X1) | | mark#(U52(X)) | → | mark#(X) |
| mark#(U61(X)) | → | mark#(X) | | mark#(U51(X1, X2)) | → | mark#(X1) |
| mark#(U72(X)) | → | mark#(X) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a____, isList, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, i, U71, a__isList, U72, u, U51, tt, U52, U81, a__isPal, a__U31, U11, a__U81, a__U11, U31, isQid, a__U61, nil
Strategy
The following SCCs where found
| a____#(__(X, Y), Z) → a____#(mark(X), a____(mark(Y), mark(Z))) |
| mark#(U22(X)) → mark#(X) | mark#(U31(X)) → mark#(X) |
| mark#(U11(X)) → mark#(X) | mark#(U42(X)) → mark#(X) |
| mark#(U21(X1, X2)) → mark#(X1) | mark#(U41(X1, X2)) → mark#(X1) |
| mark#(U52(X)) → mark#(X) | mark#(U61(X)) → mark#(X) |
| mark#(U51(X1, X2)) → mark#(X1) | mark#(U72(X)) → mark#(X) |
Problem 11: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| a____#(__(X, Y), Z) | → | a____#(mark(X), a____(mark(Y), mark(Z))) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a____, isList, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, i, U71, a__isList, U72, u, U51, tt, U52, U81, a__isPal, a__U31, U11, a__U81, a__U11, U31, isQid, a__U61, nil
Strategy
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): 1
- __(x,y): y + x + 1
- a: 0
- a__U11(x): 0
- a__U21(x,y): 0
- a__U22(x): 0
- a__U31(x): 0
- a__U41(x,y): 0
- a__U42(x): 0
- a__U51(x,y): 0
- a__U52(x): 0
- a__U61(x): 0
- a__U71(x,y): 0
- a__U72(x): 0
- a__U81(x): 1
- a____(x,y): y + x + 1
- a____#(x,y): x + 1
- a__isList(x): 0
- a__isNeList(x): 0
- a__isNePal(x): 0
- a__isPal(x): 1
- a__isQid(x): 0
- e: 1
- i: 1
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 1
- isQid(x): 0
- mark(x): x
- nil: 0
- o: 0
- tt: 0
- u: 1
Standard Usable rules
| a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) | | mark(isQid(X)) | → | a__isQid(X) |
| mark(a) | → | a | | mark(isNePal(X)) | → | a__isNePal(X) |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a____(nil, X) | → | mark(X) | | a__U81(X) | → | U81(X) |
| mark(i) | → | i | | mark(o) | → | o |
| mark(U22(X)) | → | a__U22(mark(X)) | | a__isQid(e) | → | tt |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | a__isQid(a) | → | tt |
| a__U41(X1, X2) | → | U41(X1, X2) | | a__U22(X) | → | U22(X) |
| mark(tt) | → | tt | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| mark(U42(X)) | → | a__U42(mark(X)) | | mark(isPal(X)) | → | a__isPal(X) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__U61(X) | → | U61(X) |
| mark(U52(X)) | → | a__U52(mark(X)) | | a__isList(nil) | → | tt |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | a__isQid(X) | → | isQid(X) |
| mark(U72(X)) | → | a__U72(mark(X)) | | a__isNeList(V) | → | a__U31(a__isQid(V)) |
| a__U72(X) | → | U72(X) | | a__U31(X) | → | U31(X) |
| a__U11(tt) | → | tt | | mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) |
| a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) | | a__isQid(o) | → | tt |
| a__U71(X1, X2) | → | U71(X1, X2) | | mark(U31(X)) | → | a__U31(mark(X)) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__U11(X) | → | U11(X) |
| a__isNePal(V) | → | a__U61(a__isQid(V)) | | a__isList(X) | → | isList(X) |
| a__isPal(nil) | → | tt | | a__U81(tt) | → | tt |
| a__U22(tt) | → | tt | | a__U31(tt) | → | tt |
| a__isNePal(X) | → | isNePal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(U11(X)) | → | a__U11(mark(X)) | | mark(nil) | → | nil |
| a__U51(X1, X2) | → | U51(X1, X2) | | mark(U61(X)) | → | a__U61(mark(X)) |
| a__isQid(i) | → | tt | | mark(isList(X)) | → | a__isList(X) |
| a__U72(tt) | → | tt | | a__U21(X1, X2) | → | U21(X1, X2) |
| mark(u) | → | u | | a__U21(tt, V2) | → | a__U22(a__isList(V2)) |
| a__isList(V) | → | a__U11(a__isNeList(V)) | | mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) |
| a__isPal(X) | → | isPal(X) | | mark(e) | → | e |
| a____(X, nil) | → | mark(X) | | a__U61(tt) | → | tt |
| a____(X1, X2) | → | __(X1, X2) | | a__U42(X) | → | U42(X) |
| a__isNeList(X) | → | isNeList(X) | | a__isQid(u) | → | tt |
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) | | a__U52(X) | → | U52(X) |
| a__U52(tt) | → | tt | | a__U42(tt) | → | tt |
| mark(isNeList(X)) | → | a__isNeList(X) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| a____#(__(X, Y), Z) | → | a____#(mark(X), a____(mark(Y), mark(Z))) |
Problem 12: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(U22(X)) | → | mark#(X) | | mark#(U31(X)) | → | mark#(X) |
| mark#(U11(X)) | → | mark#(X) | | mark#(U42(X)) | → | mark#(X) |
| mark#(U21(X1, X2)) | → | mark#(X1) | | mark#(U41(X1, X2)) | → | mark#(X1) |
| mark#(U52(X)) | → | mark#(X) | | mark#(U61(X)) | → | mark#(X) |
| mark#(U51(X1, X2)) | → | mark#(X1) | | mark#(U72(X)) | → | mark#(X) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a____, isList, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, i, U71, a__isList, U72, u, U51, tt, U52, U81, a__isPal, a__U31, U11, a__U81, a__U11, U31, isQid, a__U61, nil
Strategy
Polynomial Interpretation
- U11(x): x
- U21(x,y): 3y + x
- U22(x): 2x
- U31(x): x
- U41(x,y): 2x
- U42(x): 2x
- U51(x,y): x
- U52(x): 2x + 1
- U61(x): x
- U71(x,y): 0
- U72(x): x
- U81(x): 0
- __(x,y): 0
- a: 0
- a__U11(x): 0
- a__U21(x,y): 0
- a__U22(x): 0
- a__U31(x): 0
- a__U41(x,y): 0
- a__U42(x): 0
- a__U51(x,y): 0
- a__U52(x): 0
- a__U61(x): 0
- a__U71(x,y): 0
- a__U72(x): 0
- a__U81(x): 0
- a____(x,y): 0
- a__isList(x): 0
- a__isNeList(x): 0
- a__isNePal(x): 0
- a__isPal(x): 0
- a__isQid(x): 0
- e: 0
- i: 0
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 0
- isQid(x): 0
- mark(x): 0
- mark#(x): 2x
- 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:
Problem 13: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(U22(X)) | → | mark#(X) | | mark#(U11(X)) | → | mark#(X) |
| mark#(U31(X)) | → | mark#(X) | | mark#(U21(X1, X2)) | → | mark#(X1) |
| mark#(U42(X)) | → | mark#(X) | | mark#(U41(X1, X2)) | → | mark#(X1) |
| mark#(U61(X)) | → | mark#(X) | | mark#(U51(X1, X2)) | → | mark#(X1) |
| mark#(U72(X)) | → | mark#(X) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isList, a____, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, U71, i, a__isList, U72, u, U51, tt, U81, U52, a__isPal, U11, a__U31, a__U81, isQid, U31, a__U11, a__U61, nil
Strategy
Polynomial Interpretation
- U11(x): 2x + 1
- U21(x,y): 2x
- U22(x): x
- U31(x): 2x
- U41(x,y): x
- U42(x): 3x
- U51(x,y): x
- U52(x): 0
- U61(x): 2x
- U71(x,y): 0
- U72(x): x
- U81(x): 0
- __(x,y): 0
- a: 0
- a__U11(x): 0
- a__U21(x,y): 0
- a__U22(x): 0
- a__U31(x): 0
- a__U41(x,y): 0
- a__U42(x): 0
- a__U51(x,y): 0
- a__U52(x): 0
- a__U61(x): 0
- a__U71(x,y): 0
- a__U72(x): 0
- a__U81(x): 0
- a____(x,y): 0
- a__isList(x): 0
- a__isNeList(x): 0
- a__isNePal(x): 0
- a__isPal(x): 0
- a__isQid(x): 0
- e: 0
- i: 0
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 0
- isQid(x): 0
- mark(x): 0
- mark#(x): 2x
- 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:
Problem 14: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(U22(X)) | → | mark#(X) | | mark#(U31(X)) | → | mark#(X) |
| mark#(U42(X)) | → | mark#(X) | | mark#(U21(X1, X2)) | → | mark#(X1) |
| mark#(U41(X1, X2)) | → | mark#(X1) | | mark#(U61(X)) | → | mark#(X) |
| mark#(U51(X1, X2)) | → | mark#(X1) | | mark#(U72(X)) | → | mark#(X) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a____, isList, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, i, U71, a__isList, U72, u, U51, tt, U52, U81, a__isPal, a__U31, U11, a__U81, a__U11, U31, isQid, a__U61, nil
Strategy
Polynomial Interpretation
- U11(x): 0
- U21(x,y): x
- U22(x): 3x + 1
- U31(x): 2x
- U41(x,y): x
- U42(x): x
- U51(x,y): x
- U52(x): 0
- U61(x): 2x
- U71(x,y): 0
- U72(x): x
- U81(x): 0
- __(x,y): 0
- a: 0
- a__U11(x): 0
- a__U21(x,y): 0
- a__U22(x): 0
- a__U31(x): 0
- a__U41(x,y): 0
- a__U42(x): 0
- a__U51(x,y): 0
- a__U52(x): 0
- a__U61(x): 0
- a__U71(x,y): 0
- a__U72(x): 0
- a__U81(x): 0
- a____(x,y): 0
- a__isList(x): 0
- a__isNeList(x): 0
- a__isNePal(x): 0
- a__isPal(x): 0
- a__isQid(x): 0
- e: 0
- i: 0
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 0
- isQid(x): 0
- mark(x): 0
- mark#(x): 2x
- 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:
Problem 15: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(U31(X)) | → | mark#(X) | | mark#(U21(X1, X2)) | → | mark#(X1) |
| mark#(U42(X)) | → | mark#(X) | | mark#(U41(X1, X2)) | → | mark#(X1) |
| mark#(U61(X)) | → | mark#(X) | | mark#(U51(X1, X2)) | → | mark#(X1) |
| mark#(U72(X)) | → | mark#(X) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isList, a____, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, U71, i, a__isList, U72, u, U51, tt, U81, U52, a__isPal, U11, a__U31, a__U81, isQid, U31, a__U11, a__U61, nil
Strategy
Polynomial Interpretation
- U11(x): 0
- U21(x,y): 2y + 2x
- U22(x): 0
- U31(x): x
- U41(x,y): 2x
- U42(x): x
- U51(x,y): x
- U52(x): 0
- U61(x): x + 1
- U71(x,y): 0
- U72(x): x
- U81(x): 0
- __(x,y): 0
- a: 0
- a__U11(x): 0
- a__U21(x,y): 0
- a__U22(x): 0
- a__U31(x): 0
- a__U41(x,y): 0
- a__U42(x): 0
- a__U51(x,y): 0
- a__U52(x): 0
- a__U61(x): 0
- a__U71(x,y): 0
- a__U72(x): 0
- a__U81(x): 0
- a____(x,y): 0
- a__isList(x): 0
- a__isNeList(x): 0
- a__isNePal(x): 0
- a__isPal(x): 0
- a__isQid(x): 0
- e: 0
- i: 0
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 0
- isQid(x): 0
- mark(x): 0
- mark#(x): x
- 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:
Problem 16: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(U31(X)) | → | mark#(X) | | mark#(U42(X)) | → | mark#(X) |
| mark#(U21(X1, X2)) | → | mark#(X1) | | mark#(U41(X1, X2)) | → | mark#(X1) |
| mark#(U51(X1, X2)) | → | mark#(X1) | | mark#(U72(X)) | → | mark#(X) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a____, isList, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, i, U71, a__isList, U72, u, U51, tt, U52, U81, a__isPal, a__U31, U11, a__U81, a__U11, U31, isQid, a__U61, nil
Strategy
Polynomial Interpretation
- U11(x): 0
- U21(x,y): x
- U22(x): 0
- U31(x): 2x
- U41(x,y): y + 2x
- U42(x): 2x
- U51(x,y): 2y + x + 1
- U52(x): 0
- U61(x): 0
- U71(x,y): 0
- U72(x): 2x
- U81(x): 0
- __(x,y): 0
- a: 0
- a__U11(x): 0
- a__U21(x,y): 0
- a__U22(x): 0
- a__U31(x): 0
- a__U41(x,y): 0
- a__U42(x): 0
- a__U51(x,y): 0
- a__U52(x): 0
- a__U61(x): 0
- a__U71(x,y): 0
- a__U72(x): 0
- a__U81(x): 0
- a____(x,y): 0
- a__isList(x): 0
- a__isNeList(x): 0
- a__isNePal(x): 0
- a__isPal(x): 0
- a__isQid(x): 0
- e: 0
- i: 0
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 0
- isQid(x): 0
- mark(x): 0
- mark#(x): x
- 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:
| mark#(U51(X1, X2)) | → | mark#(X1) |
Problem 17: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(U31(X)) | → | mark#(X) | | mark#(U21(X1, X2)) | → | mark#(X1) |
| mark#(U42(X)) | → | mark#(X) | | mark#(U41(X1, X2)) | → | mark#(X1) |
| mark#(U72(X)) | → | mark#(X) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isList, a____, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, U71, i, a__isList, U72, u, U51, tt, U81, U52, a__isPal, U11, a__U31, a__U81, isQid, U31, a__U11, a__U61, nil
Strategy
Polynomial Interpretation
- U11(x): 0
- U21(x,y): 2y + x + 1
- U22(x): 0
- U31(x): x
- U41(x,y): 3x
- U42(x): x
- U51(x,y): 0
- U52(x): 0
- U61(x): 0
- U71(x,y): 0
- U72(x): x
- U81(x): 0
- __(x,y): 0
- a: 0
- a__U11(x): 0
- a__U21(x,y): 0
- a__U22(x): 0
- a__U31(x): 0
- a__U41(x,y): 0
- a__U42(x): 0
- a__U51(x,y): 0
- a__U52(x): 0
- a__U61(x): 0
- a__U71(x,y): 0
- a__U72(x): 0
- a__U81(x): 0
- a____(x,y): 0
- a__isList(x): 0
- a__isNeList(x): 0
- a__isNePal(x): 0
- a__isPal(x): 0
- a__isQid(x): 0
- e: 0
- i: 0
- isList(x): 0
- isNeList(x): 0
- isNePal(x): 0
- isPal(x): 0
- isQid(x): 0
- mark(x): 0
- mark#(x): x
- 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:
| mark#(U21(X1, X2)) | → | mark#(X1) |
Problem 18: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| mark#(U31(X)) | → | mark#(X) | | mark#(U42(X)) | → | mark#(X) |
| mark#(U41(X1, X2)) | → | mark#(X1) | | mark#(U72(X)) | → | mark#(X) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a____, isList, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, i, U71, a__isList, U72, u, U51, tt, U52, U81, a__isPal, a__U31, U11, a__U81, a__U11, U31, isQid, a__U61, nil
Strategy
Function Precedence
U41 = U72 = U31 < U42 < a__U51 = a__U52 = a____ = isList = a__isQid = isNeList = __ = a__isNePal = U61 = isNePal = a__isNeList = a__U41 = a__U22 = a__U72 = a__U42 = a__U71 = a__U21 = U21 = U22 = e = a = o = mark = isPal = mark# = U71 = i = a__isList = u = U51 = tt = U52 = U81 = a__isPal = U11 = a__U31 = a__U81 = isQid = a__U11 = a__U61 = nil
Argument Filtering
a__U51: all arguments are removed from a__U51
a__U52: all arguments are removed from a__U52
a____: all arguments are removed from a____
isList: all arguments are removed from isList
a__isQid: all arguments are removed from a__isQid
isNeList: all arguments are removed from isNeList
__: all arguments are removed from __
a__isNePal: all arguments are removed from a__isNePal
U61: all arguments are removed from U61
U42: 1
U41: collapses to 1
isNePal: all arguments are removed from isNePal
a__isNeList: all arguments are removed from a__isNeList
a__U41: all arguments are removed from a__U41
a__U22: all arguments are removed from a__U22
a__U72: all arguments are removed from a__U72
a__U42: all arguments are removed from a__U42
a__U71: all arguments are removed from a__U71
a__U21: all arguments are removed from a__U21
U21: all arguments are removed from U21
U22: all arguments are removed from U22
e: all arguments are removed from e
a: all arguments are removed from a
o: all arguments are removed from o
mark: all arguments are removed from mark
isPal: all arguments are removed from isPal
mark#: collapses to 1
U71: 1 2
i: all arguments are removed from i
a__isList: all arguments are removed from a__isList
U72: collapses to 1
u: all arguments are removed from u
U51: 1 2
tt: all arguments are removed from tt
U52: all arguments are removed from U52
U81: all arguments are removed from U81
a__isPal: all arguments are removed from a__isPal
U11: 1
a__U31: all arguments are removed from a__U31
a__U81: all arguments are removed from a__U81
U31: collapses to 1
isQid: all arguments are removed from isQid
a__U11: all arguments are removed from a__U11
a__U61: all arguments are removed from a__U61
nil: all arguments are removed from nil
Status
a__U51: multiset
a__U52: multiset
a____: multiset
isList: multiset
a__isQid: multiset
isNeList: multiset
__: multiset
a__isNePal: multiset
U61: multiset
U42: multiset
isNePal: multiset
a__isNeList: multiset
a__U41: multiset
a__U22: multiset
a__U72: multiset
a__U42: multiset
a__U71: multiset
a__U21: multiset
U21: multiset
U22: multiset
e: multiset
a: multiset
o: multiset
mark: multiset
isPal: multiset
U71: lexicographic with permutation 1 → 2 2 → 1
i: multiset
a__isList: multiset
u: multiset
U51: lexicographic with permutation 1 → 1 2 → 2
tt: multiset
U52: multiset
U81: multiset
a__isPal: multiset
U11: lexicographic with permutation 1 → 1
a__U31: multiset
a__U81: multiset
isQid: multiset
a__U11: multiset
a__U61: multiset
nil: multiset
Usable Rules
There are no usable rules.
The dependency pairs and usable rules are stronlgy conservative!
Eliminated dependency pairs
The following dependency pairs (at least) can be eliminated according to the given precedence.
Problem 19: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| mark#(U31(X)) | → | mark#(X) | | mark#(U41(X1, X2)) | → | mark#(X1) |
| mark#(U72(X)) | → | mark#(X) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isList, a____, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, U71, i, a__isList, U72, u, U51, tt, U81, U52, a__isPal, U11, a__U31, a__U81, isQid, U31, a__U11, a__U61, nil
Strategy
Function Precedence
U41 = U31 < a__U51 = a__U52 = a____ = isList = a__isQid = isNeList = __ = a__isNePal = U61 = U42 = isNePal = a__isNeList = a__U41 = a__U22 = a__U72 = a__U42 = a__U71 = a__U21 = U21 = U22 = e = a = o = mark = isPal = mark# = U71 = i = a__isList = U72 = u = U51 = tt = U52 = U81 = a__isPal = U11 = a__U31 = a__U81 = isQid = a__U11 = a__U61 = nil
Argument Filtering
a__U51: all arguments are removed from a__U51
a__U52: all arguments are removed from a__U52
a____: all arguments are removed from a____
isList: all arguments are removed from isList
a__isQid: all arguments are removed from a__isQid
isNeList: all arguments are removed from isNeList
__: all arguments are removed from __
a__isNePal: all arguments are removed from a__isNePal
U61: all arguments are removed from U61
U42: all arguments are removed from U42
U41: collapses to 1
isNePal: all arguments are removed from isNePal
a__isNeList: all arguments are removed from a__isNeList
a__U41: all arguments are removed from a__U41
a__U22: all arguments are removed from a__U22
a__U72: all arguments are removed from a__U72
a__U42: all arguments are removed from a__U42
a__U71: all arguments are removed from a__U71
a__U21: all arguments are removed from a__U21
U21: all arguments are removed from U21
U22: all arguments are removed from U22
e: all arguments are removed from e
a: all arguments are removed from a
o: all arguments are removed from o
mark: all arguments are removed from mark
isPal: 1
mark#: collapses to 1
U71: all arguments are removed from U71
i: all arguments are removed from i
a__isList: collapses to 1
U72: 1
u: all arguments are removed from u
U51: all arguments are removed from U51
tt: all arguments are removed from tt
U52: all arguments are removed from U52
U81: all arguments are removed from U81
a__isPal: all arguments are removed from a__isPal
U11: all arguments are removed from U11
a__U31: all arguments are removed from a__U31
a__U81: all arguments are removed from a__U81
U31: collapses to 1
isQid: all arguments are removed from isQid
a__U11: 1
a__U61: all arguments are removed from a__U61
nil: all arguments are removed from nil
Status
a__U51: multiset
a__U52: multiset
a____: multiset
isList: multiset
a__isQid: multiset
isNeList: multiset
__: multiset
a__isNePal: multiset
U61: multiset
U42: multiset
isNePal: multiset
a__isNeList: multiset
a__U41: multiset
a__U22: multiset
a__U72: multiset
a__U42: multiset
a__U71: multiset
a__U21: multiset
U21: multiset
U22: multiset
e: multiset
a: multiset
o: multiset
mark: multiset
isPal: lexicographic with permutation 1 → 1
U71: multiset
i: multiset
U72: multiset
u: multiset
U51: multiset
tt: multiset
U52: multiset
U81: multiset
a__isPal: multiset
U11: multiset
a__U31: multiset
a__U81: multiset
isQid: multiset
a__U11: lexicographic with permutation 1 → 1
a__U61: multiset
nil: multiset
Usable Rules
There are no usable rules.
The dependency pairs and usable rules are stronlgy conservative!
Eliminated dependency pairs
The following dependency pairs (at least) can be eliminated according to the given precedence.
Problem 20: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| mark#(U31(X)) | → | mark#(X) | | mark#(U41(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a____, isList, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, i, U71, a__isList, U72, u, U51, tt, U52, U81, a__isPal, a__U31, U11, a__U81, a__U11, U31, isQid, a__U61, nil
Strategy
Function Precedence
U41 = U31 < mark# < a__U51 = a__U52 = a____ = isList = a__isQid = isNeList = __ = a__isNePal = U61 = U42 = isNePal = a__isNeList = a__U41 = a__U22 = a__U72 = a__U42 = a__U71 = a__U21 = U21 = U22 = e = a = o = mark = isPal = U71 = i = a__isList = U72 = u = U51 = tt = U52 = U81 = a__isPal = U11 = a__U31 = a__U81 = isQid = a__U11 = a__U61 = nil
Argument Filtering
a__U51: all arguments are removed from a__U51
a__U52: all arguments are removed from a__U52
a____: all arguments are removed from a____
isList: all arguments are removed from isList
a__isQid: all arguments are removed from a__isQid
isNeList: all arguments are removed from isNeList
__: all arguments are removed from __
a__isNePal: all arguments are removed from a__isNePal
U61: all arguments are removed from U61
U42: all arguments are removed from U42
U41: collapses to 1
isNePal: all arguments are removed from isNePal
a__isNeList: all arguments are removed from a__isNeList
a__U41: all arguments are removed from a__U41
a__U22: all arguments are removed from a__U22
a__U72: all arguments are removed from a__U72
a__U42: all arguments are removed from a__U42
a__U71: all arguments are removed from a__U71
a__U21: all arguments are removed from a__U21
U21: all arguments are removed from U21
U22: all arguments are removed from U22
e: all arguments are removed from e
a: all arguments are removed from a
o: all arguments are removed from o
mark: all arguments are removed from mark
isPal: all arguments are removed from isPal
mark#: collapses to 1
U71: all arguments are removed from U71
i: all arguments are removed from i
a__isList: all arguments are removed from a__isList
U72: all arguments are removed from U72
u: all arguments are removed from u
U51: all arguments are removed from U51
tt: all arguments are removed from tt
U52: all arguments are removed from U52
U81: all arguments are removed from U81
a__isPal: all arguments are removed from a__isPal
U11: all arguments are removed from U11
a__U31: all arguments are removed from a__U31
a__U81: all arguments are removed from a__U81
U31: 1
isQid: all arguments are removed from isQid
a__U11: all arguments are removed from a__U11
a__U61: all arguments are removed from a__U61
nil: all arguments are removed from nil
Status
a__U51: multiset
a__U52: multiset
a____: multiset
isList: multiset
a__isQid: multiset
isNeList: multiset
__: multiset
a__isNePal: multiset
U61: multiset
U42: multiset
isNePal: multiset
a__isNeList: multiset
a__U41: multiset
a__U22: multiset
a__U72: multiset
a__U42: multiset
a__U71: multiset
a__U21: multiset
U21: multiset
U22: multiset
e: multiset
a: multiset
o: multiset
mark: multiset
isPal: multiset
U71: multiset
i: multiset
a__isList: multiset
U72: multiset
u: multiset
U51: multiset
tt: multiset
U52: multiset
U81: multiset
a__isPal: multiset
U11: multiset
a__U31: multiset
a__U81: multiset
U31: multiset
isQid: multiset
a__U11: multiset
a__U61: multiset
nil: multiset
Usable Rules
There are no usable rules.
The dependency pairs and usable rules are stronlgy conservative!
Eliminated dependency pairs
The following dependency pairs (at least) can be eliminated according to the given precedence.
Problem 21: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| mark#(U41(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isList, a____, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, U71, i, a__isList, U72, u, U51, tt, U81, U52, a__isPal, U11, a__U31, a__U81, isQid, U31, a__U11, a__U61, nil
Strategy
Function Precedence
mark# < U41 < a__U51 = a__U52 = a____ = isList = a__isQid = isNeList = __ = a__isNePal = U61 = U42 = isNePal = a__isNeList = a__U41 = a__U22 = a__U72 = a__U42 = a__U71 = a__U21 = U21 = U22 = e = a = o = mark = isPal = U71 = i = a__isList = U72 = u = U51 = tt = U52 = U81 = a__isPal = U11 = a__U31 = a__U81 = U31 = isQid = a__U11 = a__U61 = nil
Argument Filtering
a__U51: all arguments are removed from a__U51
a__U52: all arguments are removed from a__U52
a____: all arguments are removed from a____
isList: all arguments are removed from isList
a__isQid: all arguments are removed from a__isQid
isNeList: all arguments are removed from isNeList
__: all arguments are removed from __
a__isNePal: all arguments are removed from a__isNePal
U61: collapses to 1
U42: all arguments are removed from U42
U41: 1 2
isNePal: all arguments are removed from isNePal
a__isNeList: all arguments are removed from a__isNeList
a__U41: all arguments are removed from a__U41
a__U22: all arguments are removed from a__U22
a__U72: all arguments are removed from a__U72
a__U42: all arguments are removed from a__U42
a__U71: all arguments are removed from a__U71
a__U21: all arguments are removed from a__U21
U21: all arguments are removed from U21
U22: all arguments are removed from U22
e: all arguments are removed from e
a: all arguments are removed from a
o: all arguments are removed from o
mark: all arguments are removed from mark
isPal: collapses to 1
mark#: 1
U71: collapses to 1
i: all arguments are removed from i
a__isList: collapses to 1
U72: collapses to 1
u: all arguments are removed from u
U51: 1 2
tt: all arguments are removed from tt
U52: 1
U81: all arguments are removed from U81
a__isPal: all arguments are removed from a__isPal
U11: all arguments are removed from U11
a__U31: all arguments are removed from a__U31
a__U81: all arguments are removed from a__U81
U31: all arguments are removed from U31
isQid: collapses to 1
a__U11: collapses to 1
a__U61: 1
nil: all arguments are removed from nil
Status
a__U51: multiset
a__U52: multiset
a____: multiset
isList: multiset
a__isQid: multiset
isNeList: multiset
__: multiset
a__isNePal: multiset
U42: multiset
U41: multiset
isNePal: multiset
a__isNeList: multiset
a__U41: multiset
a__U22: multiset
a__U72: multiset
a__U42: multiset
a__U71: multiset
a__U21: multiset
U21: multiset
U22: multiset
e: multiset
a: multiset
o: multiset
mark: multiset
mark#: lexicographic with permutation 1 → 1
i: multiset
u: multiset
U51: lexicographic with permutation 1 → 2 2 → 1
tt: multiset
U52: lexicographic with permutation 1 → 1
U81: multiset
a__isPal: multiset
U11: multiset
a__U31: multiset
a__U81: multiset
U31: multiset
a__U61: lexicographic with permutation 1 → 1
nil: multiset
Usable Rules
There are no usable rules.
The dependency pairs and usable rules are stronlgy conservative!
Eliminated dependency pairs
The following dependency pairs (at least) can be eliminated according to the given precedence.
| mark#(U41(X1, X2)) → mark#(X1) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| a__isPal#(V) | → | a__isNePal#(V) | | a__isNePal#(__(I, __(P, I))) | → | a__U71#(a__isQid(I), P) |
| a__U71#(tt, P) | → | a__isPal#(P) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a____, isList, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, i, U71, a__isList, U72, u, U51, tt, U52, U81, a__isPal, a__U31, U11, a__U81, a__U11, U31, isQid, a__U61, nil
Strategy
Projection
The following projection was used:
- π (a__U71#): 2
- π (a__isPal#): 1
- π (a__isNePal#): 1
Thus, the following dependency pairs are removed:
| a__isNePal#(__(I, __(P, I))) | → | a__U71#(a__isQid(I), P) |
Problem 5: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__isPal#(V) | → | a__isNePal#(V) | | a__U71#(tt, P) | → | a__isPal#(P) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isList, a____, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, U71, i, a__isList, U72, u, U51, tt, U81, U52, a__isPal, U11, a__U31, a__U81, isQid, U31, a__U11, a__U61, nil
Strategy
There are no SCCs!
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| a__isNeList#(__(V1, V2)) | → | a__isList#(V1) | | a__U21#(tt, V2) | → | a__isList#(V2) |
| a__U51#(tt, V2) | → | a__isList#(V2) | | a__isNeList#(__(V1, V2)) | → | a__isNeList#(V1) |
| a__isList#(__(V1, V2)) | → | a__isList#(V1) | | a__isList#(__(V1, V2)) | → | a__U21#(a__isList(V1), V2) |
| a__isNeList#(__(V1, V2)) | → | a__U41#(a__isList(V1), V2) | | a__U41#(tt, V2) | → | a__isNeList#(V2) |
| a__isNeList#(__(V1, V2)) | → | a__U51#(a__isNeList(V1), V2) | | a__isList#(V) | → | a__isNeList#(V) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, a____, isList, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, i, U71, a__isList, U72, u, U51, tt, U52, U81, a__isPal, a__U31, U11, a__U81, a__U11, U31, isQid, a__U61, nil
Strategy
Projection
The following projection was used:
- π (a__U51#): 2
- π (a__isList#): 1
- π (a__U41#): 2
- π (a__isNeList#): 1
- π (a__U21#): 2
Thus, the following dependency pairs are removed:
| a__isNeList#(__(V1, V2)) | → | a__isList#(V1) | | a__isNeList#(__(V1, V2)) | → | a__isNeList#(V1) |
| a__isList#(__(V1, V2)) | → | a__isList#(V1) | | a__isNeList#(__(V1, V2)) | → | a__U41#(a__isList(V1), V2) |
| a__isList#(__(V1, V2)) | → | a__U21#(a__isList(V1), V2) | | a__isNeList#(__(V1, V2)) | → | a__U51#(a__isNeList(V1), V2) |
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__U21#(tt, V2) | → | a__isList#(V2) | | a__U51#(tt, V2) | → | a__isList#(V2) |
| a__U41#(tt, V2) | → | a__isNeList#(V2) | | a__isList#(V) | → | a__isNeList#(V) |
Rewrite Rules
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a____(X, nil) | → | mark(X) |
| a____(nil, X) | → | mark(X) | | a__U11(tt) | → | tt |
| a__U21(tt, V2) | → | a__U22(a__isList(V2)) | | a__U22(tt) | → | tt |
| a__U31(tt) | → | tt | | a__U41(tt, V2) | → | a__U42(a__isNeList(V2)) |
| a__U42(tt) | → | tt | | a__U51(tt, V2) | → | a__U52(a__isList(V2)) |
| a__U52(tt) | → | tt | | a__U61(tt) | → | tt |
| a__U71(tt, P) | → | a__U72(a__isPal(P)) | | a__U72(tt) | → | tt |
| a__U81(tt) | → | tt | | a__isList(V) | → | a__U11(a__isNeList(V)) |
| a__isList(nil) | → | tt | | a__isList(__(V1, V2)) | → | a__U21(a__isList(V1), V2) |
| a__isNeList(V) | → | a__U31(a__isQid(V)) | | a__isNeList(__(V1, V2)) | → | a__U41(a__isList(V1), V2) |
| a__isNeList(__(V1, V2)) | → | a__U51(a__isNeList(V1), V2) | | a__isNePal(V) | → | a__U61(a__isQid(V)) |
| a__isNePal(__(I, __(P, I))) | → | a__U71(a__isQid(I), P) | | a__isPal(V) | → | a__U81(a__isNePal(V)) |
| a__isPal(nil) | → | tt | | a__isQid(a) | → | tt |
| a__isQid(e) | → | tt | | a__isQid(i) | → | tt |
| a__isQid(o) | → | tt | | a__isQid(u) | → | tt |
| mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) | | mark(U11(X)) | → | a__U11(mark(X)) |
| mark(U21(X1, X2)) | → | a__U21(mark(X1), X2) | | mark(U22(X)) | → | a__U22(mark(X)) |
| mark(isList(X)) | → | a__isList(X) | | mark(U31(X)) | → | a__U31(mark(X)) |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | | mark(U42(X)) | → | a__U42(mark(X)) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) |
| mark(U52(X)) | → | a__U52(mark(X)) | | mark(U61(X)) | → | a__U61(mark(X)) |
| mark(U71(X1, X2)) | → | a__U71(mark(X1), X2) | | mark(U72(X)) | → | a__U72(mark(X)) |
| mark(isPal(X)) | → | a__isPal(X) | | mark(U81(X)) | → | a__U81(mark(X)) |
| mark(isQid(X)) | → | a__isQid(X) | | mark(isNePal(X)) | → | a__isNePal(X) |
| mark(nil) | → | nil | | mark(tt) | → | tt |
| mark(a) | → | a | | mark(e) | → | e |
| mark(i) | → | i | | mark(o) | → | o |
| mark(u) | → | u | | a____(X1, X2) | → | __(X1, X2) |
| a__U11(X) | → | U11(X) | | a__U21(X1, X2) | → | U21(X1, X2) |
| a__U22(X) | → | U22(X) | | a__isList(X) | → | isList(X) |
| a__U31(X) | → | U31(X) | | a__U41(X1, X2) | → | U41(X1, X2) |
| a__U42(X) | → | U42(X) | | a__isNeList(X) | → | isNeList(X) |
| a__U51(X1, X2) | → | U51(X1, X2) | | a__U52(X) | → | U52(X) |
| a__U61(X) | → | U61(X) | | a__U71(X1, X2) | → | U71(X1, X2) |
| a__U72(X) | → | U72(X) | | a__isPal(X) | → | isPal(X) |
| a__U81(X) | → | U81(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) |
Original Signature
Termination of terms over the following signature is verified: a__U51, a__U52, isList, a____, a__isQid, isNeList, __, a__isNePal, U61, U42, U41, isNePal, a__isNeList, a__U41, a__U22, a__U72, a__U42, a__U71, U21, a__U21, U22, e, a, o, mark, isPal, U71, i, a__isList, U72, u, U51, tt, U81, U52, a__isPal, U11, a__U31, a__U81, isQid, U31, a__U11, a__U61, nil
Strategy
There are no SCCs!