YES
The TRS could be proven terminating. The proof took 50852 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (4880ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor SubtermCriterion (0ms).
| – Problem 4 was processed with processor SubtermCriterion (30ms).
| – Problem 5 was processed with processor SubtermCriterion (0ms).
| – Problem 6 was processed with processor SubtermCriterion (1ms).
| – Problem 7 was processed with processor SubtermCriterion (0ms).
| – Problem 8 was processed with processor SubtermCriterion (1ms).
| – Problem 9 was processed with processor SubtermCriterion (0ms).
| – Problem 10 was processed with processor SubtermCriterion (1ms).
| – Problem 11 was processed with processor SubtermCriterion (0ms).
| – Problem 12 was processed with processor DependencyGraph (55ms).
| | – Problem 25 was processed with processor SubtermCriterion (1ms).
| – Problem 13 was processed with processor SubtermCriterion (0ms).
| – Problem 14 was processed with processor SubtermCriterion (1ms).
| – Problem 15 was processed with processor SubtermCriterion (0ms).
| – Problem 16 was processed with processor SubtermCriterion (0ms).
| – Problem 17 was processed with processor SubtermCriterion (1ms).
| – Problem 18 was processed with processor SubtermCriterion (1ms).
| – Problem 19 was processed with processor SubtermCriterion (0ms).
| – Problem 20 was processed with processor SubtermCriterion (1ms).
| – Problem 21 was processed with processor ReductionPairSAT (8333ms).
| | – Problem 26 was processed with processor ReductionPairSAT (3981ms).
| – Problem 22 was processed with processor SubtermCriterion (1ms).
| | – Problem 24 was processed with processor SubtermCriterion (0ms).
| – Problem 23 was processed with processor SubtermCriterion (0ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| active#(U71(tt, P)) | → | isPal#(P) | | proper#(U41(X1, X2)) | → | proper#(X2) |
| proper#(U41(X1, X2)) | → | proper#(X1) | | active#(U51(tt, V2)) | → | U52#(isList(V2)) |
| active#(U51(X1, X2)) | → | active#(X1) | | active#(isList(__(V1, V2))) | → | isList#(V1) |
| active#(__(__(X, Y), Z)) | → | __#(X, __(Y, Z)) | | proper#(U52(X)) | → | U52#(proper(X)) |
| U51#(mark(X1), X2) | → | U51#(X1, X2) | | proper#(U42(X)) | → | U42#(proper(X)) |
| active#(U31(X)) | → | U31#(active(X)) | | active#(U42(X)) | → | U42#(active(X)) |
| active#(isPal(V)) | → | U81#(isNePal(V)) | | top#(mark(X)) | → | proper#(X) |
| active#(__(X1, X2)) | → | __#(active(X1), X2) | | active#(U41(tt, V2)) | → | U42#(isNeList(V2)) |
| __#(mark(X1), X2) | → | __#(X1, X2) | | active#(U41(tt, V2)) | → | isNeList#(V2) |
| U81#(mark(X)) | → | U81#(X) | | active#(U11(X)) | → | U11#(active(X)) |
| proper#(U71(X1, X2)) | → | U71#(proper(X1), proper(X2)) | | active#(isNeList(V)) | → | U31#(isQid(V)) |
| active#(U41(X1, X2)) | → | active#(X1) | | proper#(isNePal(X)) | → | isNePal#(proper(X)) |
| isQid#(ok(X)) | → | isQid#(X) | | proper#(U22(X)) | → | proper#(X) |
| active#(isList(__(V1, V2))) | → | U21#(isList(V1), V2) | | active#(isNeList(__(V1, V2))) | → | isNeList#(V1) |
| U72#(ok(X)) | → | U72#(X) | | active#(isNeList(__(V1, V2))) | → | isList#(V1) |
| proper#(U11(X)) | → | proper#(X) | | top#(ok(X)) | → | active#(X) |
| active#(isPal(V)) | → | isNePal#(V) | | active#(__(X1, X2)) | → | active#(X2) |
| isList#(ok(X)) | → | isList#(X) | | U71#(mark(X1), X2) | → | U71#(X1, X2) |
| active#(U52(X)) | → | active#(X) | | proper#(U72(X)) | → | proper#(X) |
| proper#(isList(X)) | → | isList#(proper(X)) | | proper#(U51(X1, X2)) | → | proper#(X2) |
| isNeList#(ok(X)) | → | isNeList#(X) | | U42#(ok(X)) | → | U42#(X) |
| U11#(mark(X)) | → | U11#(X) | | active#(isNeList(__(V1, V2))) | → | U51#(isNeList(V1), V2) |
| active#(U21(X1, X2)) | → | U21#(active(X1), X2) | | proper#(U81(X)) | → | U81#(proper(X)) |
| U51#(ok(X1), ok(X2)) | → | U51#(X1, X2) | | active#(U52(X)) | → | U52#(active(X)) |
| U61#(mark(X)) | → | U61#(X) | | __#(ok(X1), ok(X2)) | → | __#(X1, X2) |
| proper#(U22(X)) | → | U22#(proper(X)) | | active#(__(__(X, Y), Z)) | → | __#(Y, Z) |
| __#(X1, mark(X2)) | → | __#(X1, X2) | | U31#(ok(X)) | → | U31#(X) |
| proper#(U21(X1, X2)) | → | proper#(X1) | | U81#(ok(X)) | → | U81#(X) |
| active#(isNePal(__(I, __(P, I)))) | → | U71#(isQid(I), P) | | active#(U72(X)) | → | active#(X) |
| top#(ok(X)) | → | top#(active(X)) | | U61#(ok(X)) | → | U61#(X) |
| isPal#(ok(X)) | → | isPal#(X) | | active#(U71(tt, P)) | → | U72#(isPal(P)) |
| active#(U21(tt, V2)) | → | U22#(isList(V2)) | | proper#(isList(X)) | → | proper#(X) |
| active#(U81(X)) | → | U81#(active(X)) | | U71#(ok(X1), ok(X2)) | → | U71#(X1, X2) |
| proper#(U71(X1, X2)) | → | proper#(X2) | | U42#(mark(X)) | → | U42#(X) |
| proper#(U51(X1, X2)) | → | U51#(proper(X1), proper(X2)) | | active#(U41(X1, X2)) | → | U41#(active(X1), X2) |
| proper#(isPal(X)) | → | proper#(X) | | active#(U51(X1, X2)) | → | U51#(active(X1), X2) |
| U22#(mark(X)) | → | U22#(X) | | proper#(__(X1, X2)) | → | proper#(X1) |
| top#(mark(X)) | → | top#(proper(X)) | | active#(U31(X)) | → | active#(X) |
| active#(isNePal(V)) | → | isQid#(V) | | U22#(ok(X)) | → | U22#(X) |
| proper#(isNePal(X)) | → | proper#(X) | | active#(U61(X)) | → | U61#(active(X)) |
| proper#(isNeList(X)) | → | proper#(X) | | U52#(ok(X)) | → | U52#(X) |
| active#(U81(X)) | → | active#(X) | | isNePal#(ok(X)) | → | isNePal#(X) |
| active#(U72(X)) | → | U72#(active(X)) | | U72#(mark(X)) | → | U72#(X) |
| active#(isNePal(V)) | → | U61#(isQid(V)) | | active#(U21(tt, V2)) | → | isList#(V2) |
| proper#(isQid(X)) | → | proper#(X) | | proper#(U72(X)) | → | U72#(proper(X)) |
| U31#(mark(X)) | → | U31#(X) | | active#(U71(X1, X2)) | → | U71#(active(X1), X2) |
| proper#(isPal(X)) | → | isPal#(proper(X)) | | active#(U11(X)) | → | active#(X) |
| active#(U42(X)) | → | active#(X) | | proper#(U31(X)) | → | U31#(proper(X)) |
| proper#(U61(X)) | → | U61#(proper(X)) | | proper#(U51(X1, X2)) | → | proper#(X1) |
| proper#(U42(X)) | → | proper#(X) | | proper#(U21(X1, X2)) | → | proper#(X2) |
| active#(isNeList(V)) | → | isQid#(V) | | proper#(__(X1, X2)) | → | __#(proper(X1), proper(X2)) |
| U41#(ok(X1), ok(X2)) | → | U41#(X1, X2) | | proper#(U71(X1, X2)) | → | proper#(X1) |
| active#(U22(X)) | → | U22#(active(X)) | | proper#(U11(X)) | → | U11#(proper(X)) |
| active#(__(X1, X2)) | → | __#(X1, active(X2)) | | U41#(mark(X1), X2) | → | U41#(X1, X2) |
| active#(isNeList(__(V1, V2))) | → | U41#(isList(V1), V2) | | active#(U71(X1, X2)) | → | active#(X1) |
| proper#(isQid(X)) | → | isQid#(proper(X)) | | proper#(U21(X1, X2)) | → | U21#(proper(X1), proper(X2)) |
| active#(__(X1, X2)) | → | active#(X1) | | proper#(U61(X)) | → | proper#(X) |
| active#(isList(V)) | → | U11#(isNeList(V)) | | active#(isList(V)) | → | isNeList#(V) |
| active#(isNePal(__(I, __(P, I)))) | → | isQid#(I) | | proper#(__(X1, X2)) | → | proper#(X2) |
| proper#(U81(X)) | → | proper#(X) | | proper#(U41(X1, X2)) | → | U41#(proper(X1), proper(X2)) |
| active#(U51(tt, V2)) | → | isList#(V2) | | proper#(isNeList(X)) | → | isNeList#(proper(X)) |
| active#(U21(X1, X2)) | → | active#(X1) | | active#(U22(X)) | → | active#(X) |
| U21#(mark(X1), X2) | → | U21#(X1, X2) | | U52#(mark(X)) | → | U52#(X) |
| U11#(ok(X)) | → | U11#(X) | | active#(U61(X)) | → | active#(X) |
| proper#(U52(X)) | → | proper#(X) | | U21#(ok(X1), ok(X2)) | → | U21#(X1, X2) |
| proper#(U31(X)) | → | proper#(X) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
The following SCCs where found
| active#(U11(X)) → active#(X) | active#(__(X1, X2)) → active#(X1) |
| active#(U42(X)) → active#(X) | active#(U72(X)) → active#(X) |
| active#(U31(X)) → active#(X) | active#(U51(X1, X2)) → active#(X1) |
| active#(U81(X)) → active#(X) | active#(U41(X1, X2)) → active#(X1) |
| active#(U21(X1, X2)) → active#(X1) | active#(U22(X)) → active#(X) |
| active#(__(X1, X2)) → active#(X2) | active#(U52(X)) → active#(X) |
| active#(U61(X)) → active#(X) | active#(U71(X1, X2)) → active#(X1) |
| U81#(mark(X)) → U81#(X) | U81#(ok(X)) → U81#(X) |
| U41#(ok(X1), ok(X2)) → U41#(X1, X2) | U41#(mark(X1), X2) → U41#(X1, X2) |
| U42#(mark(X)) → U42#(X) | U42#(ok(X)) → U42#(X) |
| isPal#(ok(X)) → isPal#(X) |
| U31#(ok(X)) → U31#(X) | U31#(mark(X)) → U31#(X) |
| U71#(mark(X1), X2) → U71#(X1, X2) | U71#(ok(X1), ok(X2)) → U71#(X1, X2) |
| U72#(mark(X)) → U72#(X) | U72#(ok(X)) → U72#(X) |
| U61#(mark(X)) → U61#(X) | U61#(ok(X)) → U61#(X) |
| isNePal#(ok(X)) → isNePal#(X) |
| proper#(__(X1, X2)) → proper#(X1) | proper#(U41(X1, X2)) → proper#(X2) |
| proper#(U41(X1, X2)) → proper#(X1) | proper#(U61(X)) → proper#(X) |
| proper#(isNePal(X)) → proper#(X) | proper#(isList(X)) → proper#(X) |
| proper#(U11(X)) → proper#(X) | proper#(isNeList(X)) → proper#(X) |
| proper#(__(X1, X2)) → proper#(X2) | proper#(U81(X)) → proper#(X) |
| proper#(U51(X1, X2)) → proper#(X1) | proper#(U42(X)) → proper#(X) |
| proper#(U71(X1, X2)) → proper#(X2) | proper#(U21(X1, X2)) → proper#(X2) |
| proper#(isPal(X)) → proper#(X) | proper#(U71(X1, X2)) → proper#(X1) |
| proper#(isQid(X)) → proper#(X) | proper#(U72(X)) → proper#(X) |
| proper#(U21(X1, X2)) → proper#(X1) | proper#(U51(X1, X2)) → proper#(X2) |
| proper#(U22(X)) → proper#(X) | proper#(U52(X)) → proper#(X) |
| proper#(U31(X)) → proper#(X) |
| U21#(mark(X1), X2) → U21#(X1, X2) | U21#(ok(X1), ok(X2)) → U21#(X1, X2) |
| U11#(ok(X)) → U11#(X) | U11#(mark(X)) → U11#(X) |
| isQid#(ok(X)) → isQid#(X) |
| U52#(mark(X)) → U52#(X) | U52#(ok(X)) → U52#(X) |
| isList#(ok(X)) → isList#(X) |
| __#(mark(X1), X2) → __#(X1, X2) | __#(ok(X1), ok(X2)) → __#(X1, X2) |
| __#(X1, mark(X2)) → __#(X1, X2) |
| active#(U11(X)) → active#(X) | active#(U42(X)) → active#(X) |
| active#(__(X1, X2)) → active#(X1) | active#(U72(X)) → active#(X) |
| active#(U31(X)) → active#(X) | active#(U51(X1, X2)) → active#(X1) |
| active#(isNeList(V)) → U31#(isQid(V)) | active#(U81(X)) → active#(X) |
| active#(U41(X1, X2)) → active#(X1) | active#(U21(X1, X2)) → active#(X1) |
| active#(U22(X)) → active#(X) | active#(__(X1, X2)) → active#(X2) |
| active#(U52(X)) → active#(X) | active#(__(X1, X2)) → __#(X1, active(X2)) |
| active#(U61(X)) → active#(X) | active#(U71(X1, X2)) → active#(X1) |
| isNeList#(ok(X)) → isNeList#(X) |
| U22#(ok(X)) → U22#(X) | U22#(mark(X)) → U22#(X) |
| top#(mark(X)) → top#(proper(X)) | top#(ok(X)) → top#(active(X)) |
| U51#(ok(X1), ok(X2)) → U51#(X1, X2) | U51#(mark(X1), X2) → U51#(X1, X2) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| U81#(mark(X)) | → | U81#(X) | | U81#(ok(X)) | → | U81#(X) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| U81#(mark(X)) | → | U81#(X) | | U81#(ok(X)) | → | U81#(X) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| U41#(ok(X1), ok(X2)) | → | U41#(X1, X2) | | U41#(mark(X1), X2) | → | U41#(X1, X2) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| U41#(ok(X1), ok(X2)) | → | U41#(X1, X2) | | U41#(mark(X1), X2) | → | U41#(X1, X2) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| U42#(mark(X)) | → | U42#(X) | | U42#(ok(X)) | → | U42#(X) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| U42#(mark(X)) | → | U42#(X) | | U42#(ok(X)) | → | U42#(X) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| isNeList#(ok(X)) | → | isNeList#(X) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| isNeList#(ok(X)) | → | isNeList#(X) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| U52#(mark(X)) | → | U52#(X) | | U52#(ok(X)) | → | U52#(X) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| U52#(mark(X)) | → | U52#(X) | | U52#(ok(X)) | → | U52#(X) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| U61#(mark(X)) | → | U61#(X) | | U61#(ok(X)) | → | U61#(X) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| U61#(mark(X)) | → | U61#(X) | | U61#(ok(X)) | → | U61#(X) |
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| U22#(ok(X)) | → | U22#(X) | | U22#(mark(X)) | → | U22#(X) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| U22#(ok(X)) | → | U22#(X) | | U22#(mark(X)) | → | U22#(X) |
Problem 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| U72#(mark(X)) | → | U72#(X) | | U72#(ok(X)) | → | U72#(X) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| U72#(mark(X)) | → | U72#(X) | | U72#(ok(X)) | → | U72#(X) |
Problem 10: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| U71#(mark(X1), X2) | → | U71#(X1, X2) | | U71#(ok(X1), ok(X2)) | → | U71#(X1, X2) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| U71#(mark(X1), X2) | → | U71#(X1, X2) | | U71#(ok(X1), ok(X2)) | → | U71#(X1, X2) |
Problem 11: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| active#(U11(X)) | → | active#(X) | | active#(U31(X)) | → | active#(X) |
| active#(U72(X)) | → | active#(X) | | active#(U42(X)) | → | active#(X) |
| active#(__(X1, X2)) | → | active#(X1) | | active#(U51(X1, X2)) | → | active#(X1) |
| active#(U81(X)) | → | active#(X) | | active#(U21(X1, X2)) | → | active#(X1) |
| active#(U41(X1, X2)) | → | active#(X1) | | active#(U22(X)) | → | active#(X) |
| active#(__(X1, X2)) | → | active#(X2) | | active#(U52(X)) | → | active#(X) |
| active#(U61(X)) | → | active#(X) | | active#(U71(X1, X2)) | → | active#(X1) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| active#(U11(X)) | → | active#(X) | | active#(U72(X)) | → | active#(X) |
| active#(__(X1, X2)) | → | active#(X1) | | active#(U42(X)) | → | active#(X) |
| active#(U31(X)) | → | active#(X) | | active#(U51(X1, X2)) | → | active#(X1) |
| active#(U81(X)) | → | active#(X) | | active#(U41(X1, X2)) | → | active#(X1) |
| active#(U21(X1, X2)) | → | active#(X1) | | active#(U22(X)) | → | active#(X) |
| active#(__(X1, X2)) | → | active#(X2) | | active#(U52(X)) | → | active#(X) |
| active#(U61(X)) | → | active#(X) | | active#(U71(X1, X2)) | → | active#(X1) |
Problem 12: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| active#(U11(X)) | → | active#(X) | | active#(U31(X)) | → | active#(X) |
| active#(U72(X)) | → | active#(X) | | active#(__(X1, X2)) | → | active#(X1) |
| active#(U42(X)) | → | active#(X) | | active#(U51(X1, X2)) | → | active#(X1) |
| active#(isNeList(V)) | → | U31#(isQid(V)) | | active#(U81(X)) | → | active#(X) |
| active#(U21(X1, X2)) | → | active#(X1) | | active#(U41(X1, X2)) | → | active#(X1) |
| active#(U22(X)) | → | active#(X) | | active#(__(X1, X2)) | → | active#(X2) |
| active#(U52(X)) | → | active#(X) | | active#(__(X1, X2)) | → | __#(X1, active(X2)) |
| active#(U61(X)) | → | active#(X) | | active#(U71(X1, X2)) | → | active#(X1) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
The following SCCs where found
| active#(U11(X)) → active#(X) | active#(U31(X)) → active#(X) |
| active#(U42(X)) → active#(X) | active#(__(X1, X2)) → active#(X1) |
| active#(U72(X)) → active#(X) | active#(U51(X1, X2)) → active#(X1) |
| active#(U81(X)) → active#(X) | active#(U41(X1, X2)) → active#(X1) |
| active#(U21(X1, X2)) → active#(X1) | active#(U22(X)) → active#(X) |
| active#(__(X1, X2)) → active#(X2) | active#(U52(X)) → active#(X) |
| active#(U61(X)) → active#(X) | active#(U71(X1, X2)) → active#(X1) |
Problem 25: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| active#(U11(X)) | → | active#(X) | | active#(U72(X)) | → | active#(X) |
| active#(__(X1, X2)) | → | active#(X1) | | active#(U42(X)) | → | active#(X) |
| active#(U31(X)) | → | active#(X) | | active#(U51(X1, X2)) | → | active#(X1) |
| active#(U81(X)) | → | active#(X) | | active#(U21(X1, X2)) | → | active#(X1) |
| active#(U41(X1, X2)) | → | active#(X1) | | active#(U22(X)) | → | active#(X) |
| active#(__(X1, X2)) | → | active#(X2) | | active#(U52(X)) | → | active#(X) |
| active#(U61(X)) | → | active#(X) | | active#(U71(X1, X2)) | → | active#(X1) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| active#(U11(X)) | → | active#(X) | | active#(__(X1, X2)) | → | active#(X1) |
| active#(U31(X)) | → | active#(X) | | active#(U42(X)) | → | active#(X) |
| active#(U72(X)) | → | active#(X) | | active#(U51(X1, X2)) | → | active#(X1) |
| active#(U81(X)) | → | active#(X) | | active#(U41(X1, X2)) | → | active#(X1) |
| active#(U21(X1, X2)) | → | active#(X1) | | active#(U22(X)) | → | active#(X) |
| active#(__(X1, X2)) | → | active#(X2) | | active#(U52(X)) | → | active#(X) |
| active#(U61(X)) | → | active#(X) | | active#(U71(X1, X2)) | → | active#(X1) |
Problem 13: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| U51#(ok(X1), ok(X2)) | → | U51#(X1, X2) | | U51#(mark(X1), X2) | → | U51#(X1, X2) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| U51#(mark(X1), X2) | → | U51#(X1, X2) | | U51#(ok(X1), ok(X2)) | → | U51#(X1, X2) |
Problem 14: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| U31#(ok(X)) | → | U31#(X) | | U31#(mark(X)) | → | U31#(X) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| U31#(ok(X)) | → | U31#(X) | | U31#(mark(X)) | → | U31#(X) |
Problem 15: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| U11#(ok(X)) | → | U11#(X) | | U11#(mark(X)) | → | U11#(X) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| U11#(ok(X)) | → | U11#(X) | | U11#(mark(X)) | → | U11#(X) |
Problem 16: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| isNePal#(ok(X)) | → | isNePal#(X) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| isNePal#(ok(X)) | → | isNePal#(X) |
Problem 17: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| U21#(mark(X1), X2) | → | U21#(X1, X2) | | U21#(ok(X1), ok(X2)) | → | U21#(X1, X2) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| U21#(mark(X1), X2) | → | U21#(X1, X2) | | U21#(ok(X1), ok(X2)) | → | U21#(X1, X2) |
Problem 18: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| isPal#(ok(X)) | → | isPal#(X) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| isPal#(ok(X)) | → | isPal#(X) |
Problem 19: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| isList#(ok(X)) | → | isList#(X) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| isList#(ok(X)) | → | isList#(X) |
Problem 20: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| isQid#(ok(X)) | → | isQid#(X) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| isQid#(ok(X)) | → | isQid#(X) |
Problem 21: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| top#(mark(X)) | → | top#(proper(X)) | | top#(ok(X)) | → | top#(active(X)) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Function Precedence
ok < top# < proper = i = u = nil < e < a = isQid < __ = U71 < isList = U21 = o = isPal = U72 = U51 < isNeList = U41 = isNePal = U22 = active < U61 = U42 = top = mark = tt = U81 = U52 = U11 = U31
Argument Filtering
isList: 1
isNeList: 1
__: 1 2
U61: 1
U42: 1
U41: 1 2
isNePal: 1
ok: collapses to 1
proper: collapses to 1
U21: 1 2
U22: 1
top: all arguments are removed from top
e: all arguments are removed from e
a: all arguments are removed from a
o: all arguments are removed from o
mark: 1
isPal: 1
i: all arguments are removed from i
U71: 1 2
U72: 1
u: all arguments are removed from u
U51: 1 2
tt: all arguments are removed from tt
U81: 1
U52: 1
active: collapses to 1
U11: 1
isQid: collapses to 1
U31: 1
top#: collapses to 1
nil: all arguments are removed from nil
Status
isList: multiset
isNeList: multiset
__: lexicographic with permutation 1 → 1 2 → 2
U61: lexicographic with permutation 1 → 1
U42: lexicographic with permutation 1 → 1
U41: multiset
isNePal: lexicographic with permutation 1 → 1
U21: multiset
U22: lexicographic with permutation 1 → 1
top: multiset
e: multiset
a: multiset
o: multiset
mark: lexicographic with permutation 1 → 1
isPal: lexicographic with permutation 1 → 1
i: multiset
U71: lexicographic with permutation 1 → 1 2 → 2
U72: lexicographic with permutation 1 → 1
u: multiset
U51: multiset
tt: multiset
U81: lexicographic with permutation 1 → 1
U52: lexicographic with permutation 1 → 1
U11: lexicographic with permutation 1 → 1
U31: lexicographic with permutation 1 → 1
nil: multiset
Usable Rules
| active(__(X1, X2)) → __(active(X1), X2) | active(U61(tt)) → mark(tt) |
| U21(ok(X1), ok(X2)) → ok(U21(X1, X2)) | proper(i) → ok(i) |
| active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z))) | proper(a) → ok(a) |
| U21(mark(X1), X2) → mark(U21(X1, X2)) | isPal(ok(X)) → ok(isPal(X)) |
| U31(ok(X)) → ok(U31(X)) | proper(U71(X1, X2)) → U71(proper(X1), proper(X2)) |
| proper(U31(X)) → U31(proper(X)) | active(isQid(u)) → mark(tt) |
| proper(isList(X)) → isList(proper(X)) | active(U72(tt)) → mark(tt) |
| U22(mark(X)) → mark(U22(X)) | active(U51(X1, X2)) → U51(active(X1), X2) |
| proper(isNePal(X)) → isNePal(proper(X)) | active(U81(X)) → U81(active(X)) |
| active(U22(X)) → U22(active(X)) | proper(U11(X)) → U11(proper(X)) |
| U42(mark(X)) → mark(U42(X)) | U41(ok(X1), ok(X2)) → ok(U41(X1, X2)) |
| proper(nil) → ok(nil) | active(isList(__(V1, V2))) → mark(U21(isList(V1), V2)) |
| U72(mark(X)) → mark(U72(X)) | active(U42(tt)) → mark(tt) |
| active(isNeList(__(V1, V2))) → mark(U51(isNeList(V1), V2)) | active(isNePal(__(I, __(P, I)))) → mark(U71(isQid(I), P)) |
| active(U72(X)) → U72(active(X)) | active(U31(X)) → U31(active(X)) |
| active(U22(tt)) → mark(tt) | isQid(ok(X)) → ok(isQid(X)) |
| active(U41(tt, V2)) → mark(U42(isNeList(V2))) | U31(mark(X)) → mark(U31(X)) |
| active(U11(tt)) → mark(tt) | proper(e) → ok(e) |
| U72(ok(X)) → ok(U72(X)) | active(isQid(i)) → mark(tt) |
| active(U61(X)) → U61(active(X)) | proper(U21(X1, X2)) → U21(proper(X1), proper(X2)) |
| active(U21(X1, X2)) → U21(active(X1), X2) | active(isQid(e)) → mark(tt) |
| isNeList(ok(X)) → ok(isNeList(X)) | proper(__(X1, X2)) → __(proper(X1), proper(X2)) |
| active(U52(X)) → U52(active(X)) | active(isNePal(V)) → mark(U61(isQid(V))) |
| U61(mark(X)) → mark(U61(X)) | active(isList(nil)) → mark(tt) |
| active(isList(V)) → mark(U11(isNeList(V))) | U61(ok(X)) → ok(U61(X)) |
| proper(U42(X)) → U42(proper(X)) | proper(U52(X)) → U52(proper(X)) |
| U81(ok(X)) → ok(U81(X)) | U71(mark(X1), X2) → mark(U71(X1, X2)) |
| U71(ok(X1), ok(X2)) → ok(U71(X1, X2)) | active(isQid(a)) → mark(tt) |
| active(U51(tt, V2)) → mark(U52(isList(V2))) | active(__(X, nil)) → mark(X) |
| active(isQid(o)) → mark(tt) | active(U71(tt, P)) → mark(U72(isPal(P))) |
| active(isPal(V)) → mark(U81(isNePal(V))) | isNePal(ok(X)) → ok(isNePal(X)) |
| proper(isPal(X)) → isPal(proper(X)) | __(ok(X1), ok(X2)) → ok(__(X1, X2)) |
| proper(o) → ok(o) | U11(ok(X)) → ok(U11(X)) |
| active(U81(tt)) → mark(tt) | proper(tt) → ok(tt) |
| active(isPal(nil)) → mark(tt) | U22(ok(X)) → ok(U22(X)) |
| U51(ok(X1), ok(X2)) → ok(U51(X1, X2)) | active(U11(X)) → U11(active(X)) |
| active(U42(X)) → U42(active(X)) | active(U31(tt)) → mark(tt) |
| proper(isQid(X)) → isQid(proper(X)) | active(__(X1, X2)) → __(X1, active(X2)) |
| active(U52(tt)) → mark(tt) | __(X1, mark(X2)) → mark(__(X1, X2)) |
| active(U41(X1, X2)) → U41(active(X1), X2) | U11(mark(X)) → mark(U11(X)) |
| __(mark(X1), X2) → mark(__(X1, X2)) | proper(U72(X)) → U72(proper(X)) |
| U52(mark(X)) → mark(U52(X)) | U81(mark(X)) → mark(U81(X)) |
| active(isNeList(V)) → mark(U31(isQid(V))) | active(__(nil, X)) → mark(X) |
| U51(mark(X1), X2) → mark(U51(X1, X2)) | proper(U61(X)) → U61(proper(X)) |
| proper(U41(X1, X2)) → U41(proper(X1), proper(X2)) | isList(ok(X)) → ok(isList(X)) |
| proper(u) → ok(u) | U41(mark(X1), X2) → mark(U41(X1, X2)) |
| proper(U51(X1, X2)) → U51(proper(X1), proper(X2)) | proper(U81(X)) → U81(proper(X)) |
| active(U21(tt, V2)) → mark(U22(isList(V2))) | active(U71(X1, X2)) → U71(active(X1), X2) |
| U52(ok(X)) → ok(U52(X)) | proper(U22(X)) → U22(proper(X)) |
| proper(isNeList(X)) → isNeList(proper(X)) | U42(ok(X)) → ok(U42(X)) |
| active(isNeList(__(V1, V2))) → mark(U41(isList(V1), V2)) |
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.
| top#(mark(X)) → top#(proper(X)) |
Problem 26: ReductionPairSAT
Dependency Pair Problem
Dependency Pairs
| top#(ok(X)) | → | top#(active(X)) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, top, U22, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, U11, active, U31, isQid, nil
Strategy
Function Precedence
e = o = i < U72 < u < a = nil < U11 < isNePal < U52 < U21 < isNeList < U61 = isQid < mark < __ = U41 = U81 = active < top# < U31 < U22 < U51 < isList = U42 = ok = proper = top = isPal = U71 = tt
Argument Filtering
isList: collapses to 1
isNeList: collapses to 1
__: 1 2
U61: collapses to 1
U42: collapses to 1
U41: 1 2
isNePal: collapses to 1
ok: 1
proper: all arguments are removed from proper
U21: collapses to 2
U22: collapses to 1
top: 1
e: all arguments are removed from e
a: all arguments are removed from a
o: all arguments are removed from o
mark: collapses to 1
isPal: collapses to 1
i: all arguments are removed from i
U71: collapses to 2
U72: collapses to 1
u: all arguments are removed from u
U51: collapses to 2
tt: all arguments are removed from tt
U81: collapses to 1
U52: collapses to 1
active: collapses to 1
U11: collapses to 1
isQid: collapses to 1
U31: collapses to 1
top#: 1
nil: all arguments are removed from nil
Status
__: lexicographic with permutation 1 → 1 2 → 2
U41: lexicographic with permutation 1 → 1 2 → 2
ok: lexicographic with permutation 1 → 1
proper: multiset
top: lexicographic with permutation 1 → 1
e: multiset
a: multiset
o: multiset
i: multiset
u: multiset
tt: multiset
top#: multiset
nil: multiset
Usable Rules
| active(__(X1, X2)) → __(active(X1), X2) | active(U61(tt)) → mark(tt) |
| U71(ok(X1), ok(X2)) → ok(U71(X1, X2)) | active(isQid(a)) → mark(tt) |
| active(__(X, nil)) → mark(X) | active(U51(tt, V2)) → mark(U52(isList(V2))) |
| U21(ok(X1), ok(X2)) → ok(U21(X1, X2)) | active(isQid(o)) → mark(tt) |
| active(U71(tt, P)) → mark(U72(isPal(P))) | active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z))) |
| active(isPal(V)) → mark(U81(isNePal(V))) | isNePal(ok(X)) → ok(isNePal(X)) |
| U21(mark(X1), X2) → mark(U21(X1, X2)) | U31(ok(X)) → ok(U31(X)) |
| isPal(ok(X)) → ok(isPal(X)) | __(ok(X1), ok(X2)) → ok(__(X1, X2)) |
| U11(ok(X)) → ok(U11(X)) | active(isQid(u)) → mark(tt) |
| active(U81(tt)) → mark(tt) | U22(ok(X)) → ok(U22(X)) |
| active(isPal(nil)) → mark(tt) | U22(mark(X)) → mark(U22(X)) |
| active(U72(tt)) → mark(tt) | U51(ok(X1), ok(X2)) → ok(U51(X1, X2)) |
| active(U11(X)) → U11(active(X)) | active(U51(X1, X2)) → U51(active(X1), X2) |
| active(U42(X)) → U42(active(X)) | active(U81(X)) → U81(active(X)) |
| active(U22(X)) → U22(active(X)) | U42(mark(X)) → mark(U42(X)) |
| active(U31(tt)) → mark(tt) | U41(ok(X1), ok(X2)) → ok(U41(X1, X2)) |
| active(isList(__(V1, V2))) → mark(U21(isList(V1), V2)) | active(U52(tt)) → mark(tt) |
| active(__(X1, X2)) → __(X1, active(X2)) | U72(mark(X)) → mark(U72(X)) |
| __(X1, mark(X2)) → mark(__(X1, X2)) | active(U42(tt)) → mark(tt) |
| active(isNeList(__(V1, V2))) → mark(U51(isNeList(V1), V2)) | active(isNePal(__(I, __(P, I)))) → mark(U71(isQid(I), P)) |
| active(U72(X)) → U72(active(X)) | active(U31(X)) → U31(active(X)) |
| active(U41(X1, X2)) → U41(active(X1), X2) | U11(mark(X)) → mark(U11(X)) |
| active(U22(tt)) → mark(tt) | __(mark(X1), X2) → mark(__(X1, X2)) |
| isQid(ok(X)) → ok(isQid(X)) | U52(mark(X)) → mark(U52(X)) |
| U31(mark(X)) → mark(U31(X)) | active(U41(tt, V2)) → mark(U42(isNeList(V2))) |
| U72(ok(X)) → ok(U72(X)) | active(U11(tt)) → mark(tt) |
| U81(mark(X)) → mark(U81(X)) | active(isQid(i)) → mark(tt) |
| active(isNeList(V)) → mark(U31(isQid(V))) | active(U61(X)) → U61(active(X)) |
| active(isQid(e)) → mark(tt) | active(U21(X1, X2)) → U21(active(X1), X2) |
| isNeList(ok(X)) → ok(isNeList(X)) | active(__(nil, X)) → mark(X) |
| U51(mark(X1), X2) → mark(U51(X1, X2)) | active(isNePal(V)) → mark(U61(isQid(V))) |
| active(U52(X)) → U52(active(X)) | U61(mark(X)) → mark(U61(X)) |
| isList(ok(X)) → ok(isList(X)) | active(isList(nil)) → mark(tt) |
| U41(mark(X1), X2) → mark(U41(X1, X2)) | U61(ok(X)) → ok(U61(X)) |
| active(isList(V)) → mark(U11(isNeList(V))) | active(U21(tt, V2)) → mark(U22(isList(V2))) |
| active(U71(X1, X2)) → U71(active(X1), X2) | U52(ok(X)) → ok(U52(X)) |
| U81(ok(X)) → ok(U81(X)) | U71(mark(X1), X2) → mark(U71(X1, X2)) |
| U42(ok(X)) → ok(U42(X)) | active(isNeList(__(V1, V2))) → mark(U41(isList(V1), V2)) |
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.
| top#(ok(X)) → top#(active(X)) |
Problem 22: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| __#(mark(X1), X2) | → | __#(X1, X2) | | __#(ok(X1), ok(X2)) | → | __#(X1, X2) |
| __#(X1, mark(X2)) | → | __#(X1, X2) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| __#(mark(X1), X2) | → | __#(X1, X2) | | __#(ok(X1), ok(X2)) | → | __#(X1, X2) |
Problem 24: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| __#(X1, mark(X2)) | → | __#(X1, X2) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, top, U22, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, U11, active, U31, isQid, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| __#(X1, mark(X2)) | → | __#(X1, X2) |
Problem 23: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| proper#(__(X1, X2)) | → | proper#(X1) | | proper#(U41(X1, X2)) | → | proper#(X2) |
| proper#(U41(X1, X2)) | → | proper#(X1) | | proper#(U61(X)) | → | proper#(X) |
| proper#(isList(X)) | → | proper#(X) | | proper#(isNePal(X)) | → | proper#(X) |
| proper#(isNeList(X)) | → | proper#(X) | | proper#(U11(X)) | → | proper#(X) |
| proper#(__(X1, X2)) | → | proper#(X2) | | proper#(U81(X)) | → | proper#(X) |
| proper#(U42(X)) | → | proper#(X) | | proper#(U51(X1, X2)) | → | proper#(X1) |
| proper#(U71(X1, X2)) | → | proper#(X2) | | proper#(U21(X1, X2)) | → | proper#(X2) |
| proper#(isPal(X)) | → | proper#(X) | | proper#(U71(X1, X2)) | → | proper#(X1) |
| proper#(isQid(X)) | → | proper#(X) | | proper#(U72(X)) | → | proper#(X) |
| proper#(U21(X1, X2)) | → | proper#(X1) | | proper#(U51(X1, X2)) | → | proper#(X2) |
| proper#(U22(X)) | → | proper#(X) | | proper#(U52(X)) | → | proper#(X) |
| proper#(U31(X)) | → | proper#(X) |
Rewrite Rules
| active(__(__(X, Y), Z)) | → | mark(__(X, __(Y, Z))) | | active(__(X, nil)) | → | mark(X) |
| active(__(nil, X)) | → | mark(X) | | active(U11(tt)) | → | mark(tt) |
| active(U21(tt, V2)) | → | mark(U22(isList(V2))) | | active(U22(tt)) | → | mark(tt) |
| active(U31(tt)) | → | mark(tt) | | active(U41(tt, V2)) | → | mark(U42(isNeList(V2))) |
| active(U42(tt)) | → | mark(tt) | | active(U51(tt, V2)) | → | mark(U52(isList(V2))) |
| active(U52(tt)) | → | mark(tt) | | active(U61(tt)) | → | mark(tt) |
| active(U71(tt, P)) | → | mark(U72(isPal(P))) | | active(U72(tt)) | → | mark(tt) |
| active(U81(tt)) | → | mark(tt) | | active(isList(V)) | → | mark(U11(isNeList(V))) |
| active(isList(nil)) | → | mark(tt) | | active(isList(__(V1, V2))) | → | mark(U21(isList(V1), V2)) |
| active(isNeList(V)) | → | mark(U31(isQid(V))) | | active(isNeList(__(V1, V2))) | → | mark(U41(isList(V1), V2)) |
| active(isNeList(__(V1, V2))) | → | mark(U51(isNeList(V1), V2)) | | active(isNePal(V)) | → | mark(U61(isQid(V))) |
| active(isNePal(__(I, __(P, I)))) | → | mark(U71(isQid(I), P)) | | active(isPal(V)) | → | mark(U81(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) |
| active(__(X1, X2)) | → | __(active(X1), X2) | | active(__(X1, X2)) | → | __(X1, active(X2)) |
| active(U11(X)) | → | U11(active(X)) | | active(U21(X1, X2)) | → | U21(active(X1), X2) |
| active(U22(X)) | → | U22(active(X)) | | active(U31(X)) | → | U31(active(X)) |
| active(U41(X1, X2)) | → | U41(active(X1), X2) | | active(U42(X)) | → | U42(active(X)) |
| active(U51(X1, X2)) | → | U51(active(X1), X2) | | active(U52(X)) | → | U52(active(X)) |
| active(U61(X)) | → | U61(active(X)) | | active(U71(X1, X2)) | → | U71(active(X1), X2) |
| active(U72(X)) | → | U72(active(X)) | | active(U81(X)) | → | U81(active(X)) |
| __(mark(X1), X2) | → | mark(__(X1, X2)) | | __(X1, mark(X2)) | → | mark(__(X1, X2)) |
| U11(mark(X)) | → | mark(U11(X)) | | U21(mark(X1), X2) | → | mark(U21(X1, X2)) |
| U22(mark(X)) | → | mark(U22(X)) | | U31(mark(X)) | → | mark(U31(X)) |
| U41(mark(X1), X2) | → | mark(U41(X1, X2)) | | U42(mark(X)) | → | mark(U42(X)) |
| U51(mark(X1), X2) | → | mark(U51(X1, X2)) | | U52(mark(X)) | → | mark(U52(X)) |
| U61(mark(X)) | → | mark(U61(X)) | | U71(mark(X1), X2) | → | mark(U71(X1, X2)) |
| U72(mark(X)) | → | mark(U72(X)) | | U81(mark(X)) | → | mark(U81(X)) |
| proper(__(X1, X2)) | → | __(proper(X1), proper(X2)) | | proper(nil) | → | ok(nil) |
| proper(U11(X)) | → | U11(proper(X)) | | proper(tt) | → | ok(tt) |
| proper(U21(X1, X2)) | → | U21(proper(X1), proper(X2)) | | proper(U22(X)) | → | U22(proper(X)) |
| proper(isList(X)) | → | isList(proper(X)) | | proper(U31(X)) | → | U31(proper(X)) |
| proper(U41(X1, X2)) | → | U41(proper(X1), proper(X2)) | | proper(U42(X)) | → | U42(proper(X)) |
| proper(isNeList(X)) | → | isNeList(proper(X)) | | proper(U51(X1, X2)) | → | U51(proper(X1), proper(X2)) |
| proper(U52(X)) | → | U52(proper(X)) | | proper(U61(X)) | → | U61(proper(X)) |
| proper(U71(X1, X2)) | → | U71(proper(X1), proper(X2)) | | proper(U72(X)) | → | U72(proper(X)) |
| proper(isPal(X)) | → | isPal(proper(X)) | | proper(U81(X)) | → | U81(proper(X)) |
| proper(isQid(X)) | → | isQid(proper(X)) | | proper(isNePal(X)) | → | isNePal(proper(X)) |
| proper(a) | → | ok(a) | | proper(e) | → | ok(e) |
| proper(i) | → | ok(i) | | proper(o) | → | ok(o) |
| proper(u) | → | ok(u) | | __(ok(X1), ok(X2)) | → | ok(__(X1, X2)) |
| U11(ok(X)) | → | ok(U11(X)) | | U21(ok(X1), ok(X2)) | → | ok(U21(X1, X2)) |
| U22(ok(X)) | → | ok(U22(X)) | | isList(ok(X)) | → | ok(isList(X)) |
| U31(ok(X)) | → | ok(U31(X)) | | U41(ok(X1), ok(X2)) | → | ok(U41(X1, X2)) |
| U42(ok(X)) | → | ok(U42(X)) | | isNeList(ok(X)) | → | ok(isNeList(X)) |
| U51(ok(X1), ok(X2)) | → | ok(U51(X1, X2)) | | U52(ok(X)) | → | ok(U52(X)) |
| U61(ok(X)) | → | ok(U61(X)) | | U71(ok(X1), ok(X2)) | → | ok(U71(X1, X2)) |
| U72(ok(X)) | → | ok(U72(X)) | | isPal(ok(X)) | → | ok(isPal(X)) |
| U81(ok(X)) | → | ok(U81(X)) | | isQid(ok(X)) | → | ok(isQid(X)) |
| isNePal(ok(X)) | → | ok(isNePal(X)) | | top(mark(X)) | → | top(proper(X)) |
| top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: isList, isNeList, __, U61, U42, U41, isNePal, ok, proper, U21, U22, top, e, a, o, mark, isPal, U71, i, U72, u, U51, tt, U52, U81, active, U11, isQid, U31, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| proper#(__(X1, X2)) | → | proper#(X1) | | proper#(U41(X1, X2)) | → | proper#(X2) |
| proper#(U41(X1, X2)) | → | proper#(X1) | | proper#(U61(X)) | → | proper#(X) |
| proper#(isList(X)) | → | proper#(X) | | proper#(isNePal(X)) | → | proper#(X) |
| proper#(isNeList(X)) | → | proper#(X) | | proper#(U11(X)) | → | proper#(X) |
| proper#(__(X1, X2)) | → | proper#(X2) | | proper#(U81(X)) | → | proper#(X) |
| proper#(U51(X1, X2)) | → | proper#(X1) | | proper#(U42(X)) | → | proper#(X) |
| proper#(U71(X1, X2)) | → | proper#(X2) | | proper#(U21(X1, X2)) | → | proper#(X2) |
| proper#(isPal(X)) | → | proper#(X) | | proper#(U71(X1, X2)) | → | proper#(X1) |
| proper#(isQid(X)) | → | proper#(X) | | proper#(U72(X)) | → | proper#(X) |
| proper#(U21(X1, X2)) | → | proper#(X1) | | proper#(U51(X1, X2)) | → | proper#(X2) |
| proper#(U22(X)) | → | proper#(X) | | proper#(U52(X)) | → | proper#(X) |
| proper#(U31(X)) | → | proper#(X) |