TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60056 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (5711ms).
| – Problem 2 was processed with processor ReductionPairSAT (15507ms).
| | – Problem 12 was processed with processor ReductionPairSAT (15301ms).
| | | – Problem 15 remains open; application of the following processors failed [DependencyGraph (589ms), ReductionPairSAT (timeout)].
| – Problem 3 was processed with processor SubtermCriterion (3ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| – Problem 5 was processed with processor SubtermCriterion (1ms).
| | – Problem 10 was processed with processor ReductionPairSAT (67ms).
| | | – Problem 13 was processed with processor ReductionPairSAT (63ms).
| – Problem 6 was processed with processor SubtermCriterion (1ms).
| – Problem 7 was processed with processor SubtermCriterion (1ms).
| – Problem 8 was processed with processor SubtermCriterion (1ms).
| | – Problem 11 was processed with processor ReductionPairSAT (90ms).
| | | – Problem 14 was processed with processor ReductionPairSAT (65ms).
| – Problem 9 was processed with processor SubtermCriterion (3ms).
The following open problems remain:
Open Dependency Pair Problem 15
Dependency Pairs
| active#(isList(V)) | → | mark#(isNeList(V)) | | active#(isQid(a)) | → | mark#(tt) |
| active#(__(__(X, Y), Z)) | → | mark#(__(X, __(Y, Z))) | | active#(__(X, nil)) | → | mark#(X) |
| active#(isNePal(V)) | → | mark#(isQid(V)) | | mark#(isNePal(X)) | → | active#(isNePal(X)) |
| active#(isNeList(__(V1, V2))) | → | mark#(and(isList(V1), isNeList(V2))) | | active#(isList(nil)) | → | mark#(tt) |
| active#(isNeList(V)) | → | mark#(isQid(V)) | | active#(isQid(i)) | → | mark#(tt) |
| mark#(and(X1, X2)) | → | active#(and(mark(X1), X2)) | | mark#(__(X1, X2)) | → | mark#(X2) |
| active#(isQid(o)) | → | mark#(tt) | | active#(isQid(e)) | → | mark#(tt) |
| active#(isNeList(__(V1, V2))) | → | mark#(and(isNeList(V1), isList(V2))) | | active#(__(nil, X)) | → | mark#(X) |
| active#(isPal(V)) | → | mark#(isNePal(V)) | | mark#(isPal(X)) | → | active#(isPal(X)) |
| active#(isList(__(V1, V2))) | → | mark#(and(isList(V1), isList(V2))) | | mark#(__(X1, X2)) | → | active#(__(mark(X1), mark(X2))) |
| active#(isNePal(__(I, __(P, I)))) | → | mark#(and(isQid(I), isPal(P))) | | active#(and(tt, X)) | → | mark#(X) |
| active#(isQid(u)) | → | mark#(tt) | | mark#(isQid(X)) | → | active#(isQid(X)) |
| mark#(isList(X)) | → | active#(isList(X)) | | mark#(and(X1, X2)) | → | mark#(X1) |
| mark#(isNeList(X)) | → | active#(isNeList(X)) | | active#(isPal(nil)) | → | mark#(tt) |
| mark#(__(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(and(tt, X)) | → | mark(X) |
| active(isList(V)) | → | mark(isNeList(V)) | | active(isList(nil)) | → | mark(tt) |
| active(isList(__(V1, V2))) | → | mark(and(isList(V1), isList(V2))) | | active(isNeList(V)) | → | mark(isQid(V)) |
| active(isNeList(__(V1, V2))) | → | mark(and(isList(V1), isNeList(V2))) | | active(isNeList(__(V1, V2))) | → | mark(and(isNeList(V1), isList(V2))) |
| active(isNePal(V)) | → | mark(isQid(V)) | | active(isNePal(__(I, __(P, I)))) | → | mark(and(isQid(I), isPal(P))) |
| active(isPal(V)) | → | mark(isNePal(V)) | | active(isPal(nil)) | → | mark(tt) |
| active(isQid(a)) | → | mark(tt) | | active(isQid(e)) | → | mark(tt) |
| active(isQid(i)) | → | mark(tt) | | active(isQid(o)) | → | mark(tt) |
| active(isQid(u)) | → | mark(tt) | | mark(__(X1, X2)) | → | active(__(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(tt) | → | active(tt) | | mark(isList(X)) | → | active(isList(X)) |
| mark(isNeList(X)) | → | active(isNeList(X)) | | mark(isQid(X)) | → | active(isQid(X)) |
| mark(isNePal(X)) | → | active(isNePal(X)) | | mark(isPal(X)) | → | active(isPal(X)) |
| mark(a) | → | active(a) | | mark(e) | → | active(e) |
| mark(i) | → | active(i) | | mark(o) | → | active(o) |
| mark(u) | → | active(u) | | __(mark(X1), X2) | → | __(X1, X2) |
| __(X1, mark(X2)) | → | __(X1, X2) | | __(active(X1), X2) | → | __(X1, X2) |
| __(X1, active(X2)) | → | __(X1, X2) | | and(mark(X1), X2) | → | and(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | and(active(X1), X2) | → | and(X1, X2) |
| and(X1, active(X2)) | → | and(X1, X2) | | isList(mark(X)) | → | isList(X) |
| isList(active(X)) | → | isList(X) | | isNeList(mark(X)) | → | isNeList(X) |
| isNeList(active(X)) | → | isNeList(X) | | isQid(mark(X)) | → | isQid(X) |
| isQid(active(X)) | → | isQid(X) | | isNePal(mark(X)) | → | isNePal(X) |
| isNePal(active(X)) | → | isNePal(X) | | isPal(mark(X)) | → | isPal(X) |
| isPal(active(X)) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, isQid, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(__(X1, X2)) | → | __#(mark(X1), mark(X2)) | | active#(isQid(a)) | → | mark#(tt) |
| active#(__(__(X, Y), Z)) | → | mark#(__(X, __(Y, Z))) | | active#(isList(__(V1, V2))) | → | isList#(V1) |
| active#(__(__(X, Y), Z)) | → | __#(X, __(Y, Z)) | | active#(__(X, nil)) | → | mark#(X) |
| mark#(a) | → | active#(a) | | isList#(active(X)) | → | isList#(X) |
| active#(isNePal(V)) | → | mark#(isQid(V)) | | mark#(e) | → | active#(e) |
| __#(X1, active(X2)) | → | __#(X1, X2) | | active#(isNeList(__(V1, V2))) | → | mark#(and(isList(V1), isNeList(V2))) |
| __#(active(X1), X2) | → | __#(X1, X2) | | active#(isNeList(V)) | → | mark#(isQid(V)) |
| mark#(i) | → | active#(i) | | isNeList#(active(X)) | → | isNeList#(X) |
| active#(isQid(i)) | → | mark#(tt) | | mark#(__(X1, X2)) | → | mark#(X2) |
| isPal#(active(X)) | → | isPal#(X) | | active#(isQid(e)) | → | mark#(tt) |
| __#(mark(X1), X2) | → | __#(X1, X2) | | active#(isNePal(V)) | → | isQid#(V) |
| mark#(and(X1, X2)) | → | and#(mark(X1), X2) | | active#(isPal(V)) | → | mark#(isNePal(V)) |
| mark#(isPal(X)) | → | active#(isPal(X)) | | active#(isNePal(__(I, __(P, I)))) | → | and#(isQid(I), isPal(P)) |
| active#(isList(__(V1, V2))) | → | mark#(and(isList(V1), isList(V2))) | | active#(isNeList(__(V1, V2))) | → | isNeList#(V2) |
| active#(isNePal(__(I, __(P, I)))) | → | mark#(and(isQid(I), isPal(P))) | | mark#(__(X1, X2)) | → | active#(__(mark(X1), mark(X2))) |
| and#(mark(X1), X2) | → | and#(X1, X2) | | mark#(isQid(X)) | → | active#(isQid(X)) |
| mark#(and(X1, X2)) | → | mark#(X1) | | mark#(isNeList(X)) | → | active#(isNeList(X)) |
| active#(isPal(nil)) | → | mark#(tt) | | mark#(__(X1, X2)) | → | mark#(X1) |
| isNeList#(mark(X)) | → | isNeList#(X) | | mark#(isNeList(X)) | → | isNeList#(X) |
| and#(active(X1), X2) | → | and#(X1, X2) | | active#(isList(V)) | → | mark#(isNeList(V)) |
| active#(isNeList(__(V1, V2))) | → | isNeList#(V1) | | and#(X1, active(X2)) | → | and#(X1, X2) |
| isPal#(mark(X)) | → | isPal#(X) | | mark#(isPal(X)) | → | isPal#(X) |
| mark#(tt) | → | active#(tt) | | mark#(o) | → | active#(o) |
| active#(isNeList(__(V1, V2))) | → | isList#(V1) | | mark#(isNePal(X)) | → | active#(isNePal(X)) |
| mark#(isList(X)) | → | isList#(X) | | isList#(mark(X)) | → | isList#(X) |
| mark#(u) | → | active#(u) | | active#(isList(nil)) | → | mark#(tt) |
| active#(isNeList(V)) | → | isQid#(V) | | mark#(nil) | → | active#(nil) |
| active#(isPal(V)) | → | isNePal#(V) | | mark#(and(X1, X2)) | → | active#(and(mark(X1), X2)) |
| active#(isNePal(__(I, __(P, I)))) | → | isPal#(P) | | isQid#(active(X)) | → | isQid#(X) |
| active#(isQid(o)) | → | mark#(tt) | | and#(X1, mark(X2)) | → | and#(X1, X2) |
| isNePal#(active(X)) | → | isNePal#(X) | | active#(isNeList(__(V1, V2))) | → | mark#(and(isNeList(V1), isList(V2))) |
| active#(isNeList(__(V1, V2))) | → | isList#(V2) | | active#(__(nil, X)) | → | mark#(X) |
| active#(isList(__(V1, V2))) | → | and#(isList(V1), isList(V2)) | | active#(isList(V)) | → | isNeList#(V) |
| active#(__(__(X, Y), Z)) | → | __#(Y, Z) | | __#(X1, mark(X2)) | → | __#(X1, X2) |
| active#(isNePal(__(I, __(P, I)))) | → | isQid#(I) | | mark#(isNePal(X)) | → | isNePal#(X) |
| isNePal#(mark(X)) | → | isNePal#(X) | | active#(and(tt, X)) | → | mark#(X) |
| mark#(isQid(X)) | → | isQid#(X) | | isQid#(mark(X)) | → | isQid#(X) |
| active#(isQid(u)) | → | mark#(tt) | | active#(isNeList(__(V1, V2))) | → | and#(isList(V1), isNeList(V2)) |
| mark#(isList(X)) | → | active#(isList(X)) | | active#(isNeList(__(V1, V2))) | → | and#(isNeList(V1), isList(V2)) |
| active#(isList(__(V1, V2))) | → | isList#(V2) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(and(tt, X)) | → | mark(X) |
| active(isList(V)) | → | mark(isNeList(V)) | | active(isList(nil)) | → | mark(tt) |
| active(isList(__(V1, V2))) | → | mark(and(isList(V1), isList(V2))) | | active(isNeList(V)) | → | mark(isQid(V)) |
| active(isNeList(__(V1, V2))) | → | mark(and(isList(V1), isNeList(V2))) | | active(isNeList(__(V1, V2))) | → | mark(and(isNeList(V1), isList(V2))) |
| active(isNePal(V)) | → | mark(isQid(V)) | | active(isNePal(__(I, __(P, I)))) | → | mark(and(isQid(I), isPal(P))) |
| active(isPal(V)) | → | mark(isNePal(V)) | | active(isPal(nil)) | → | mark(tt) |
| active(isQid(a)) | → | mark(tt) | | active(isQid(e)) | → | mark(tt) |
| active(isQid(i)) | → | mark(tt) | | active(isQid(o)) | → | mark(tt) |
| active(isQid(u)) | → | mark(tt) | | mark(__(X1, X2)) | → | active(__(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(tt) | → | active(tt) | | mark(isList(X)) | → | active(isList(X)) |
| mark(isNeList(X)) | → | active(isNeList(X)) | | mark(isQid(X)) | → | active(isQid(X)) |
| mark(isNePal(X)) | → | active(isNePal(X)) | | mark(isPal(X)) | → | active(isPal(X)) |
| mark(a) | → | active(a) | | mark(e) | → | active(e) |
| mark(i) | → | active(i) | | mark(o) | → | active(o) |
| mark(u) | → | active(u) | | __(mark(X1), X2) | → | __(X1, X2) |
| __(X1, mark(X2)) | → | __(X1, X2) | | __(active(X1), X2) | → | __(X1, X2) |
| __(X1, active(X2)) | → | __(X1, X2) | | and(mark(X1), X2) | → | and(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | and(active(X1), X2) | → | and(X1, X2) |
| and(X1, active(X2)) | → | and(X1, X2) | | isList(mark(X)) | → | isList(X) |
| isList(active(X)) | → | isList(X) | | isNeList(mark(X)) | → | isNeList(X) |
| isNeList(active(X)) | → | isNeList(X) | | isQid(mark(X)) | → | isQid(X) |
| isQid(active(X)) | → | isQid(X) | | isNePal(mark(X)) | → | isNePal(X) |
| isNePal(active(X)) | → | isNePal(X) | | isPal(mark(X)) | → | isPal(X) |
| isPal(active(X)) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, isQid, nil
Strategy
The following SCCs where found
| isQid#(mark(X)) → isQid#(X) | isQid#(active(X)) → isQid#(X) |
| active#(isList(V)) → mark#(isNeList(V)) | active#(isQid(a)) → mark#(tt) |
| active#(__(__(X, Y), Z)) → mark#(__(X, __(Y, Z))) | active#(__(X, nil)) → mark#(X) |
| mark#(tt) → active#(tt) | mark#(o) → active#(o) |
| mark#(a) → active#(a) | active#(isNePal(V)) → mark#(isQid(V)) |
| mark#(isNePal(X)) → active#(isNePal(X)) | mark#(e) → active#(e) |
| mark#(u) → active#(u) | active#(isList(nil)) → mark#(tt) |
| active#(isNeList(__(V1, V2))) → mark#(and(isList(V1), isNeList(V2))) | mark#(i) → active#(i) |
| active#(isNeList(V)) → mark#(isQid(V)) | mark#(nil) → active#(nil) |
| active#(isQid(i)) → mark#(tt) | mark#(and(X1, X2)) → active#(and(mark(X1), X2)) |
| mark#(__(X1, X2)) → mark#(X2) | active#(isQid(o)) → mark#(tt) |
| active#(isQid(e)) → mark#(tt) | active#(isNeList(__(V1, V2))) → mark#(and(isNeList(V1), isList(V2))) |
| active#(isPal(V)) → mark#(isNePal(V)) | active#(__(nil, X)) → mark#(X) |
| mark#(isPal(X)) → active#(isPal(X)) | active#(isList(__(V1, V2))) → mark#(and(isList(V1), isList(V2))) |
| active#(isNePal(__(I, __(P, I)))) → mark#(and(isQid(I), isPal(P))) | mark#(__(X1, X2)) → active#(__(mark(X1), mark(X2))) |
| active#(and(tt, X)) → mark#(X) | active#(isQid(u)) → mark#(tt) |
| mark#(isQid(X)) → active#(isQid(X)) | mark#(and(X1, X2)) → mark#(X1) |
| mark#(isList(X)) → active#(isList(X)) | mark#(isNeList(X)) → active#(isNeList(X)) |
| active#(isPal(nil)) → mark#(tt) | mark#(__(X1, X2)) → mark#(X1) |
| isPal#(mark(X)) → isPal#(X) | isPal#(active(X)) → isPal#(X) |
| isNeList#(active(X)) → isNeList#(X) | isNeList#(mark(X)) → isNeList#(X) |
| __#(active(X1), X2) → __#(X1, X2) | __#(mark(X1), X2) → __#(X1, X2) |
| __#(X1, mark(X2)) → __#(X1, X2) | __#(X1, active(X2)) → __#(X1, X2) |
| isList#(active(X)) → isList#(X) | isList#(mark(X)) → isList#(X) |
| and#(active(X1), X2) → and#(X1, X2) | and#(X1, active(X2)) → and#(X1, X2) |
| and#(mark(X1), X2) → and#(X1, X2) | and#(X1, mark(X2)) → and#(X1, X2) |
| isNePal#(active(X)) → isNePal#(X) | isNePal#(mark(X)) → isNePal#(X) |
Problem 2: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| active#(isList(V)) | → | mark#(isNeList(V)) | | active#(isQid(a)) | → | mark#(tt) |
| active#(__(__(X, Y), Z)) | → | mark#(__(X, __(Y, Z))) | | active#(__(X, nil)) | → | mark#(X) |
| mark#(tt) | → | active#(tt) | | mark#(o) | → | active#(o) |
| mark#(a) | → | active#(a) | | active#(isNePal(V)) | → | mark#(isQid(V)) |
| mark#(isNePal(X)) | → | active#(isNePal(X)) | | mark#(e) | → | active#(e) |
| mark#(u) | → | active#(u) | | active#(isList(nil)) | → | mark#(tt) |
| active#(isNeList(__(V1, V2))) | → | mark#(and(isList(V1), isNeList(V2))) | | mark#(nil) | → | active#(nil) |
| active#(isNeList(V)) | → | mark#(isQid(V)) | | mark#(i) | → | active#(i) |
| active#(isQid(i)) | → | mark#(tt) | | mark#(and(X1, X2)) | → | active#(and(mark(X1), X2)) |
| mark#(__(X1, X2)) | → | mark#(X2) | | active#(isQid(o)) | → | mark#(tt) |
| active#(isQid(e)) | → | mark#(tt) | | active#(isNeList(__(V1, V2))) | → | mark#(and(isNeList(V1), isList(V2))) |
| active#(__(nil, X)) | → | mark#(X) | | active#(isPal(V)) | → | mark#(isNePal(V)) |
| mark#(isPal(X)) | → | active#(isPal(X)) | | active#(isList(__(V1, V2))) | → | mark#(and(isList(V1), isList(V2))) |
| active#(isNePal(__(I, __(P, I)))) | → | mark#(and(isQid(I), isPal(P))) | | mark#(__(X1, X2)) | → | active#(__(mark(X1), mark(X2))) |
| active#(and(tt, X)) | → | mark#(X) | | active#(isQid(u)) | → | mark#(tt) |
| mark#(isQid(X)) | → | active#(isQid(X)) | | mark#(and(X1, X2)) | → | mark#(X1) |
| mark#(isList(X)) | → | active#(isList(X)) | | mark#(isNeList(X)) | → | active#(isNeList(X)) |
| active#(isPal(nil)) | → | mark#(tt) | | mark#(__(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(and(tt, X)) | → | mark(X) |
| active(isList(V)) | → | mark(isNeList(V)) | | active(isList(nil)) | → | mark(tt) |
| active(isList(__(V1, V2))) | → | mark(and(isList(V1), isList(V2))) | | active(isNeList(V)) | → | mark(isQid(V)) |
| active(isNeList(__(V1, V2))) | → | mark(and(isList(V1), isNeList(V2))) | | active(isNeList(__(V1, V2))) | → | mark(and(isNeList(V1), isList(V2))) |
| active(isNePal(V)) | → | mark(isQid(V)) | | active(isNePal(__(I, __(P, I)))) | → | mark(and(isQid(I), isPal(P))) |
| active(isPal(V)) | → | mark(isNePal(V)) | | active(isPal(nil)) | → | mark(tt) |
| active(isQid(a)) | → | mark(tt) | | active(isQid(e)) | → | mark(tt) |
| active(isQid(i)) | → | mark(tt) | | active(isQid(o)) | → | mark(tt) |
| active(isQid(u)) | → | mark(tt) | | mark(__(X1, X2)) | → | active(__(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(tt) | → | active(tt) | | mark(isList(X)) | → | active(isList(X)) |
| mark(isNeList(X)) | → | active(isNeList(X)) | | mark(isQid(X)) | → | active(isQid(X)) |
| mark(isNePal(X)) | → | active(isNePal(X)) | | mark(isPal(X)) | → | active(isPal(X)) |
| mark(a) | → | active(a) | | mark(e) | → | active(e) |
| mark(i) | → | active(i) | | mark(o) | → | active(o) |
| mark(u) | → | active(u) | | __(mark(X1), X2) | → | __(X1, X2) |
| __(X1, mark(X2)) | → | __(X1, X2) | | __(active(X1), X2) | → | __(X1, X2) |
| __(X1, active(X2)) | → | __(X1, X2) | | and(mark(X1), X2) | → | and(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | and(active(X1), X2) | → | and(X1, X2) |
| and(X1, active(X2)) | → | and(X1, X2) | | isList(mark(X)) | → | isList(X) |
| isList(active(X)) | → | isList(X) | | isNeList(mark(X)) | → | isNeList(X) |
| isNeList(active(X)) | → | isNeList(X) | | isQid(mark(X)) | → | isQid(X) |
| isQid(active(X)) | → | isQid(X) | | isNePal(mark(X)) | → | isNePal(X) |
| isNePal(active(X)) | → | isNePal(X) | | isPal(mark(X)) | → | isPal(X) |
| isPal(active(X)) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, isQid, nil
Strategy
Function Precedence
active < isList = e = a = isNeList = o = __ = mark = isPal = mark# = i = and = u = tt = isNePal = isQid = active# = nil
Argument Filtering
isList: all arguments are removed from isList
e: all arguments are removed from e
a: all arguments are removed from a
isNeList: all arguments are removed from isNeList
o: all arguments are removed from o
__: all arguments are removed from __
mark: all arguments are removed from mark
isPal: all arguments are removed from isPal
mark#: all arguments are removed from mark#
i: all arguments are removed from i
and: all arguments are removed from and
u: all arguments are removed from u
tt: all arguments are removed from tt
isNePal: all arguments are removed from isNePal
active: collapses to 1
isQid: all arguments are removed from isQid
active#: collapses to 1
nil: all arguments are removed from nil
Status
isList: multiset
e: multiset
a: multiset
isNeList: multiset
o: multiset
__: multiset
mark: multiset
isPal: multiset
mark#: multiset
i: multiset
and: multiset
u: multiset
tt: multiset
isNePal: multiset
isQid: multiset
nil: multiset
Usable Rules
| isQid(active(X)) → isQid(X) | active(isQid(a)) → mark(tt) |
| active(__(X, nil)) → mark(X) | __(active(X1), X2) → __(X1, X2) |
| active(isNePal(V)) → mark(isQid(V)) | and(active(X1), X2) → and(X1, X2) |
| mark(isQid(X)) → active(isQid(X)) | active(isQid(o)) → mark(tt) |
| mark(isNePal(X)) → active(isNePal(X)) | active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z))) |
| isNePal(mark(X)) → isNePal(X) | isPal(active(X)) → isPal(X) |
| mark(nil) → active(nil) | active(isQid(u)) → mark(tt) |
| mark(__(X1, X2)) → active(__(mark(X1), mark(X2))) | active(isPal(nil)) → mark(tt) |
| isList(mark(X)) → isList(X) | active(and(tt, X)) → mark(X) |
| isList(active(X)) → isList(X) | and(mark(X1), X2) → and(X1, X2) |
| mark(a) → active(a) | mark(u) → active(u) |
| isPal(mark(X)) → isPal(X) | mark(o) → active(o) |
| active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P))) | mark(e) → active(e) |
| isNeList(mark(X)) → isNeList(X) | __(X1, mark(X2)) → __(X1, X2) |
| and(X1, mark(X2)) → and(X1, X2) | mark(and(X1, X2)) → active(and(mark(X1), X2)) |
| active(isQid(i)) → mark(tt) | active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2))) |
| active(isList(V)) → mark(isNeList(V)) | active(isQid(e)) → mark(tt) |
| mark(i) → active(i) | isNePal(active(X)) → isNePal(X) |
| active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2))) | active(__(nil, X)) → mark(X) |
| active(isPal(V)) → mark(isNePal(V)) | isNeList(active(X)) → isNeList(X) |
| mark(tt) → active(tt) | active(isNeList(V)) → mark(isQid(V)) |
| active(isList(nil)) → mark(tt) | mark(isNeList(X)) → active(isNeList(X)) |
| mark(isList(X)) → active(isList(X)) | __(mark(X1), X2) → __(X1, X2) |
| active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2))) | isQid(mark(X)) → isQid(X) |
| mark(isPal(X)) → active(isPal(X)) | and(X1, active(X2)) → and(X1, X2) |
| __(X1, active(X2)) → __(X1, X2) |
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#(tt) → active#(tt) | mark#(e) → active#(e) |
Problem 12: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| active#(isList(V)) | → | mark#(isNeList(V)) | | active#(isQid(a)) | → | mark#(tt) |
| active#(__(__(X, Y), Z)) | → | mark#(__(X, __(Y, Z))) | | active#(__(X, nil)) | → | mark#(X) |
| mark#(a) | → | active#(a) | | mark#(o) | → | active#(o) |
| active#(isNePal(V)) | → | mark#(isQid(V)) | | mark#(isNePal(X)) | → | active#(isNePal(X)) |
| mark#(u) | → | active#(u) | | active#(isNeList(__(V1, V2))) | → | mark#(and(isList(V1), isNeList(V2))) |
| active#(isList(nil)) | → | mark#(tt) | | active#(isNeList(V)) | → | mark#(isQid(V)) |
| mark#(nil) | → | active#(nil) | | mark#(i) | → | active#(i) |
| active#(isQid(i)) | → | mark#(tt) | | mark#(and(X1, X2)) | → | active#(and(mark(X1), X2)) |
| mark#(__(X1, X2)) | → | mark#(X2) | | active#(isQid(o)) | → | mark#(tt) |
| active#(isQid(e)) | → | mark#(tt) | | active#(isNeList(__(V1, V2))) | → | mark#(and(isNeList(V1), isList(V2))) |
| active#(__(nil, X)) | → | mark#(X) | | active#(isPal(V)) | → | mark#(isNePal(V)) |
| mark#(isPal(X)) | → | active#(isPal(X)) | | active#(isList(__(V1, V2))) | → | mark#(and(isList(V1), isList(V2))) |
| mark#(__(X1, X2)) | → | active#(__(mark(X1), mark(X2))) | | active#(isNePal(__(I, __(P, I)))) | → | mark#(and(isQid(I), isPal(P))) |
| active#(and(tt, X)) | → | mark#(X) | | active#(isQid(u)) | → | mark#(tt) |
| mark#(isQid(X)) | → | active#(isQid(X)) | | mark#(isList(X)) | → | active#(isList(X)) |
| mark#(and(X1, X2)) | → | mark#(X1) | | mark#(isNeList(X)) | → | active#(isNeList(X)) |
| active#(isPal(nil)) | → | mark#(tt) | | mark#(__(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(and(tt, X)) | → | mark(X) |
| active(isList(V)) | → | mark(isNeList(V)) | | active(isList(nil)) | → | mark(tt) |
| active(isList(__(V1, V2))) | → | mark(and(isList(V1), isList(V2))) | | active(isNeList(V)) | → | mark(isQid(V)) |
| active(isNeList(__(V1, V2))) | → | mark(and(isList(V1), isNeList(V2))) | | active(isNeList(__(V1, V2))) | → | mark(and(isNeList(V1), isList(V2))) |
| active(isNePal(V)) | → | mark(isQid(V)) | | active(isNePal(__(I, __(P, I)))) | → | mark(and(isQid(I), isPal(P))) |
| active(isPal(V)) | → | mark(isNePal(V)) | | active(isPal(nil)) | → | mark(tt) |
| active(isQid(a)) | → | mark(tt) | | active(isQid(e)) | → | mark(tt) |
| active(isQid(i)) | → | mark(tt) | | active(isQid(o)) | → | mark(tt) |
| active(isQid(u)) | → | mark(tt) | | mark(__(X1, X2)) | → | active(__(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(tt) | → | active(tt) | | mark(isList(X)) | → | active(isList(X)) |
| mark(isNeList(X)) | → | active(isNeList(X)) | | mark(isQid(X)) | → | active(isQid(X)) |
| mark(isNePal(X)) | → | active(isNePal(X)) | | mark(isPal(X)) | → | active(isPal(X)) |
| mark(a) | → | active(a) | | mark(e) | → | active(e) |
| mark(i) | → | active(i) | | mark(o) | → | active(o) |
| mark(u) | → | active(u) | | __(mark(X1), X2) | → | __(X1, X2) |
| __(X1, mark(X2)) | → | __(X1, X2) | | __(active(X1), X2) | → | __(X1, X2) |
| __(X1, active(X2)) | → | __(X1, X2) | | and(mark(X1), X2) | → | and(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | and(active(X1), X2) | → | and(X1, X2) |
| and(X1, active(X2)) | → | and(X1, X2) | | isList(mark(X)) | → | isList(X) |
| isList(active(X)) | → | isList(X) | | isNeList(mark(X)) | → | isNeList(X) |
| isNeList(active(X)) | → | isNeList(X) | | isQid(mark(X)) | → | isQid(X) |
| isQid(active(X)) | → | isQid(X) | | isNePal(mark(X)) | → | isNePal(X) |
| isNePal(active(X)) | → | isNePal(X) | | isPal(mark(X)) | → | isPal(X) |
| isPal(active(X)) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, isQid, nil
Strategy
Function Precedence
active < active# < isList = e = a = isNeList = o = __ = mark = isPal = mark# = i = and = u = tt = isNePal = isQid = nil
Argument Filtering
isList: all arguments are removed from isList
e: all arguments are removed from e
a: all arguments are removed from a
isNeList: all arguments are removed from isNeList
o: all arguments are removed from o
__: all arguments are removed from __
mark: all arguments are removed from mark
isPal: all arguments are removed from isPal
mark#: all arguments are removed from mark#
i: all arguments are removed from i
and: all arguments are removed from and
u: all arguments are removed from u
tt: all arguments are removed from tt
isNePal: all arguments are removed from isNePal
active: collapses to 1
isQid: all arguments are removed from isQid
active#: collapses to 1
nil: all arguments are removed from nil
Status
isList: multiset
e: multiset
a: multiset
isNeList: multiset
o: multiset
__: multiset
mark: multiset
isPal: multiset
mark#: multiset
i: multiset
and: multiset
u: multiset
tt: multiset
isNePal: multiset
isQid: multiset
nil: multiset
Usable Rules
| isQid(active(X)) → isQid(X) | active(isQid(a)) → mark(tt) |
| active(__(X, nil)) → mark(X) | __(active(X1), X2) → __(X1, X2) |
| active(isNePal(V)) → mark(isQid(V)) | and(active(X1), X2) → and(X1, X2) |
| mark(isQid(X)) → active(isQid(X)) | active(isQid(o)) → mark(tt) |
| mark(isNePal(X)) → active(isNePal(X)) | active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z))) |
| isNePal(mark(X)) → isNePal(X) | isPal(active(X)) → isPal(X) |
| mark(nil) → active(nil) | active(isQid(u)) → mark(tt) |
| mark(__(X1, X2)) → active(__(mark(X1), mark(X2))) | active(isPal(nil)) → mark(tt) |
| isList(mark(X)) → isList(X) | active(and(tt, X)) → mark(X) |
| isList(active(X)) → isList(X) | and(mark(X1), X2) → and(X1, X2) |
| mark(a) → active(a) | mark(u) → active(u) |
| isPal(mark(X)) → isPal(X) | mark(o) → active(o) |
| active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P))) | mark(e) → active(e) |
| isNeList(mark(X)) → isNeList(X) | __(X1, mark(X2)) → __(X1, X2) |
| and(X1, mark(X2)) → and(X1, X2) | mark(and(X1, X2)) → active(and(mark(X1), X2)) |
| active(isQid(i)) → mark(tt) | active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2))) |
| active(isList(V)) → mark(isNeList(V)) | active(isQid(e)) → mark(tt) |
| mark(i) → active(i) | isNePal(active(X)) → isNePal(X) |
| active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2))) | active(__(nil, X)) → mark(X) |
| active(isPal(V)) → mark(isNePal(V)) | isNeList(active(X)) → isNeList(X) |
| mark(tt) → active(tt) | active(isNeList(V)) → mark(isQid(V)) |
| active(isList(nil)) → mark(tt) | mark(isNeList(X)) → active(isNeList(X)) |
| mark(isList(X)) → active(isList(X)) | __(mark(X1), X2) → __(X1, X2) |
| active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2))) | isQid(mark(X)) → isQid(X) |
| mark(isPal(X)) → active(isPal(X)) | and(X1, active(X2)) → and(X1, X2) |
| __(X1, active(X2)) → __(X1, X2) |
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#(i) → active#(i) | mark#(nil) → active#(nil) |
| mark#(o) → active#(o) | mark#(a) → active#(a) |
| mark#(u) → active#(u) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| isQid#(mark(X)) | → | isQid#(X) | | isQid#(active(X)) | → | isQid#(X) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(and(tt, X)) | → | mark(X) |
| active(isList(V)) | → | mark(isNeList(V)) | | active(isList(nil)) | → | mark(tt) |
| active(isList(__(V1, V2))) | → | mark(and(isList(V1), isList(V2))) | | active(isNeList(V)) | → | mark(isQid(V)) |
| active(isNeList(__(V1, V2))) | → | mark(and(isList(V1), isNeList(V2))) | | active(isNeList(__(V1, V2))) | → | mark(and(isNeList(V1), isList(V2))) |
| active(isNePal(V)) | → | mark(isQid(V)) | | active(isNePal(__(I, __(P, I)))) | → | mark(and(isQid(I), isPal(P))) |
| active(isPal(V)) | → | mark(isNePal(V)) | | active(isPal(nil)) | → | mark(tt) |
| active(isQid(a)) | → | mark(tt) | | active(isQid(e)) | → | mark(tt) |
| active(isQid(i)) | → | mark(tt) | | active(isQid(o)) | → | mark(tt) |
| active(isQid(u)) | → | mark(tt) | | mark(__(X1, X2)) | → | active(__(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(tt) | → | active(tt) | | mark(isList(X)) | → | active(isList(X)) |
| mark(isNeList(X)) | → | active(isNeList(X)) | | mark(isQid(X)) | → | active(isQid(X)) |
| mark(isNePal(X)) | → | active(isNePal(X)) | | mark(isPal(X)) | → | active(isPal(X)) |
| mark(a) | → | active(a) | | mark(e) | → | active(e) |
| mark(i) | → | active(i) | | mark(o) | → | active(o) |
| mark(u) | → | active(u) | | __(mark(X1), X2) | → | __(X1, X2) |
| __(X1, mark(X2)) | → | __(X1, X2) | | __(active(X1), X2) | → | __(X1, X2) |
| __(X1, active(X2)) | → | __(X1, X2) | | and(mark(X1), X2) | → | and(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | and(active(X1), X2) | → | and(X1, X2) |
| and(X1, active(X2)) | → | and(X1, X2) | | isList(mark(X)) | → | isList(X) |
| isList(active(X)) | → | isList(X) | | isNeList(mark(X)) | → | isNeList(X) |
| isNeList(active(X)) | → | isNeList(X) | | isQid(mark(X)) | → | isQid(X) |
| isQid(active(X)) | → | isQid(X) | | isNePal(mark(X)) | → | isNePal(X) |
| isNePal(active(X)) | → | isNePal(X) | | isPal(mark(X)) | → | isPal(X) |
| isPal(active(X)) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, isQid, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| isQid#(mark(X)) | → | isQid#(X) | | isQid#(active(X)) | → | isQid#(X) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| isList#(active(X)) | → | isList#(X) | | isList#(mark(X)) | → | isList#(X) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(and(tt, X)) | → | mark(X) |
| active(isList(V)) | → | mark(isNeList(V)) | | active(isList(nil)) | → | mark(tt) |
| active(isList(__(V1, V2))) | → | mark(and(isList(V1), isList(V2))) | | active(isNeList(V)) | → | mark(isQid(V)) |
| active(isNeList(__(V1, V2))) | → | mark(and(isList(V1), isNeList(V2))) | | active(isNeList(__(V1, V2))) | → | mark(and(isNeList(V1), isList(V2))) |
| active(isNePal(V)) | → | mark(isQid(V)) | | active(isNePal(__(I, __(P, I)))) | → | mark(and(isQid(I), isPal(P))) |
| active(isPal(V)) | → | mark(isNePal(V)) | | active(isPal(nil)) | → | mark(tt) |
| active(isQid(a)) | → | mark(tt) | | active(isQid(e)) | → | mark(tt) |
| active(isQid(i)) | → | mark(tt) | | active(isQid(o)) | → | mark(tt) |
| active(isQid(u)) | → | mark(tt) | | mark(__(X1, X2)) | → | active(__(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(tt) | → | active(tt) | | mark(isList(X)) | → | active(isList(X)) |
| mark(isNeList(X)) | → | active(isNeList(X)) | | mark(isQid(X)) | → | active(isQid(X)) |
| mark(isNePal(X)) | → | active(isNePal(X)) | | mark(isPal(X)) | → | active(isPal(X)) |
| mark(a) | → | active(a) | | mark(e) | → | active(e) |
| mark(i) | → | active(i) | | mark(o) | → | active(o) |
| mark(u) | → | active(u) | | __(mark(X1), X2) | → | __(X1, X2) |
| __(X1, mark(X2)) | → | __(X1, X2) | | __(active(X1), X2) | → | __(X1, X2) |
| __(X1, active(X2)) | → | __(X1, X2) | | and(mark(X1), X2) | → | and(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | and(active(X1), X2) | → | and(X1, X2) |
| and(X1, active(X2)) | → | and(X1, X2) | | isList(mark(X)) | → | isList(X) |
| isList(active(X)) | → | isList(X) | | isNeList(mark(X)) | → | isNeList(X) |
| isNeList(active(X)) | → | isNeList(X) | | isQid(mark(X)) | → | isQid(X) |
| isQid(active(X)) | → | isQid(X) | | isNePal(mark(X)) | → | isNePal(X) |
| isNePal(active(X)) | → | isNePal(X) | | isPal(mark(X)) | → | isPal(X) |
| isPal(active(X)) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, isQid, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| isList#(active(X)) | → | isList#(X) | | isList#(mark(X)) | → | isList#(X) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| __#(active(X1), X2) | → | __#(X1, X2) | | __#(mark(X1), X2) | → | __#(X1, X2) |
| __#(X1, mark(X2)) | → | __#(X1, X2) | | __#(X1, active(X2)) | → | __#(X1, X2) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(and(tt, X)) | → | mark(X) |
| active(isList(V)) | → | mark(isNeList(V)) | | active(isList(nil)) | → | mark(tt) |
| active(isList(__(V1, V2))) | → | mark(and(isList(V1), isList(V2))) | | active(isNeList(V)) | → | mark(isQid(V)) |
| active(isNeList(__(V1, V2))) | → | mark(and(isList(V1), isNeList(V2))) | | active(isNeList(__(V1, V2))) | → | mark(and(isNeList(V1), isList(V2))) |
| active(isNePal(V)) | → | mark(isQid(V)) | | active(isNePal(__(I, __(P, I)))) | → | mark(and(isQid(I), isPal(P))) |
| active(isPal(V)) | → | mark(isNePal(V)) | | active(isPal(nil)) | → | mark(tt) |
| active(isQid(a)) | → | mark(tt) | | active(isQid(e)) | → | mark(tt) |
| active(isQid(i)) | → | mark(tt) | | active(isQid(o)) | → | mark(tt) |
| active(isQid(u)) | → | mark(tt) | | mark(__(X1, X2)) | → | active(__(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(tt) | → | active(tt) | | mark(isList(X)) | → | active(isList(X)) |
| mark(isNeList(X)) | → | active(isNeList(X)) | | mark(isQid(X)) | → | active(isQid(X)) |
| mark(isNePal(X)) | → | active(isNePal(X)) | | mark(isPal(X)) | → | active(isPal(X)) |
| mark(a) | → | active(a) | | mark(e) | → | active(e) |
| mark(i) | → | active(i) | | mark(o) | → | active(o) |
| mark(u) | → | active(u) | | __(mark(X1), X2) | → | __(X1, X2) |
| __(X1, mark(X2)) | → | __(X1, X2) | | __(active(X1), X2) | → | __(X1, X2) |
| __(X1, active(X2)) | → | __(X1, X2) | | and(mark(X1), X2) | → | and(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | and(active(X1), X2) | → | and(X1, X2) |
| and(X1, active(X2)) | → | and(X1, X2) | | isList(mark(X)) | → | isList(X) |
| isList(active(X)) | → | isList(X) | | isNeList(mark(X)) | → | isNeList(X) |
| isNeList(active(X)) | → | isNeList(X) | | isQid(mark(X)) | → | isQid(X) |
| isQid(active(X)) | → | isQid(X) | | isNePal(mark(X)) | → | isNePal(X) |
| isNePal(active(X)) | → | isNePal(X) | | isPal(mark(X)) | → | isPal(X) |
| isPal(active(X)) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, isQid, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| __#(mark(X1), X2) | → | __#(X1, X2) | | __#(active(X1), X2) | → | __#(X1, X2) |
Problem 10: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| __#(X1, mark(X2)) | → | __#(X1, X2) | | __#(X1, active(X2)) | → | __#(X1, X2) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(and(tt, X)) | → | mark(X) |
| active(isList(V)) | → | mark(isNeList(V)) | | active(isList(nil)) | → | mark(tt) |
| active(isList(__(V1, V2))) | → | mark(and(isList(V1), isList(V2))) | | active(isNeList(V)) | → | mark(isQid(V)) |
| active(isNeList(__(V1, V2))) | → | mark(and(isList(V1), isNeList(V2))) | | active(isNeList(__(V1, V2))) | → | mark(and(isNeList(V1), isList(V2))) |
| active(isNePal(V)) | → | mark(isQid(V)) | | active(isNePal(__(I, __(P, I)))) | → | mark(and(isQid(I), isPal(P))) |
| active(isPal(V)) | → | mark(isNePal(V)) | | active(isPal(nil)) | → | mark(tt) |
| active(isQid(a)) | → | mark(tt) | | active(isQid(e)) | → | mark(tt) |
| active(isQid(i)) | → | mark(tt) | | active(isQid(o)) | → | mark(tt) |
| active(isQid(u)) | → | mark(tt) | | mark(__(X1, X2)) | → | active(__(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(tt) | → | active(tt) | | mark(isList(X)) | → | active(isList(X)) |
| mark(isNeList(X)) | → | active(isNeList(X)) | | mark(isQid(X)) | → | active(isQid(X)) |
| mark(isNePal(X)) | → | active(isNePal(X)) | | mark(isPal(X)) | → | active(isPal(X)) |
| mark(a) | → | active(a) | | mark(e) | → | active(e) |
| mark(i) | → | active(i) | | mark(o) | → | active(o) |
| mark(u) | → | active(u) | | __(mark(X1), X2) | → | __(X1, X2) |
| __(X1, mark(X2)) | → | __(X1, X2) | | __(active(X1), X2) | → | __(X1, X2) |
| __(X1, active(X2)) | → | __(X1, X2) | | and(mark(X1), X2) | → | and(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | and(active(X1), X2) | → | and(X1, X2) |
| and(X1, active(X2)) | → | and(X1, X2) | | isList(mark(X)) | → | isList(X) |
| isList(active(X)) | → | isList(X) | | isNeList(mark(X)) | → | isNeList(X) |
| isNeList(active(X)) | → | isNeList(X) | | isQid(mark(X)) | → | isQid(X) |
| isQid(active(X)) | → | isQid(X) | | isNePal(mark(X)) | → | isNePal(X) |
| isNePal(active(X)) | → | isNePal(X) | | isPal(mark(X)) | → | isPal(X) |
| isPal(active(X)) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, isQid, nil
Strategy
Function Precedence
mark = active < isList = e = a = isNeList = o = __ = isPal = i = and = __# = u = tt = isNePal = isQid = nil
Argument Filtering
isList: all arguments are removed from isList
e: all arguments are removed from e
a: all arguments are removed from a
isNeList: all arguments are removed from isNeList
o: all arguments are removed from o
__: all arguments are removed from __
mark: 1
isPal: all arguments are removed from isPal
i: all arguments are removed from i
and: all arguments are removed from and
__#: collapses to 2
u: all arguments are removed from u
tt: all arguments are removed from tt
isNePal: all arguments are removed from isNePal
active: collapses to 1
isQid: all arguments are removed from isQid
nil: all arguments are removed from nil
Status
isList: multiset
e: multiset
a: multiset
isNeList: multiset
o: multiset
__: multiset
mark: multiset
isPal: multiset
i: multiset
and: multiset
u: multiset
tt: multiset
isNePal: multiset
isQid: 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.
| __#(X1, mark(X2)) → __#(X1, X2) |
Problem 13: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| __#(X1, active(X2)) | → | __#(X1, X2) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(and(tt, X)) | → | mark(X) |
| active(isList(V)) | → | mark(isNeList(V)) | | active(isList(nil)) | → | mark(tt) |
| active(isList(__(V1, V2))) | → | mark(and(isList(V1), isList(V2))) | | active(isNeList(V)) | → | mark(isQid(V)) |
| active(isNeList(__(V1, V2))) | → | mark(and(isList(V1), isNeList(V2))) | | active(isNeList(__(V1, V2))) | → | mark(and(isNeList(V1), isList(V2))) |
| active(isNePal(V)) | → | mark(isQid(V)) | | active(isNePal(__(I, __(P, I)))) | → | mark(and(isQid(I), isPal(P))) |
| active(isPal(V)) | → | mark(isNePal(V)) | | active(isPal(nil)) | → | mark(tt) |
| active(isQid(a)) | → | mark(tt) | | active(isQid(e)) | → | mark(tt) |
| active(isQid(i)) | → | mark(tt) | | active(isQid(o)) | → | mark(tt) |
| active(isQid(u)) | → | mark(tt) | | mark(__(X1, X2)) | → | active(__(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(tt) | → | active(tt) | | mark(isList(X)) | → | active(isList(X)) |
| mark(isNeList(X)) | → | active(isNeList(X)) | | mark(isQid(X)) | → | active(isQid(X)) |
| mark(isNePal(X)) | → | active(isNePal(X)) | | mark(isPal(X)) | → | active(isPal(X)) |
| mark(a) | → | active(a) | | mark(e) | → | active(e) |
| mark(i) | → | active(i) | | mark(o) | → | active(o) |
| mark(u) | → | active(u) | | __(mark(X1), X2) | → | __(X1, X2) |
| __(X1, mark(X2)) | → | __(X1, X2) | | __(active(X1), X2) | → | __(X1, X2) |
| __(X1, active(X2)) | → | __(X1, X2) | | and(mark(X1), X2) | → | and(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | and(active(X1), X2) | → | and(X1, X2) |
| and(X1, active(X2)) | → | and(X1, X2) | | isList(mark(X)) | → | isList(X) |
| isList(active(X)) | → | isList(X) | | isNeList(mark(X)) | → | isNeList(X) |
| isNeList(active(X)) | → | isNeList(X) | | isQid(mark(X)) | → | isQid(X) |
| isQid(active(X)) | → | isQid(X) | | isNePal(mark(X)) | → | isNePal(X) |
| isNePal(active(X)) | → | isNePal(X) | | isPal(mark(X)) | → | isPal(X) |
| isPal(active(X)) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, isQid, nil
Strategy
Function Precedence
active < isList = e = a = isNeList = o = __ = mark = isPal = i = and = __# = u = tt = isNePal = isQid = nil
Argument Filtering
isList: all arguments are removed from isList
e: all arguments are removed from e
a: all arguments are removed from a
isNeList: all arguments are removed from isNeList
o: all arguments are removed from o
__: 1 2
mark: all arguments are removed from mark
isPal: collapses to 1
i: all arguments are removed from i
and: 1 2
__#: collapses to 2
u: all arguments are removed from u
tt: all arguments are removed from tt
isNePal: all arguments are removed from isNePal
active: 1
isQid: all arguments are removed from isQid
nil: all arguments are removed from nil
Status
isList: multiset
e: multiset
a: multiset
isNeList: multiset
o: multiset
__: lexicographic with permutation 1 → 2 2 → 1
mark: multiset
i: multiset
and: lexicographic with permutation 1 → 2 2 → 1
u: multiset
tt: multiset
isNePal: multiset
active: multiset
isQid: 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.
| __#(X1, active(X2)) → __#(X1, X2) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| isNeList#(active(X)) | → | isNeList#(X) | | isNeList#(mark(X)) | → | isNeList#(X) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(and(tt, X)) | → | mark(X) |
| active(isList(V)) | → | mark(isNeList(V)) | | active(isList(nil)) | → | mark(tt) |
| active(isList(__(V1, V2))) | → | mark(and(isList(V1), isList(V2))) | | active(isNeList(V)) | → | mark(isQid(V)) |
| active(isNeList(__(V1, V2))) | → | mark(and(isList(V1), isNeList(V2))) | | active(isNeList(__(V1, V2))) | → | mark(and(isNeList(V1), isList(V2))) |
| active(isNePal(V)) | → | mark(isQid(V)) | | active(isNePal(__(I, __(P, I)))) | → | mark(and(isQid(I), isPal(P))) |
| active(isPal(V)) | → | mark(isNePal(V)) | | active(isPal(nil)) | → | mark(tt) |
| active(isQid(a)) | → | mark(tt) | | active(isQid(e)) | → | mark(tt) |
| active(isQid(i)) | → | mark(tt) | | active(isQid(o)) | → | mark(tt) |
| active(isQid(u)) | → | mark(tt) | | mark(__(X1, X2)) | → | active(__(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(tt) | → | active(tt) | | mark(isList(X)) | → | active(isList(X)) |
| mark(isNeList(X)) | → | active(isNeList(X)) | | mark(isQid(X)) | → | active(isQid(X)) |
| mark(isNePal(X)) | → | active(isNePal(X)) | | mark(isPal(X)) | → | active(isPal(X)) |
| mark(a) | → | active(a) | | mark(e) | → | active(e) |
| mark(i) | → | active(i) | | mark(o) | → | active(o) |
| mark(u) | → | active(u) | | __(mark(X1), X2) | → | __(X1, X2) |
| __(X1, mark(X2)) | → | __(X1, X2) | | __(active(X1), X2) | → | __(X1, X2) |
| __(X1, active(X2)) | → | __(X1, X2) | | and(mark(X1), X2) | → | and(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | and(active(X1), X2) | → | and(X1, X2) |
| and(X1, active(X2)) | → | and(X1, X2) | | isList(mark(X)) | → | isList(X) |
| isList(active(X)) | → | isList(X) | | isNeList(mark(X)) | → | isNeList(X) |
| isNeList(active(X)) | → | isNeList(X) | | isQid(mark(X)) | → | isQid(X) |
| isQid(active(X)) | → | isQid(X) | | isNePal(mark(X)) | → | isNePal(X) |
| isNePal(active(X)) | → | isNePal(X) | | isPal(mark(X)) | → | isPal(X) |
| isPal(active(X)) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, isQid, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| isNeList#(active(X)) | → | isNeList#(X) | | isNeList#(mark(X)) | → | isNeList#(X) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| isNePal#(active(X)) | → | isNePal#(X) | | isNePal#(mark(X)) | → | isNePal#(X) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(and(tt, X)) | → | mark(X) |
| active(isList(V)) | → | mark(isNeList(V)) | | active(isList(nil)) | → | mark(tt) |
| active(isList(__(V1, V2))) | → | mark(and(isList(V1), isList(V2))) | | active(isNeList(V)) | → | mark(isQid(V)) |
| active(isNeList(__(V1, V2))) | → | mark(and(isList(V1), isNeList(V2))) | | active(isNeList(__(V1, V2))) | → | mark(and(isNeList(V1), isList(V2))) |
| active(isNePal(V)) | → | mark(isQid(V)) | | active(isNePal(__(I, __(P, I)))) | → | mark(and(isQid(I), isPal(P))) |
| active(isPal(V)) | → | mark(isNePal(V)) | | active(isPal(nil)) | → | mark(tt) |
| active(isQid(a)) | → | mark(tt) | | active(isQid(e)) | → | mark(tt) |
| active(isQid(i)) | → | mark(tt) | | active(isQid(o)) | → | mark(tt) |
| active(isQid(u)) | → | mark(tt) | | mark(__(X1, X2)) | → | active(__(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(tt) | → | active(tt) | | mark(isList(X)) | → | active(isList(X)) |
| mark(isNeList(X)) | → | active(isNeList(X)) | | mark(isQid(X)) | → | active(isQid(X)) |
| mark(isNePal(X)) | → | active(isNePal(X)) | | mark(isPal(X)) | → | active(isPal(X)) |
| mark(a) | → | active(a) | | mark(e) | → | active(e) |
| mark(i) | → | active(i) | | mark(o) | → | active(o) |
| mark(u) | → | active(u) | | __(mark(X1), X2) | → | __(X1, X2) |
| __(X1, mark(X2)) | → | __(X1, X2) | | __(active(X1), X2) | → | __(X1, X2) |
| __(X1, active(X2)) | → | __(X1, X2) | | and(mark(X1), X2) | → | and(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | and(active(X1), X2) | → | and(X1, X2) |
| and(X1, active(X2)) | → | and(X1, X2) | | isList(mark(X)) | → | isList(X) |
| isList(active(X)) | → | isList(X) | | isNeList(mark(X)) | → | isNeList(X) |
| isNeList(active(X)) | → | isNeList(X) | | isQid(mark(X)) | → | isQid(X) |
| isQid(active(X)) | → | isQid(X) | | isNePal(mark(X)) | → | isNePal(X) |
| isNePal(active(X)) | → | isNePal(X) | | isPal(mark(X)) | → | isPal(X) |
| isPal(active(X)) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, isQid, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| isNePal#(active(X)) | → | isNePal#(X) | | isNePal#(mark(X)) | → | isNePal#(X) |
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| and#(active(X1), X2) | → | and#(X1, X2) | | and#(X1, active(X2)) | → | and#(X1, X2) |
| and#(mark(X1), X2) | → | and#(X1, X2) | | and#(X1, mark(X2)) | → | and#(X1, X2) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(and(tt, X)) | → | mark(X) |
| active(isList(V)) | → | mark(isNeList(V)) | | active(isList(nil)) | → | mark(tt) |
| active(isList(__(V1, V2))) | → | mark(and(isList(V1), isList(V2))) | | active(isNeList(V)) | → | mark(isQid(V)) |
| active(isNeList(__(V1, V2))) | → | mark(and(isList(V1), isNeList(V2))) | | active(isNeList(__(V1, V2))) | → | mark(and(isNeList(V1), isList(V2))) |
| active(isNePal(V)) | → | mark(isQid(V)) | | active(isNePal(__(I, __(P, I)))) | → | mark(and(isQid(I), isPal(P))) |
| active(isPal(V)) | → | mark(isNePal(V)) | | active(isPal(nil)) | → | mark(tt) |
| active(isQid(a)) | → | mark(tt) | | active(isQid(e)) | → | mark(tt) |
| active(isQid(i)) | → | mark(tt) | | active(isQid(o)) | → | mark(tt) |
| active(isQid(u)) | → | mark(tt) | | mark(__(X1, X2)) | → | active(__(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(tt) | → | active(tt) | | mark(isList(X)) | → | active(isList(X)) |
| mark(isNeList(X)) | → | active(isNeList(X)) | | mark(isQid(X)) | → | active(isQid(X)) |
| mark(isNePal(X)) | → | active(isNePal(X)) | | mark(isPal(X)) | → | active(isPal(X)) |
| mark(a) | → | active(a) | | mark(e) | → | active(e) |
| mark(i) | → | active(i) | | mark(o) | → | active(o) |
| mark(u) | → | active(u) | | __(mark(X1), X2) | → | __(X1, X2) |
| __(X1, mark(X2)) | → | __(X1, X2) | | __(active(X1), X2) | → | __(X1, X2) |
| __(X1, active(X2)) | → | __(X1, X2) | | and(mark(X1), X2) | → | and(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | and(active(X1), X2) | → | and(X1, X2) |
| and(X1, active(X2)) | → | and(X1, X2) | | isList(mark(X)) | → | isList(X) |
| isList(active(X)) | → | isList(X) | | isNeList(mark(X)) | → | isNeList(X) |
| isNeList(active(X)) | → | isNeList(X) | | isQid(mark(X)) | → | isQid(X) |
| isQid(active(X)) | → | isQid(X) | | isNePal(mark(X)) | → | isNePal(X) |
| isNePal(active(X)) | → | isNePal(X) | | isPal(mark(X)) | → | isPal(X) |
| isPal(active(X)) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, isQid, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| and#(active(X1), X2) | → | and#(X1, X2) | | and#(mark(X1), X2) | → | and#(X1, X2) |
Problem 11: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| and#(X1, active(X2)) | → | and#(X1, X2) | | and#(X1, mark(X2)) | → | and#(X1, X2) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(and(tt, X)) | → | mark(X) |
| active(isList(V)) | → | mark(isNeList(V)) | | active(isList(nil)) | → | mark(tt) |
| active(isList(__(V1, V2))) | → | mark(and(isList(V1), isList(V2))) | | active(isNeList(V)) | → | mark(isQid(V)) |
| active(isNeList(__(V1, V2))) | → | mark(and(isList(V1), isNeList(V2))) | | active(isNeList(__(V1, V2))) | → | mark(and(isNeList(V1), isList(V2))) |
| active(isNePal(V)) | → | mark(isQid(V)) | | active(isNePal(__(I, __(P, I)))) | → | mark(and(isQid(I), isPal(P))) |
| active(isPal(V)) | → | mark(isNePal(V)) | | active(isPal(nil)) | → | mark(tt) |
| active(isQid(a)) | → | mark(tt) | | active(isQid(e)) | → | mark(tt) |
| active(isQid(i)) | → | mark(tt) | | active(isQid(o)) | → | mark(tt) |
| active(isQid(u)) | → | mark(tt) | | mark(__(X1, X2)) | → | active(__(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(tt) | → | active(tt) | | mark(isList(X)) | → | active(isList(X)) |
| mark(isNeList(X)) | → | active(isNeList(X)) | | mark(isQid(X)) | → | active(isQid(X)) |
| mark(isNePal(X)) | → | active(isNePal(X)) | | mark(isPal(X)) | → | active(isPal(X)) |
| mark(a) | → | active(a) | | mark(e) | → | active(e) |
| mark(i) | → | active(i) | | mark(o) | → | active(o) |
| mark(u) | → | active(u) | | __(mark(X1), X2) | → | __(X1, X2) |
| __(X1, mark(X2)) | → | __(X1, X2) | | __(active(X1), X2) | → | __(X1, X2) |
| __(X1, active(X2)) | → | __(X1, X2) | | and(mark(X1), X2) | → | and(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | and(active(X1), X2) | → | and(X1, X2) |
| and(X1, active(X2)) | → | and(X1, X2) | | isList(mark(X)) | → | isList(X) |
| isList(active(X)) | → | isList(X) | | isNeList(mark(X)) | → | isNeList(X) |
| isNeList(active(X)) | → | isNeList(X) | | isQid(mark(X)) | → | isQid(X) |
| isQid(active(X)) | → | isQid(X) | | isNePal(mark(X)) | → | isNePal(X) |
| isNePal(active(X)) | → | isNePal(X) | | isPal(mark(X)) | → | isPal(X) |
| isPal(active(X)) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, isQid, nil
Strategy
Function Precedence
mark < isList = e = a = isNeList = o = __ = and# = isPal = i = and = u = tt = isNePal = active = isQid = nil
Argument Filtering
isList: collapses to 1
e: all arguments are removed from e
a: all arguments are removed from a
isNeList: all arguments are removed from isNeList
o: all arguments are removed from o
__: collapses to 2
and#: collapses to 2
mark: 1
isPal: all arguments are removed from isPal
i: all arguments are removed from i
and: collapses to 1
u: all arguments are removed from u
tt: all arguments are removed from tt
isNePal: collapses to 1
active: collapses to 1
isQid: all arguments are removed from isQid
nil: all arguments are removed from nil
Status
e: multiset
a: multiset
isNeList: multiset
o: multiset
mark: multiset
isPal: multiset
i: multiset
u: multiset
tt: multiset
isQid: 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.
| and#(X1, mark(X2)) → and#(X1, X2) |
Problem 14: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| and#(X1, active(X2)) | → | and#(X1, X2) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(and(tt, X)) | → | mark(X) |
| active(isList(V)) | → | mark(isNeList(V)) | | active(isList(nil)) | → | mark(tt) |
| active(isList(__(V1, V2))) | → | mark(and(isList(V1), isList(V2))) | | active(isNeList(V)) | → | mark(isQid(V)) |
| active(isNeList(__(V1, V2))) | → | mark(and(isList(V1), isNeList(V2))) | | active(isNeList(__(V1, V2))) | → | mark(and(isNeList(V1), isList(V2))) |
| active(isNePal(V)) | → | mark(isQid(V)) | | active(isNePal(__(I, __(P, I)))) | → | mark(and(isQid(I), isPal(P))) |
| active(isPal(V)) | → | mark(isNePal(V)) | | active(isPal(nil)) | → | mark(tt) |
| active(isQid(a)) | → | mark(tt) | | active(isQid(e)) | → | mark(tt) |
| active(isQid(i)) | → | mark(tt) | | active(isQid(o)) | → | mark(tt) |
| active(isQid(u)) | → | mark(tt) | | mark(__(X1, X2)) | → | active(__(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(tt) | → | active(tt) | | mark(isList(X)) | → | active(isList(X)) |
| mark(isNeList(X)) | → | active(isNeList(X)) | | mark(isQid(X)) | → | active(isQid(X)) |
| mark(isNePal(X)) | → | active(isNePal(X)) | | mark(isPal(X)) | → | active(isPal(X)) |
| mark(a) | → | active(a) | | mark(e) | → | active(e) |
| mark(i) | → | active(i) | | mark(o) | → | active(o) |
| mark(u) | → | active(u) | | __(mark(X1), X2) | → | __(X1, X2) |
| __(X1, mark(X2)) | → | __(X1, X2) | | __(active(X1), X2) | → | __(X1, X2) |
| __(X1, active(X2)) | → | __(X1, X2) | | and(mark(X1), X2) | → | and(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | and(active(X1), X2) | → | and(X1, X2) |
| and(X1, active(X2)) | → | and(X1, X2) | | isList(mark(X)) | → | isList(X) |
| isList(active(X)) | → | isList(X) | | isNeList(mark(X)) | → | isNeList(X) |
| isNeList(active(X)) | → | isNeList(X) | | isQid(mark(X)) | → | isQid(X) |
| isQid(active(X)) | → | isQid(X) | | isNePal(mark(X)) | → | isNePal(X) |
| isNePal(active(X)) | → | isNePal(X) | | isPal(mark(X)) | → | isPal(X) |
| isPal(active(X)) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, isQid, nil
Strategy
Function Precedence
isList = e = a = isNeList = o = __ = and# = mark = isPal = i = and = u = tt = isNePal = active = isQid = nil
Argument Filtering
isList: all arguments are removed from isList
e: all arguments are removed from e
a: all arguments are removed from a
isNeList: all arguments are removed from isNeList
o: all arguments are removed from o
__: all arguments are removed from __
and#: collapses to 2
mark: all arguments are removed from mark
isPal: all arguments are removed from isPal
i: all arguments are removed from i
and: 1 2
u: all arguments are removed from u
tt: all arguments are removed from tt
isNePal: all arguments are removed from isNePal
active: 1
isQid: all arguments are removed from isQid
nil: all arguments are removed from nil
Status
isList: multiset
e: multiset
a: multiset
isNeList: multiset
o: multiset
__: multiset
mark: multiset
isPal: multiset
i: multiset
and: lexicographic with permutation 1 → 2 2 → 1
u: multiset
tt: multiset
isNePal: multiset
active: multiset
isQid: 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.
| and#(X1, active(X2)) → and#(X1, X2) |
Problem 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| isPal#(mark(X)) | → | isPal#(X) | | isPal#(active(X)) | → | isPal#(X) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(and(tt, X)) | → | mark(X) |
| active(isList(V)) | → | mark(isNeList(V)) | | active(isList(nil)) | → | mark(tt) |
| active(isList(__(V1, V2))) | → | mark(and(isList(V1), isList(V2))) | | active(isNeList(V)) | → | mark(isQid(V)) |
| active(isNeList(__(V1, V2))) | → | mark(and(isList(V1), isNeList(V2))) | | active(isNeList(__(V1, V2))) | → | mark(and(isNeList(V1), isList(V2))) |
| active(isNePal(V)) | → | mark(isQid(V)) | | active(isNePal(__(I, __(P, I)))) | → | mark(and(isQid(I), isPal(P))) |
| active(isPal(V)) | → | mark(isNePal(V)) | | active(isPal(nil)) | → | mark(tt) |
| active(isQid(a)) | → | mark(tt) | | active(isQid(e)) | → | mark(tt) |
| active(isQid(i)) | → | mark(tt) | | active(isQid(o)) | → | mark(tt) |
| active(isQid(u)) | → | mark(tt) | | mark(__(X1, X2)) | → | active(__(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(and(X1, X2)) | → | active(and(mark(X1), X2)) |
| mark(tt) | → | active(tt) | | mark(isList(X)) | → | active(isList(X)) |
| mark(isNeList(X)) | → | active(isNeList(X)) | | mark(isQid(X)) | → | active(isQid(X)) |
| mark(isNePal(X)) | → | active(isNePal(X)) | | mark(isPal(X)) | → | active(isPal(X)) |
| mark(a) | → | active(a) | | mark(e) | → | active(e) |
| mark(i) | → | active(i) | | mark(o) | → | active(o) |
| mark(u) | → | active(u) | | __(mark(X1), X2) | → | __(X1, X2) |
| __(X1, mark(X2)) | → | __(X1, X2) | | __(active(X1), X2) | → | __(X1, X2) |
| __(X1, active(X2)) | → | __(X1, X2) | | and(mark(X1), X2) | → | and(X1, X2) |
| and(X1, mark(X2)) | → | and(X1, X2) | | and(active(X1), X2) | → | and(X1, X2) |
| and(X1, active(X2)) | → | and(X1, X2) | | isList(mark(X)) | → | isList(X) |
| isList(active(X)) | → | isList(X) | | isNeList(mark(X)) | → | isNeList(X) |
| isNeList(active(X)) | → | isNeList(X) | | isQid(mark(X)) | → | isQid(X) |
| isQid(active(X)) | → | isQid(X) | | isNePal(mark(X)) | → | isNePal(X) |
| isNePal(active(X)) | → | isNePal(X) | | isPal(mark(X)) | → | isPal(X) |
| isPal(active(X)) | → | isPal(X) |
Original Signature
Termination of terms over the following signature is verified: isList, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, isQid, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| isPal#(mark(X)) | → | isPal#(X) | | isPal#(active(X)) | → | isPal#(X) |