YES
The TRS could be proven terminating. The proof took 42388 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (520ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (256ms).
| | – Problem 3 was processed with processor DependencyGraph (35ms).
| | | – Problem 4 was processed with processor PolynomialLinearRange4 (128ms).
| | | | – Problem 6 was processed with processor DependencyGraph (5ms).
| | | | | – Problem 7 was processed with processor PolynomialLinearRange4 (201ms).
| | | | | | – Problem 8 was processed with processor DependencyGraph (1ms).
| | | – Problem 5 was processed with processor PolynomialLinearRange4 (94ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a____#(__(X, Y), Z) | → | mark#(Y) | | mark#(isNePal(X)) | → | a__isNePal#(X) |
| mark#(__(X1, X2)) | → | a____#(mark(X1), mark(X2)) | | a____#(__(X, Y), Z) | → | a____#(mark(Y), mark(Z)) |
| a____#(nil, X) | → | mark#(X) | | a____#(__(X, Y), Z) | → | mark#(X) |
| a____#(X, nil) | → | mark#(X) | | mark#(isList(X)) | → | a__isList#(X) |
| a__isNeList#(__(V1, V2)) | → | a__isList#(V1) | | a____#(__(X, Y), Z) | → | mark#(Z) |
| a__isList#(__(V1, V2)) | → | a__and#(a__isList(V1), isList(V2)) | | a__isNeList#(__(V1, V2)) | → | a__and#(a__isNeList(V1), isList(V2)) |
| a____#(__(X, Y), Z) | → | a____#(mark(X), a____(mark(Y), mark(Z))) | | a__and#(tt, X) | → | mark#(X) |
| a__isNePal#(V) | → | a__isQid#(V) | | mark#(__(X1, X2)) | → | mark#(X2) |
| a__isList#(V) | → | a__isNeList#(V) | | a__isNeList#(V) | → | a__isQid#(V) |
| a__isPal#(V) | → | a__isNePal#(V) | | mark#(isQid(X)) | → | a__isQid#(X) |
| a__isNeList#(__(V1, V2)) | → | a__isNeList#(V1) | | a__isList#(__(V1, V2)) | → | a__isList#(V1) |
| a__isNePal#(__(I, __(P, I))) | → | a__isQid#(I) | | mark#(and(X1, X2)) | → | mark#(X1) |
| a__isNePal#(__(I, __(P, I))) | → | a__and#(a__isQid(I), isPal(P)) | | mark#(and(X1, X2)) | → | a__and#(mark(X1), X2) |
| mark#(isNeList(X)) | → | a__isNeList#(X) | | mark#(isPal(X)) | → | a__isPal#(X) |
| mark#(__(X1, X2)) | → | mark#(X1) | | a__isNeList#(__(V1, V2)) | → | a__and#(a__isList(V1), isNeList(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__and(tt, X) | → | mark(X) |
| a__isList(V) | → | a__isNeList(V) | | a__isList(nil) | → | tt |
| a__isList(__(V1, V2)) | → | a__and(a__isList(V1), isList(V2)) | | a__isNeList(V) | → | a__isQid(V) |
| a__isNeList(__(V1, V2)) | → | a__and(a__isList(V1), isNeList(V2)) | | a__isNeList(__(V1, V2)) | → | a__and(a__isNeList(V1), isList(V2)) |
| a__isNePal(V) | → | a__isQid(V) | | a__isNePal(__(I, __(P, I))) | → | a__and(a__isQid(I), isPal(P)) |
| a__isPal(V) | → | 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(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(isList(X)) | → | a__isList(X) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(isQid(X)) | → | a__isQid(X) |
| mark(isNePal(X)) | → | a__isNePal(X) | | mark(isPal(X)) | → | a__isPal(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__and(X1, X2) | → | and(X1, X2) | | a__isList(X) | → | isList(X) |
| a__isNeList(X) | → | isNeList(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) | | a__isPal(X) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: a____, isList, e, a__isQid, a, isNeList, o, __, mark, a__isNePal, isPal, a__and, and, i, a__isList, u, tt, isNePal, a__isNeList, a__isPal, isQid, nil
Strategy
The following SCCs where found
| a____#(__(X, Y), Z) → mark#(Y) | mark#(isNePal(X)) → a__isNePal#(X) |
| a____#(__(X, Y), Z) → a____#(mark(Y), mark(Z)) | mark#(__(X1, X2)) → a____#(mark(X1), mark(X2)) |
| a____#(nil, X) → mark#(X) | a____#(__(X, Y), Z) → mark#(X) |
| a____#(X, nil) → mark#(X) | mark#(isList(X)) → a__isList#(X) |
| a__isList#(__(V1, V2)) → a__and#(a__isList(V1), isList(V2)) | a__isNeList#(__(V1, V2)) → a__isList#(V1) |
| a____#(__(X, Y), Z) → mark#(Z) | a__isNeList#(__(V1, V2)) → a__and#(a__isNeList(V1), isList(V2)) |
| a____#(__(X, Y), Z) → a____#(mark(X), a____(mark(Y), mark(Z))) | a__and#(tt, X) → mark#(X) |
| mark#(__(X1, X2)) → mark#(X2) | a__isList#(V) → a__isNeList#(V) |
| a__isPal#(V) → a__isNePal#(V) | a__isNeList#(__(V1, V2)) → a__isNeList#(V1) |
| a__isList#(__(V1, V2)) → a__isList#(V1) | mark#(and(X1, X2)) → mark#(X1) |
| a__isNePal#(__(I, __(P, I))) → a__and#(a__isQid(I), isPal(P)) | mark#(and(X1, X2)) → a__and#(mark(X1), X2) |
| mark#(isNeList(X)) → a__isNeList#(X) | mark#(isPal(X)) → a__isPal#(X) |
| mark#(__(X1, X2)) → mark#(X1) | a__isNeList#(__(V1, V2)) → a__and#(a__isList(V1), isNeList(V2)) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| a____#(__(X, Y), Z) | → | mark#(Y) | | mark#(isNePal(X)) | → | a__isNePal#(X) |
| a____#(__(X, Y), Z) | → | a____#(mark(Y), mark(Z)) | | mark#(__(X1, X2)) | → | a____#(mark(X1), mark(X2)) |
| a____#(nil, X) | → | mark#(X) | | a____#(__(X, Y), Z) | → | mark#(X) |
| a____#(X, nil) | → | mark#(X) | | mark#(isList(X)) | → | a__isList#(X) |
| a__isList#(__(V1, V2)) | → | a__and#(a__isList(V1), isList(V2)) | | a__isNeList#(__(V1, V2)) | → | a__isList#(V1) |
| a____#(__(X, Y), Z) | → | mark#(Z) | | a__isNeList#(__(V1, V2)) | → | a__and#(a__isNeList(V1), isList(V2)) |
| a____#(__(X, Y), Z) | → | a____#(mark(X), a____(mark(Y), mark(Z))) | | a__and#(tt, X) | → | mark#(X) |
| mark#(__(X1, X2)) | → | mark#(X2) | | a__isList#(V) | → | a__isNeList#(V) |
| a__isPal#(V) | → | a__isNePal#(V) | | a__isNeList#(__(V1, V2)) | → | a__isNeList#(V1) |
| a__isList#(__(V1, V2)) | → | a__isList#(V1) | | mark#(and(X1, X2)) | → | mark#(X1) |
| a__isNePal#(__(I, __(P, I))) | → | a__and#(a__isQid(I), isPal(P)) | | mark#(and(X1, X2)) | → | a__and#(mark(X1), X2) |
| mark#(isNeList(X)) | → | a__isNeList#(X) | | mark#(isPal(X)) | → | a__isPal#(X) |
| mark#(__(X1, X2)) | → | mark#(X1) | | a__isNeList#(__(V1, V2)) | → | a__and#(a__isList(V1), isNeList(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__and(tt, X) | → | mark(X) |
| a__isList(V) | → | a__isNeList(V) | | a__isList(nil) | → | tt |
| a__isList(__(V1, V2)) | → | a__and(a__isList(V1), isList(V2)) | | a__isNeList(V) | → | a__isQid(V) |
| a__isNeList(__(V1, V2)) | → | a__and(a__isList(V1), isNeList(V2)) | | a__isNeList(__(V1, V2)) | → | a__and(a__isNeList(V1), isList(V2)) |
| a__isNePal(V) | → | a__isQid(V) | | a__isNePal(__(I, __(P, I))) | → | a__and(a__isQid(I), isPal(P)) |
| a__isPal(V) | → | 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(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(isList(X)) | → | a__isList(X) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(isQid(X)) | → | a__isQid(X) |
| mark(isNePal(X)) | → | a__isNePal(X) | | mark(isPal(X)) | → | a__isPal(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__and(X1, X2) | → | and(X1, X2) | | a__isList(X) | → | isList(X) |
| a__isNeList(X) | → | isNeList(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) | | a__isPal(X) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: a____, isList, e, a__isQid, a, isNeList, o, __, mark, a__isNePal, isPal, a__and, and, i, a__isList, u, tt, isNePal, a__isNeList, a__isPal, isQid, nil
Strategy
Polynomial Interpretation
- __(x,y): y + x + 1
- a: 3
- a____(x,y): y + x + 1
- a____#(x,y): 2y + 2x
- a__and(x,y): y + x
- a__and#(x,y): 2y
- a__isList(x): x + 1
- a__isList#(x): 2x
- a__isNeList(x): x + 1
- a__isNeList#(x): 2x
- a__isNePal(x): 1
- a__isNePal#(x): 2
- a__isPal(x): 1
- a__isPal#(x): 2
- a__isQid(x): 0
- and(x,y): y + x
- e: 1
- i: 2
- isList(x): x + 1
- isNeList(x): x + 1
- isNePal(x): 1
- isPal(x): 1
- isQid(x): 0
- mark(x): x
- mark#(x): 2x
- nil: 0
- o: 1
- tt: 0
- u: 2
Standard Usable rules
| a__isList(X) | → | isList(X) | | a__isPal(nil) | → | tt |
| mark(isQid(X)) | → | a__isQid(X) | | mark(a) | → | a |
| a__isNePal(__(I, __(P, I))) | → | a__and(a__isQid(I), isPal(P)) | | mark(isNePal(X)) | → | a__isNePal(X) |
| a__isNePal(X) | → | isNePal(X) | | a____(nil, X) | → | mark(X) |
| mark(i) | → | i | | mark(o) | → | o |
| mark(nil) | → | nil | | a__isQid(e) | → | tt |
| a__isQid(i) | → | tt | | a__isQid(a) | → | tt |
| a__isNeList(V) | → | a__isQid(V) | | mark(isList(X)) | → | a__isList(X) |
| mark(u) | → | u | | mark(tt) | → | tt |
| a__and(X1, X2) | → | and(X1, X2) | | mark(isPal(X)) | → | a__isPal(X) |
| a__isPal(X) | → | isPal(X) | | a__and(tt, X) | → | mark(X) |
| mark(e) | → | e | | a____(X, nil) | → | mark(X) |
| a____(X1, X2) | → | __(X1, X2) | | a__isNeList(X) | → | isNeList(X) |
| a__isNeList(__(V1, V2)) | → | a__and(a__isList(V1), isNeList(V2)) | | a__isList(V) | → | a__isNeList(V) |
| a__isNePal(V) | → | a__isQid(V) | | a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) |
| a__isQid(u) | → | tt | | a__isPal(V) | → | a__isNePal(V) |
| a__isList(nil) | → | tt | | a__isQid(X) | → | isQid(X) |
| mark(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) |
| a__isList(__(V1, V2)) | → | a__and(a__isList(V1), isList(V2)) | | a__isQid(o) | → | tt |
| a__isNeList(__(V1, V2)) | → | a__and(a__isNeList(V1), isList(V2)) | | 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) | | mark#(__(X1, X2)) | → | a____#(mark(X1), mark(X2)) |
| a____#(__(X, Y), Z) | → | a____#(mark(Y), mark(Z)) | | a____#(__(X, Y), Z) | → | mark#(X) |
| mark#(isList(X)) | → | a__isList#(X) | | a____#(__(X, Y), Z) | → | mark#(Z) |
| a__isNeList#(__(V1, V2)) | → | a__isList#(V1) | | mark#(__(X1, X2)) | → | mark#(X2) |
| a__isNeList#(__(V1, V2)) | → | a__isNeList#(V1) | | a__isList#(__(V1, V2)) | → | a__isList#(V1) |
| mark#(isNeList(X)) | → | a__isNeList#(X) | | mark#(__(X1, X2)) | → | mark#(X1) |
Problem 3: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__isPal#(V) | → | a__isNePal#(V) | | mark#(isNePal(X)) | → | a__isNePal#(X) |
| a____#(nil, X) | → | mark#(X) | | a____#(X, nil) | → | mark#(X) |
| a__isList#(__(V1, V2)) | → | a__and#(a__isList(V1), isList(V2)) | | mark#(and(X1, X2)) | → | mark#(X1) |
| a__isNePal#(__(I, __(P, I))) | → | a__and#(a__isQid(I), isPal(P)) | | a__isNeList#(__(V1, V2)) | → | a__and#(a__isNeList(V1), isList(V2)) |
| a____#(__(X, Y), Z) | → | a____#(mark(X), a____(mark(Y), mark(Z))) | | mark#(and(X1, X2)) | → | a__and#(mark(X1), X2) |
| a__and#(tt, X) | → | mark#(X) | | mark#(isPal(X)) | → | a__isPal#(X) |
| a__isNeList#(__(V1, V2)) | → | a__and#(a__isList(V1), 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__and(tt, X) | → | mark(X) |
| a__isList(V) | → | a__isNeList(V) | | a__isList(nil) | → | tt |
| a__isList(__(V1, V2)) | → | a__and(a__isList(V1), isList(V2)) | | a__isNeList(V) | → | a__isQid(V) |
| a__isNeList(__(V1, V2)) | → | a__and(a__isList(V1), isNeList(V2)) | | a__isNeList(__(V1, V2)) | → | a__and(a__isNeList(V1), isList(V2)) |
| a__isNePal(V) | → | a__isQid(V) | | a__isNePal(__(I, __(P, I))) | → | a__and(a__isQid(I), isPal(P)) |
| a__isPal(V) | → | 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(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(isList(X)) | → | a__isList(X) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(isQid(X)) | → | a__isQid(X) |
| mark(isNePal(X)) | → | a__isNePal(X) | | mark(isPal(X)) | → | a__isPal(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__and(X1, X2) | → | and(X1, X2) | | a__isList(X) | → | isList(X) |
| a__isNeList(X) | → | isNeList(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) | | a__isPal(X) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: a____, isList, e, a__isQid, a, isNeList, o, __, mark, a__isNePal, isPal, i, a__and, and, a__isList, u, tt, isNePal, a__isNeList, a__isPal, isQid, nil
Strategy
The following SCCs where found
| a____#(__(X, Y), Z) → a____#(mark(X), a____(mark(Y), mark(Z))) |
| mark#(and(X1, X2)) → mark#(X1) | a__isNePal#(__(I, __(P, I))) → a__and#(a__isQid(I), isPal(P)) |
| a__isPal#(V) → a__isNePal#(V) | mark#(isNePal(X)) → a__isNePal#(X) |
| mark#(and(X1, X2)) → a__and#(mark(X1), X2) | a__and#(tt, X) → mark#(X) |
| mark#(isPal(X)) → a__isPal#(X) |
Problem 4: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(and(X1, X2)) | → | mark#(X1) | | a__isNePal#(__(I, __(P, I))) | → | a__and#(a__isQid(I), isPal(P)) |
| a__isPal#(V) | → | a__isNePal#(V) | | mark#(isNePal(X)) | → | a__isNePal#(X) |
| mark#(and(X1, X2)) | → | a__and#(mark(X1), X2) | | a__and#(tt, X) | → | mark#(X) |
| mark#(isPal(X)) | → | a__isPal#(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__and(tt, X) | → | mark(X) |
| a__isList(V) | → | a__isNeList(V) | | a__isList(nil) | → | tt |
| a__isList(__(V1, V2)) | → | a__and(a__isList(V1), isList(V2)) | | a__isNeList(V) | → | a__isQid(V) |
| a__isNeList(__(V1, V2)) | → | a__and(a__isList(V1), isNeList(V2)) | | a__isNeList(__(V1, V2)) | → | a__and(a__isNeList(V1), isList(V2)) |
| a__isNePal(V) | → | a__isQid(V) | | a__isNePal(__(I, __(P, I))) | → | a__and(a__isQid(I), isPal(P)) |
| a__isPal(V) | → | 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(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(isList(X)) | → | a__isList(X) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(isQid(X)) | → | a__isQid(X) |
| mark(isNePal(X)) | → | a__isNePal(X) | | mark(isPal(X)) | → | a__isPal(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__and(X1, X2) | → | and(X1, X2) | | a__isList(X) | → | isList(X) |
| a__isNeList(X) | → | isNeList(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) | | a__isPal(X) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: a____, isList, e, a__isQid, a, isNeList, o, __, mark, a__isNePal, isPal, i, a__and, and, a__isList, u, tt, isNePal, a__isNeList, a__isPal, isQid, nil
Strategy
Polynomial Interpretation
- __(x,y): y + 2x + 1
- a: 0
- a____(x,y): y + 2x + 1
- a__and(x,y): y + 2x
- a__and#(x,y): 2y
- a__isList(x): 2x + 1
- a__isNeList(x): 2x
- a__isNePal(x): x
- a__isNePal#(x): x
- a__isPal(x): x + 1
- a__isPal#(x): 2x + 2
- a__isQid(x): x
- and(x,y): y + 2x
- e: 2
- i: 0
- isList(x): 2x + 1
- isNeList(x): 2x
- isNePal(x): x
- isPal(x): x + 1
- isQid(x): x
- mark(x): x
- mark#(x): 2x
- nil: 0
- o: 0
- tt: 0
- u: 0
Standard Usable rules
| a__isList(X) | → | isList(X) | | mark(isQid(X)) | → | a__isQid(X) |
| a__isPal(nil) | → | tt | | mark(a) | → | a |
| a__isNePal(__(I, __(P, I))) | → | a__and(a__isQid(I), isPal(P)) | | mark(isNePal(X)) | → | a__isNePal(X) |
| a__isNePal(X) | → | isNePal(X) | | a____(nil, X) | → | mark(X) |
| mark(i) | → | i | | mark(nil) | → | nil |
| mark(o) | → | o | | a__isQid(e) | → | tt |
| a__isQid(i) | → | tt | | a__isNeList(V) | → | a__isQid(V) |
| a__isQid(a) | → | tt | | mark(isList(X)) | → | a__isList(X) |
| mark(tt) | → | tt | | mark(u) | → | u |
| mark(isPal(X)) | → | a__isPal(X) | | a__and(X1, X2) | → | and(X1, X2) |
| a__isPal(X) | → | isPal(X) | | a__and(tt, X) | → | mark(X) |
| mark(e) | → | e | | a____(X, nil) | → | mark(X) |
| a____(X1, X2) | → | __(X1, X2) | | a__isNeList(__(V1, V2)) | → | a__and(a__isList(V1), isNeList(V2)) |
| a__isList(V) | → | a__isNeList(V) | | a__isNeList(X) | → | isNeList(X) |
| a__isNePal(V) | → | a__isQid(V) | | a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) |
| a__isQid(u) | → | tt | | a__isPal(V) | → | a__isNePal(V) |
| a__isList(nil) | → | tt | | a__isQid(X) | → | isQid(X) |
| mark(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) |
| a__isList(__(V1, V2)) | → | a__and(a__isList(V1), isList(V2)) | | a__isQid(o) | → | tt |
| a__isNeList(__(V1, V2)) | → | a__and(a__isNeList(V1), isList(V2)) | | 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__isPal#(V) | → | a__isNePal#(V) |
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(and(X1, X2)) | → | mark#(X1) | | a__isNePal#(__(I, __(P, I))) | → | a__and#(a__isQid(I), isPal(P)) |
| mark#(isNePal(X)) | → | a__isNePal#(X) | | mark#(and(X1, X2)) | → | a__and#(mark(X1), X2) |
| a__and#(tt, X) | → | mark#(X) | | mark#(isPal(X)) | → | a__isPal#(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__and(tt, X) | → | mark(X) |
| a__isList(V) | → | a__isNeList(V) | | a__isList(nil) | → | tt |
| a__isList(__(V1, V2)) | → | a__and(a__isList(V1), isList(V2)) | | a__isNeList(V) | → | a__isQid(V) |
| a__isNeList(__(V1, V2)) | → | a__and(a__isList(V1), isNeList(V2)) | | a__isNeList(__(V1, V2)) | → | a__and(a__isNeList(V1), isList(V2)) |
| a__isNePal(V) | → | a__isQid(V) | | a__isNePal(__(I, __(P, I))) | → | a__and(a__isQid(I), isPal(P)) |
| a__isPal(V) | → | 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(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(isList(X)) | → | a__isList(X) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(isQid(X)) | → | a__isQid(X) |
| mark(isNePal(X)) | → | a__isNePal(X) | | mark(isPal(X)) | → | a__isPal(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__and(X1, X2) | → | and(X1, X2) | | a__isList(X) | → | isList(X) |
| a__isNeList(X) | → | isNeList(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) | | a__isPal(X) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: a____, isList, e, a__isQid, a, isNeList, o, __, mark, a__isNePal, isPal, and, i, a__and, a__isList, u, tt, isNePal, a__isNeList, a__isPal, isQid, nil
Strategy
The following SCCs where found
| mark#(and(X1, X2)) → mark#(X1) | a__isNePal#(__(I, __(P, I))) → a__and#(a__isQid(I), isPal(P)) |
| mark#(isNePal(X)) → a__isNePal#(X) | mark#(and(X1, X2)) → a__and#(mark(X1), X2) |
| a__and#(tt, X) → mark#(X) |
Problem 7: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(and(X1, X2)) | → | mark#(X1) | | a__isNePal#(__(I, __(P, I))) | → | a__and#(a__isQid(I), isPal(P)) |
| mark#(isNePal(X)) | → | a__isNePal#(X) | | mark#(and(X1, X2)) | → | a__and#(mark(X1), X2) |
| a__and#(tt, 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__and(tt, X) | → | mark(X) |
| a__isList(V) | → | a__isNeList(V) | | a__isList(nil) | → | tt |
| a__isList(__(V1, V2)) | → | a__and(a__isList(V1), isList(V2)) | | a__isNeList(V) | → | a__isQid(V) |
| a__isNeList(__(V1, V2)) | → | a__and(a__isList(V1), isNeList(V2)) | | a__isNeList(__(V1, V2)) | → | a__and(a__isNeList(V1), isList(V2)) |
| a__isNePal(V) | → | a__isQid(V) | | a__isNePal(__(I, __(P, I))) | → | a__and(a__isQid(I), isPal(P)) |
| a__isPal(V) | → | 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(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(isList(X)) | → | a__isList(X) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(isQid(X)) | → | a__isQid(X) |
| mark(isNePal(X)) | → | a__isNePal(X) | | mark(isPal(X)) | → | a__isPal(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__and(X1, X2) | → | and(X1, X2) | | a__isList(X) | → | isList(X) |
| a__isNeList(X) | → | isNeList(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) | | a__isPal(X) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: a____, isList, e, a__isQid, a, isNeList, o, __, mark, a__isNePal, isPal, and, i, a__and, a__isList, u, tt, isNePal, a__isNeList, a__isPal, isQid, nil
Strategy
Polynomial Interpretation
- __(x,y): y + 2x + 1
- a: 2
- a____(x,y): y + 2x + 1
- a__and(x,y): y + x + 1
- a__and#(x,y): 2y
- a__isList(x): 2x
- a__isNeList(x): 2x
- a__isNePal(x): x + 1
- a__isNePal#(x): x
- a__isPal(x): x + 1
- a__isQid(x): x
- and(x,y): y + x + 1
- e: 2
- i: 3
- isList(x): 2x
- isNeList(x): 2x
- isNePal(x): x + 1
- isPal(x): x + 1
- isQid(x): x
- mark(x): x
- mark#(x): 2x
- nil: 1
- o: 3
- tt: 2
- u: 2
Standard Usable rules
| a__isList(X) | → | isList(X) | | mark(isQid(X)) | → | a__isQid(X) |
| a__isPal(nil) | → | tt | | mark(a) | → | a |
| a__isNePal(__(I, __(P, I))) | → | a__and(a__isQid(I), isPal(P)) | | mark(isNePal(X)) | → | a__isNePal(X) |
| a__isNePal(X) | → | isNePal(X) | | a____(nil, X) | → | mark(X) |
| mark(i) | → | i | | mark(nil) | → | nil |
| mark(o) | → | o | | a__isQid(e) | → | tt |
| a__isQid(i) | → | tt | | a__isNeList(V) | → | a__isQid(V) |
| a__isQid(a) | → | tt | | mark(isList(X)) | → | a__isList(X) |
| mark(tt) | → | tt | | mark(u) | → | u |
| mark(isPal(X)) | → | a__isPal(X) | | a__and(X1, X2) | → | and(X1, X2) |
| a__isPal(X) | → | isPal(X) | | a__and(tt, X) | → | mark(X) |
| mark(e) | → | e | | a____(X, nil) | → | mark(X) |
| a____(X1, X2) | → | __(X1, X2) | | a__isNeList(__(V1, V2)) | → | a__and(a__isList(V1), isNeList(V2)) |
| a__isList(V) | → | a__isNeList(V) | | a__isNeList(X) | → | isNeList(X) |
| a__isNePal(V) | → | a__isQid(V) | | a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) |
| a__isQid(u) | → | tt | | a__isPal(V) | → | a__isNePal(V) |
| a__isList(nil) | → | tt | | a__isQid(X) | → | isQid(X) |
| mark(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) |
| a__isList(__(V1, V2)) | → | a__and(a__isList(V1), isList(V2)) | | a__isQid(o) | → | tt |
| a__isNeList(__(V1, V2)) | → | a__and(a__isNeList(V1), isList(V2)) | | 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#(and(X1, X2)) | → | mark#(X1) | | mark#(isNePal(X)) | → | a__isNePal#(X) |
| mark#(and(X1, X2)) | → | a__and#(mark(X1), X2) |
Problem 8: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__isNePal#(__(I, __(P, I))) | → | a__and#(a__isQid(I), isPal(P)) | | a__and#(tt, 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__and(tt, X) | → | mark(X) |
| a__isList(V) | → | a__isNeList(V) | | a__isList(nil) | → | tt |
| a__isList(__(V1, V2)) | → | a__and(a__isList(V1), isList(V2)) | | a__isNeList(V) | → | a__isQid(V) |
| a__isNeList(__(V1, V2)) | → | a__and(a__isList(V1), isNeList(V2)) | | a__isNeList(__(V1, V2)) | → | a__and(a__isNeList(V1), isList(V2)) |
| a__isNePal(V) | → | a__isQid(V) | | a__isNePal(__(I, __(P, I))) | → | a__and(a__isQid(I), isPal(P)) |
| a__isPal(V) | → | 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(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(isList(X)) | → | a__isList(X) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(isQid(X)) | → | a__isQid(X) |
| mark(isNePal(X)) | → | a__isNePal(X) | | mark(isPal(X)) | → | a__isPal(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__and(X1, X2) | → | and(X1, X2) | | a__isList(X) | → | isList(X) |
| a__isNeList(X) | → | isNeList(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) | | a__isPal(X) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: a____, isList, e, a__isQid, a, isNeList, o, __, mark, a__isNePal, isPal, a__and, and, i, a__isList, u, tt, isNePal, a__isNeList, a__isPal, isQid, nil
Strategy
There are no SCCs!
Problem 5: 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__and(tt, X) | → | mark(X) |
| a__isList(V) | → | a__isNeList(V) | | a__isList(nil) | → | tt |
| a__isList(__(V1, V2)) | → | a__and(a__isList(V1), isList(V2)) | | a__isNeList(V) | → | a__isQid(V) |
| a__isNeList(__(V1, V2)) | → | a__and(a__isList(V1), isNeList(V2)) | | a__isNeList(__(V1, V2)) | → | a__and(a__isNeList(V1), isList(V2)) |
| a__isNePal(V) | → | a__isQid(V) | | a__isNePal(__(I, __(P, I))) | → | a__and(a__isQid(I), isPal(P)) |
| a__isPal(V) | → | 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(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(isList(X)) | → | a__isList(X) |
| mark(isNeList(X)) | → | a__isNeList(X) | | mark(isQid(X)) | → | a__isQid(X) |
| mark(isNePal(X)) | → | a__isNePal(X) | | mark(isPal(X)) | → | a__isPal(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__and(X1, X2) | → | and(X1, X2) | | a__isList(X) | → | isList(X) |
| a__isNeList(X) | → | isNeList(X) | | a__isQid(X) | → | isQid(X) |
| a__isNePal(X) | → | isNePal(X) | | a__isPal(X) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: a____, isList, e, a__isQid, a, isNeList, o, __, mark, a__isNePal, isPal, i, a__and, and, a__isList, u, tt, isNePal, a__isNeList, a__isPal, isQid, nil
Strategy
Polynomial Interpretation
- __(x,y): y + 2x + 1
- a: 2
- a____(x,y): y + 2x + 1
- a____#(x,y): y + 2x
- a__and(x,y): y
- a__isList(x): x
- a__isNeList(x): x
- a__isNePal(x): x
- a__isPal(x): x + 2
- a__isQid(x): x
- and(x,y): y
- e: 1
- i: 2
- isList(x): x
- isNeList(x): x
- isNePal(x): x
- isPal(x): x + 2
- isQid(x): x
- mark(x): x
- nil: 0
- o: 2
- tt: 0
- u: 0
Standard Usable rules
| a__isList(X) | → | isList(X) | | mark(isQid(X)) | → | a__isQid(X) |
| a__isPal(nil) | → | tt | | mark(a) | → | a |
| a__isNePal(__(I, __(P, I))) | → | a__and(a__isQid(I), isPal(P)) | | mark(isNePal(X)) | → | a__isNePal(X) |
| a__isNePal(X) | → | isNePal(X) | | a____(nil, X) | → | mark(X) |
| mark(i) | → | i | | mark(nil) | → | nil |
| mark(o) | → | o | | a__isQid(e) | → | tt |
| a__isQid(i) | → | tt | | a__isQid(a) | → | tt |
| a__isNeList(V) | → | a__isQid(V) | | mark(isList(X)) | → | a__isList(X) |
| mark(tt) | → | tt | | mark(u) | → | u |
| mark(isPal(X)) | → | a__isPal(X) | | a__and(X1, X2) | → | and(X1, X2) |
| a__isPal(X) | → | isPal(X) | | mark(e) | → | e |
| a__and(tt, X) | → | mark(X) | | a____(X, nil) | → | mark(X) |
| a____(X1, X2) | → | __(X1, X2) | | a__isNeList(__(V1, V2)) | → | a__and(a__isList(V1), isNeList(V2)) |
| a__isList(V) | → | a__isNeList(V) | | a__isNeList(X) | → | isNeList(X) |
| a__isNePal(V) | → | a__isQid(V) | | a__isQid(u) | → | tt |
| a____(__(X, Y), Z) | → | a____(mark(X), a____(mark(Y), mark(Z))) | | a__isPal(V) | → | a__isNePal(V) |
| a__isList(nil) | → | tt | | a__isQid(X) | → | isQid(X) |
| mark(and(X1, X2)) | → | a__and(mark(X1), X2) | | mark(__(X1, X2)) | → | a____(mark(X1), mark(X2)) |
| a__isList(__(V1, V2)) | → | a__and(a__isList(V1), isList(V2)) | | a__isQid(o) | → | tt |
| a__isNeList(__(V1, V2)) | → | a__and(a__isNeList(V1), isList(V2)) | | 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))) |