YES

The TRS could be proven terminating. The proof took 19632 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (677ms).
 | – Problem 2 was processed with processor SubtermCriterion (3ms).
 | – Problem 3 was processed with processor SubtermCriterion (0ms).
 | – Problem 4 was processed with processor SubtermCriterion (1ms).
 | – Problem 5 was processed with processor SubtermCriterion (0ms).
 | – Problem 6 was processed with processor PolynomialOrderingProcessor (15601ms).
 |    | – Problem 13 was processed with processor PolynomialOrderingProcessor (1726ms).
 | – Problem 7 was processed with processor SubtermCriterion (0ms).
 | – Problem 8 was processed with processor SubtermCriterion (0ms).
 |    | – Problem 12 was processed with processor SubtermCriterion (0ms).
 | – Problem 9 was processed with processor SubtermCriterion (1ms).
 | – Problem 10 was processed with processor SubtermCriterion (0ms).
 | – Problem 11 was processed with processor SubtermCriterion (1ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

top#(ok(X))top#(active(X))active#(isList(__(V1, V2)))isList#(V1)
active#(__(__(X, Y), Z))__#(X, __(Y, Z))isPal#(ok(X))isPal#(X)
proper#(isList(X))proper#(X)proper#(and(X1, X2))and#(proper(X1), proper(X2))
proper#(and(X1, X2))proper#(X2)proper#(isPal(X))proper#(X)
top#(mark(X))proper#(X)active#(__(X1, X2))__#(active(X1), X2)
proper#(__(X1, X2))proper#(X1)__#(mark(X1), X2)__#(X1, X2)
top#(mark(X))top#(proper(X))active#(isNePal(V))isQid#(V)
proper#(isNePal(X))proper#(X)active#(isNePal(__(I, __(P, I))))and#(isQid(I), isPal(P))
proper#(isNeList(X))proper#(X)active#(isNeList(__(V1, V2)))isNeList#(V2)
and#(mark(X1), X2)and#(X1, X2)isNePal#(ok(X))isNePal#(X)
proper#(isNePal(X))isNePal#(proper(X))isQid#(ok(X))isQid#(X)
proper#(isQid(X))proper#(X)proper#(isPal(X))isPal#(proper(X))
active#(isNeList(__(V1, V2)))isNeList#(V1)active#(isNeList(__(V1, V2)))isList#(V1)
and#(ok(X1), ok(X2))and#(X1, X2)proper#(and(X1, X2))proper#(X1)
top#(ok(X))active#(X)active#(isNeList(V))isQid#(V)
active#(and(X1, X2))and#(active(X1), X2)proper#(__(X1, X2))__#(proper(X1), proper(X2))
active#(isPal(V))isNePal#(V)active#(__(X1, X2))active#(X2)
isList#(ok(X))isList#(X)active#(__(X1, X2))__#(X1, active(X2))
proper#(isList(X))isList#(proper(X))isNeList#(ok(X))isNeList#(X)
active#(isNePal(__(I, __(P, I))))isPal#(P)proper#(isQid(X))isQid#(proper(X))
active#(__(X1, X2))active#(X1)active#(isNeList(__(V1, V2)))isList#(V2)
__#(ok(X1), ok(X2))__#(X1, X2)active#(__(__(X, Y), Z))__#(Y, Z)
active#(isList(V))isNeList#(V)active#(isList(__(V1, V2)))and#(isList(V1), isList(V2))
__#(X1, mark(X2))__#(X1, X2)active#(isNePal(__(I, __(P, I))))isQid#(I)
proper#(__(X1, X2))proper#(X2)active#(isNeList(__(V1, V2)))and#(isList(V1), isNeList(V2))
proper#(isNeList(X))isNeList#(proper(X))active#(and(X1, X2))active#(X1)
active#(isNeList(__(V1, V2)))and#(isNeList(V1), isList(V2))active#(isList(__(V1, V2)))isList#(V2)

Rewrite Rules

active(__(__(X, Y), Z))mark(__(X, __(Y, Z)))active(__(X, nil))mark(X)
active(__(nil, X))mark(X)active(and(tt, X))mark(X)
active(isList(V))mark(isNeList(V))active(isList(nil))mark(tt)
active(isList(__(V1, V2)))mark(and(isList(V1), isList(V2)))active(isNeList(V))mark(isQid(V))
active(isNeList(__(V1, V2)))mark(and(isList(V1), isNeList(V2)))active(isNeList(__(V1, V2)))mark(and(isNeList(V1), isList(V2)))
active(isNePal(V))mark(isQid(V))active(isNePal(__(I, __(P, I))))mark(and(isQid(I), isPal(P)))
active(isPal(V))mark(isNePal(V))active(isPal(nil))mark(tt)
active(isQid(a))mark(tt)active(isQid(e))mark(tt)
active(isQid(i))mark(tt)active(isQid(o))mark(tt)
active(isQid(u))mark(tt)active(__(X1, X2))__(active(X1), X2)
active(__(X1, X2))__(X1, active(X2))active(and(X1, X2))and(active(X1), X2)
__(mark(X1), X2)mark(__(X1, X2))__(X1, mark(X2))mark(__(X1, X2))
and(mark(X1), X2)mark(and(X1, X2))proper(__(X1, X2))__(proper(X1), proper(X2))
proper(nil)ok(nil)proper(and(X1, X2))and(proper(X1), proper(X2))
proper(tt)ok(tt)proper(isList(X))isList(proper(X))
proper(isNeList(X))isNeList(proper(X))proper(isQid(X))isQid(proper(X))
proper(isNePal(X))isNePal(proper(X))proper(isPal(X))isPal(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))
and(ok(X1), ok(X2))ok(and(X1, X2))isList(ok(X))ok(isList(X))
isNeList(ok(X))ok(isNeList(X))isQid(ok(X))ok(isQid(X))
isNePal(ok(X))ok(isNePal(X))isPal(ok(X))ok(isPal(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, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, ok, isQid, proper, nil, top

Strategy


The following SCCs where found

isQid#(ok(X)) → isQid#(X)

isList#(ok(X)) → isList#(X)

__#(mark(X1), X2) → __#(X1, X2)__#(ok(X1), ok(X2)) → __#(X1, X2)
__#(X1, mark(X2)) → __#(X1, X2)

isPal#(ok(X)) → isPal#(X)

isNeList#(ok(X)) → isNeList#(X)

and#(ok(X1), ok(X2)) → and#(X1, X2)and#(mark(X1), X2) → and#(X1, X2)

isNePal#(ok(X)) → isNePal#(X)

active#(__(X1, X2)) → active#(X1)active#(__(X1, X2)) → active#(X2)
active#(and(X1, X2)) → active#(X1)

proper#(__(X1, X2)) → proper#(X1)proper#(isPal(X)) → proper#(X)
proper#(and(X1, X2)) → proper#(X2)proper#(isList(X)) → proper#(X)
proper#(isQid(X)) → proper#(X)proper#(isNePal(X)) → proper#(X)
proper#(isNeList(X)) → proper#(X)proper#(__(X1, X2)) → proper#(X2)
proper#(and(X1, X2)) → proper#(X1)

top#(mark(X)) → top#(proper(X))top#(ok(X)) → top#(active(X))

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

and#(ok(X1), ok(X2))and#(X1, X2)and#(mark(X1), X2)and#(X1, X2)

Rewrite Rules

active(__(__(X, Y), Z))mark(__(X, __(Y, Z)))active(__(X, nil))mark(X)
active(__(nil, X))mark(X)active(and(tt, X))mark(X)
active(isList(V))mark(isNeList(V))active(isList(nil))mark(tt)
active(isList(__(V1, V2)))mark(and(isList(V1), isList(V2)))active(isNeList(V))mark(isQid(V))
active(isNeList(__(V1, V2)))mark(and(isList(V1), isNeList(V2)))active(isNeList(__(V1, V2)))mark(and(isNeList(V1), isList(V2)))
active(isNePal(V))mark(isQid(V))active(isNePal(__(I, __(P, I))))mark(and(isQid(I), isPal(P)))
active(isPal(V))mark(isNePal(V))active(isPal(nil))mark(tt)
active(isQid(a))mark(tt)active(isQid(e))mark(tt)
active(isQid(i))mark(tt)active(isQid(o))mark(tt)
active(isQid(u))mark(tt)active(__(X1, X2))__(active(X1), X2)
active(__(X1, X2))__(X1, active(X2))active(and(X1, X2))and(active(X1), X2)
__(mark(X1), X2)mark(__(X1, X2))__(X1, mark(X2))mark(__(X1, X2))
and(mark(X1), X2)mark(and(X1, X2))proper(__(X1, X2))__(proper(X1), proper(X2))
proper(nil)ok(nil)proper(and(X1, X2))and(proper(X1), proper(X2))
proper(tt)ok(tt)proper(isList(X))isList(proper(X))
proper(isNeList(X))isNeList(proper(X))proper(isQid(X))isQid(proper(X))
proper(isNePal(X))isNePal(proper(X))proper(isPal(X))isPal(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))
and(ok(X1), ok(X2))ok(and(X1, X2))isList(ok(X))ok(isList(X))
isNeList(ok(X))ok(isNeList(X))isQid(ok(X))ok(isQid(X))
isNePal(ok(X))ok(isNePal(X))isPal(ok(X))ok(isPal(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, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, ok, isQid, proper, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

and#(ok(X1), ok(X2))and#(X1, X2)and#(mark(X1), X2)and#(X1, X2)

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

active#(__(X1, X2))active#(X1)active#(__(X1, X2))active#(X2)
active#(and(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(and(tt, X))mark(X)
active(isList(V))mark(isNeList(V))active(isList(nil))mark(tt)
active(isList(__(V1, V2)))mark(and(isList(V1), isList(V2)))active(isNeList(V))mark(isQid(V))
active(isNeList(__(V1, V2)))mark(and(isList(V1), isNeList(V2)))active(isNeList(__(V1, V2)))mark(and(isNeList(V1), isList(V2)))
active(isNePal(V))mark(isQid(V))active(isNePal(__(I, __(P, I))))mark(and(isQid(I), isPal(P)))
active(isPal(V))mark(isNePal(V))active(isPal(nil))mark(tt)
active(isQid(a))mark(tt)active(isQid(e))mark(tt)
active(isQid(i))mark(tt)active(isQid(o))mark(tt)
active(isQid(u))mark(tt)active(__(X1, X2))__(active(X1), X2)
active(__(X1, X2))__(X1, active(X2))active(and(X1, X2))and(active(X1), X2)
__(mark(X1), X2)mark(__(X1, X2))__(X1, mark(X2))mark(__(X1, X2))
and(mark(X1), X2)mark(and(X1, X2))proper(__(X1, X2))__(proper(X1), proper(X2))
proper(nil)ok(nil)proper(and(X1, X2))and(proper(X1), proper(X2))
proper(tt)ok(tt)proper(isList(X))isList(proper(X))
proper(isNeList(X))isNeList(proper(X))proper(isQid(X))isQid(proper(X))
proper(isNePal(X))isNePal(proper(X))proper(isPal(X))isPal(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))
and(ok(X1), ok(X2))ok(and(X1, X2))isList(ok(X))ok(isList(X))
isNeList(ok(X))ok(isNeList(X))isQid(ok(X))ok(isQid(X))
isNePal(ok(X))ok(isNePal(X))isPal(ok(X))ok(isPal(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, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, ok, isQid, proper, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

active#(__(X1, X2))active#(X1)active#(__(X1, X2))active#(X2)
active#(and(X1, X2))active#(X1)

Problem 4: 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(and(tt, X))mark(X)
active(isList(V))mark(isNeList(V))active(isList(nil))mark(tt)
active(isList(__(V1, V2)))mark(and(isList(V1), isList(V2)))active(isNeList(V))mark(isQid(V))
active(isNeList(__(V1, V2)))mark(and(isList(V1), isNeList(V2)))active(isNeList(__(V1, V2)))mark(and(isNeList(V1), isList(V2)))
active(isNePal(V))mark(isQid(V))active(isNePal(__(I, __(P, I))))mark(and(isQid(I), isPal(P)))
active(isPal(V))mark(isNePal(V))active(isPal(nil))mark(tt)
active(isQid(a))mark(tt)active(isQid(e))mark(tt)
active(isQid(i))mark(tt)active(isQid(o))mark(tt)
active(isQid(u))mark(tt)active(__(X1, X2))__(active(X1), X2)
active(__(X1, X2))__(X1, active(X2))active(and(X1, X2))and(active(X1), X2)
__(mark(X1), X2)mark(__(X1, X2))__(X1, mark(X2))mark(__(X1, X2))
and(mark(X1), X2)mark(and(X1, X2))proper(__(X1, X2))__(proper(X1), proper(X2))
proper(nil)ok(nil)proper(and(X1, X2))and(proper(X1), proper(X2))
proper(tt)ok(tt)proper(isList(X))isList(proper(X))
proper(isNeList(X))isNeList(proper(X))proper(isQid(X))isQid(proper(X))
proper(isNePal(X))isNePal(proper(X))proper(isPal(X))isPal(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))
and(ok(X1), ok(X2))ok(and(X1, X2))isList(ok(X))ok(isList(X))
isNeList(ok(X))ok(isNeList(X))isQid(ok(X))ok(isQid(X))
isNePal(ok(X))ok(isNePal(X))isPal(ok(X))ok(isPal(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, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, ok, isQid, proper, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isNePal#(ok(X))isNePal#(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(and(tt, X))mark(X)
active(isList(V))mark(isNeList(V))active(isList(nil))mark(tt)
active(isList(__(V1, V2)))mark(and(isList(V1), isList(V2)))active(isNeList(V))mark(isQid(V))
active(isNeList(__(V1, V2)))mark(and(isList(V1), isNeList(V2)))active(isNeList(__(V1, V2)))mark(and(isNeList(V1), isList(V2)))
active(isNePal(V))mark(isQid(V))active(isNePal(__(I, __(P, I))))mark(and(isQid(I), isPal(P)))
active(isPal(V))mark(isNePal(V))active(isPal(nil))mark(tt)
active(isQid(a))mark(tt)active(isQid(e))mark(tt)
active(isQid(i))mark(tt)active(isQid(o))mark(tt)
active(isQid(u))mark(tt)active(__(X1, X2))__(active(X1), X2)
active(__(X1, X2))__(X1, active(X2))active(and(X1, X2))and(active(X1), X2)
__(mark(X1), X2)mark(__(X1, X2))__(X1, mark(X2))mark(__(X1, X2))
and(mark(X1), X2)mark(and(X1, X2))proper(__(X1, X2))__(proper(X1), proper(X2))
proper(nil)ok(nil)proper(and(X1, X2))and(proper(X1), proper(X2))
proper(tt)ok(tt)proper(isList(X))isList(proper(X))
proper(isNeList(X))isNeList(proper(X))proper(isQid(X))isQid(proper(X))
proper(isNePal(X))isNePal(proper(X))proper(isPal(X))isPal(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))
and(ok(X1), ok(X2))ok(and(X1, X2))isList(ok(X))ok(isList(X))
isNeList(ok(X))ok(isNeList(X))isQid(ok(X))ok(isQid(X))
isNePal(ok(X))ok(isNePal(X))isPal(ok(X))ok(isPal(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, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, ok, isQid, proper, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isNeList#(ok(X))isNeList#(X)

Problem 6: PolynomialOrderingProcessor



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(and(tt, X))mark(X)
active(isList(V))mark(isNeList(V))active(isList(nil))mark(tt)
active(isList(__(V1, V2)))mark(and(isList(V1), isList(V2)))active(isNeList(V))mark(isQid(V))
active(isNeList(__(V1, V2)))mark(and(isList(V1), isNeList(V2)))active(isNeList(__(V1, V2)))mark(and(isNeList(V1), isList(V2)))
active(isNePal(V))mark(isQid(V))active(isNePal(__(I, __(P, I))))mark(and(isQid(I), isPal(P)))
active(isPal(V))mark(isNePal(V))active(isPal(nil))mark(tt)
active(isQid(a))mark(tt)active(isQid(e))mark(tt)
active(isQid(i))mark(tt)active(isQid(o))mark(tt)
active(isQid(u))mark(tt)active(__(X1, X2))__(active(X1), X2)
active(__(X1, X2))__(X1, active(X2))active(and(X1, X2))and(active(X1), X2)
__(mark(X1), X2)mark(__(X1, X2))__(X1, mark(X2))mark(__(X1, X2))
and(mark(X1), X2)mark(and(X1, X2))proper(__(X1, X2))__(proper(X1), proper(X2))
proper(nil)ok(nil)proper(and(X1, X2))and(proper(X1), proper(X2))
proper(tt)ok(tt)proper(isList(X))isList(proper(X))
proper(isNeList(X))isNeList(proper(X))proper(isQid(X))isQid(proper(X))
proper(isNePal(X))isNePal(proper(X))proper(isPal(X))isPal(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))
and(ok(X1), ok(X2))ok(and(X1, X2))isList(ok(X))ok(isList(X))
isNeList(ok(X))ok(isNeList(X))isQid(ok(X))ok(isQid(X))
isNePal(ok(X))ok(isNePal(X))isPal(ok(X))ok(isPal(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, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, ok, isQid, proper, nil, top

Strategy


Polynomial Interpretation

Improved Usable rules

active(__(X1, X2))__(active(X1), X2)active(isNePal(__(I, __(P, I))))mark(and(isQid(I), isPal(P)))
and(ok(X1), ok(X2))ok(and(X1, X2))active(isQid(a))mark(tt)
active(__(X, nil))mark(X)active(isNePal(V))mark(isQid(V))
proper(i)ok(i)__(mark(X1), X2)mark(__(X1, X2))
active(isQid(o))mark(tt)isQid(ok(X))ok(isQid(X))
proper(and(X1, X2))and(proper(X1), proper(X2))proper(e)ok(e)
active(__(__(X, Y), Z))mark(__(X, __(Y, Z)))proper(a)ok(a)
active(isQid(i))mark(tt)active(isNeList(__(V1, V2)))mark(and(isList(V1), isNeList(V2)))
active(isList(V))mark(isNeList(V))isNePal(ok(X))ok(isNePal(X))
active(isQid(e))mark(tt)active(and(X1, X2))and(active(X1), X2)
isPal(ok(X))ok(isPal(X))proper(isPal(X))isPal(proper(X))
active(isList(__(V1, V2)))mark(and(isList(V1), isList(V2)))__(ok(X1), ok(X2))ok(__(X1, X2))
isNeList(ok(X))ok(isNeList(X))proper(o)ok(o)
active(__(nil, X))mark(X)active(isPal(V))mark(isNePal(V))
active(isQid(u))mark(tt)proper(__(X1, X2))__(proper(X1), proper(X2))
proper(tt)ok(tt)proper(isList(X))isList(proper(X))
active(isPal(nil))mark(tt)active(isNeList(V))mark(isQid(V))
isList(ok(X))ok(isList(X))active(isList(nil))mark(tt)
proper(u)ok(u)active(and(tt, X))mark(X)
proper(isNePal(X))isNePal(proper(X))proper(isQid(X))isQid(proper(X))
active(isNeList(__(V1, V2)))mark(and(isNeList(V1), isList(V2)))proper(nil)ok(nil)
and(mark(X1), X2)mark(and(X1, X2))active(__(X1, X2))__(X1, active(X2))
proper(isNeList(X))isNeList(proper(X))__(X1, mark(X2))mark(__(X1, X2))

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

top#(mark(X))top#(proper(X))

Problem 13: PolynomialOrderingProcessor



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(and(tt, X))mark(X)
active(isList(V))mark(isNeList(V))active(isList(nil))mark(tt)
active(isList(__(V1, V2)))mark(and(isList(V1), isList(V2)))active(isNeList(V))mark(isQid(V))
active(isNeList(__(V1, V2)))mark(and(isList(V1), isNeList(V2)))active(isNeList(__(V1, V2)))mark(and(isNeList(V1), isList(V2)))
active(isNePal(V))mark(isQid(V))active(isNePal(__(I, __(P, I))))mark(and(isQid(I), isPal(P)))
active(isPal(V))mark(isNePal(V))active(isPal(nil))mark(tt)
active(isQid(a))mark(tt)active(isQid(e))mark(tt)
active(isQid(i))mark(tt)active(isQid(o))mark(tt)
active(isQid(u))mark(tt)active(__(X1, X2))__(active(X1), X2)
active(__(X1, X2))__(X1, active(X2))active(and(X1, X2))and(active(X1), X2)
__(mark(X1), X2)mark(__(X1, X2))__(X1, mark(X2))mark(__(X1, X2))
and(mark(X1), X2)mark(and(X1, X2))proper(__(X1, X2))__(proper(X1), proper(X2))
proper(nil)ok(nil)proper(and(X1, X2))and(proper(X1), proper(X2))
proper(tt)ok(tt)proper(isList(X))isList(proper(X))
proper(isNeList(X))isNeList(proper(X))proper(isQid(X))isQid(proper(X))
proper(isNePal(X))isNePal(proper(X))proper(isPal(X))isPal(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))
and(ok(X1), ok(X2))ok(and(X1, X2))isList(ok(X))ok(isList(X))
isNeList(ok(X))ok(isNeList(X))isQid(ok(X))ok(isQid(X))
isNePal(ok(X))ok(isNePal(X))isPal(ok(X))ok(isPal(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, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, ok, proper, isQid, top, nil

Strategy


Polynomial Interpretation

Improved Usable rules

active(__(X1, X2))__(active(X1), X2)active(isNePal(__(I, __(P, I))))mark(and(isQid(I), isPal(P)))
and(ok(X1), ok(X2))ok(and(X1, X2))active(isQid(a))mark(tt)
active(__(X, nil))mark(X)active(isNePal(V))mark(isQid(V))
__(mark(X1), X2)mark(__(X1, X2))active(isQid(o))mark(tt)
active(__(__(X, Y), Z))mark(__(X, __(Y, Z)))active(isQid(i))mark(tt)
active(isNeList(__(V1, V2)))mark(and(isList(V1), isNeList(V2)))active(isList(V))mark(isNeList(V))
active(isQid(e))mark(tt)active(and(X1, X2))and(active(X1), X2)
__(ok(X1), ok(X2))ok(__(X1, X2))active(isList(__(V1, V2)))mark(and(isList(V1), isList(V2)))
active(__(nil, X))mark(X)active(isPal(V))mark(isNePal(V))
active(isQid(u))mark(tt)active(isPal(nil))mark(tt)
active(isNeList(V))mark(isQid(V))active(isList(nil))mark(tt)
active(and(tt, X))mark(X)active(isNeList(__(V1, V2)))mark(and(isNeList(V1), isList(V2)))
and(mark(X1), X2)mark(and(X1, X2))active(__(X1, X2))__(X1, active(X2))
__(X1, mark(X2))mark(__(X1, X2))

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

top#(ok(X))top#(active(X))

Problem 7: 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(and(tt, X))mark(X)
active(isList(V))mark(isNeList(V))active(isList(nil))mark(tt)
active(isList(__(V1, V2)))mark(and(isList(V1), isList(V2)))active(isNeList(V))mark(isQid(V))
active(isNeList(__(V1, V2)))mark(and(isList(V1), isNeList(V2)))active(isNeList(__(V1, V2)))mark(and(isNeList(V1), isList(V2)))
active(isNePal(V))mark(isQid(V))active(isNePal(__(I, __(P, I))))mark(and(isQid(I), isPal(P)))
active(isPal(V))mark(isNePal(V))active(isPal(nil))mark(tt)
active(isQid(a))mark(tt)active(isQid(e))mark(tt)
active(isQid(i))mark(tt)active(isQid(o))mark(tt)
active(isQid(u))mark(tt)active(__(X1, X2))__(active(X1), X2)
active(__(X1, X2))__(X1, active(X2))active(and(X1, X2))and(active(X1), X2)
__(mark(X1), X2)mark(__(X1, X2))__(X1, mark(X2))mark(__(X1, X2))
and(mark(X1), X2)mark(and(X1, X2))proper(__(X1, X2))__(proper(X1), proper(X2))
proper(nil)ok(nil)proper(and(X1, X2))and(proper(X1), proper(X2))
proper(tt)ok(tt)proper(isList(X))isList(proper(X))
proper(isNeList(X))isNeList(proper(X))proper(isQid(X))isQid(proper(X))
proper(isNePal(X))isNePal(proper(X))proper(isPal(X))isPal(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))
and(ok(X1), ok(X2))ok(and(X1, X2))isList(ok(X))ok(isList(X))
isNeList(ok(X))ok(isNeList(X))isQid(ok(X))ok(isQid(X))
isNePal(ok(X))ok(isNePal(X))isPal(ok(X))ok(isPal(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, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, ok, isQid, proper, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isPal#(ok(X))isPal#(X)

Problem 8: 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(and(tt, X))mark(X)
active(isList(V))mark(isNeList(V))active(isList(nil))mark(tt)
active(isList(__(V1, V2)))mark(and(isList(V1), isList(V2)))active(isNeList(V))mark(isQid(V))
active(isNeList(__(V1, V2)))mark(and(isList(V1), isNeList(V2)))active(isNeList(__(V1, V2)))mark(and(isNeList(V1), isList(V2)))
active(isNePal(V))mark(isQid(V))active(isNePal(__(I, __(P, I))))mark(and(isQid(I), isPal(P)))
active(isPal(V))mark(isNePal(V))active(isPal(nil))mark(tt)
active(isQid(a))mark(tt)active(isQid(e))mark(tt)
active(isQid(i))mark(tt)active(isQid(o))mark(tt)
active(isQid(u))mark(tt)active(__(X1, X2))__(active(X1), X2)
active(__(X1, X2))__(X1, active(X2))active(and(X1, X2))and(active(X1), X2)
__(mark(X1), X2)mark(__(X1, X2))__(X1, mark(X2))mark(__(X1, X2))
and(mark(X1), X2)mark(and(X1, X2))proper(__(X1, X2))__(proper(X1), proper(X2))
proper(nil)ok(nil)proper(and(X1, X2))and(proper(X1), proper(X2))
proper(tt)ok(tt)proper(isList(X))isList(proper(X))
proper(isNeList(X))isNeList(proper(X))proper(isQid(X))isQid(proper(X))
proper(isNePal(X))isNePal(proper(X))proper(isPal(X))isPal(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))
and(ok(X1), ok(X2))ok(and(X1, X2))isList(ok(X))ok(isList(X))
isNeList(ok(X))ok(isNeList(X))isQid(ok(X))ok(isQid(X))
isNePal(ok(X))ok(isNePal(X))isPal(ok(X))ok(isPal(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, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, ok, isQid, proper, nil, top

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 12: 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(and(tt, X))mark(X)
active(isList(V))mark(isNeList(V))active(isList(nil))mark(tt)
active(isList(__(V1, V2)))mark(and(isList(V1), isList(V2)))active(isNeList(V))mark(isQid(V))
active(isNeList(__(V1, V2)))mark(and(isList(V1), isNeList(V2)))active(isNeList(__(V1, V2)))mark(and(isNeList(V1), isList(V2)))
active(isNePal(V))mark(isQid(V))active(isNePal(__(I, __(P, I))))mark(and(isQid(I), isPal(P)))
active(isPal(V))mark(isNePal(V))active(isPal(nil))mark(tt)
active(isQid(a))mark(tt)active(isQid(e))mark(tt)
active(isQid(i))mark(tt)active(isQid(o))mark(tt)
active(isQid(u))mark(tt)active(__(X1, X2))__(active(X1), X2)
active(__(X1, X2))__(X1, active(X2))active(and(X1, X2))and(active(X1), X2)
__(mark(X1), X2)mark(__(X1, X2))__(X1, mark(X2))mark(__(X1, X2))
and(mark(X1), X2)mark(and(X1, X2))proper(__(X1, X2))__(proper(X1), proper(X2))
proper(nil)ok(nil)proper(and(X1, X2))and(proper(X1), proper(X2))
proper(tt)ok(tt)proper(isList(X))isList(proper(X))
proper(isNeList(X))isNeList(proper(X))proper(isQid(X))isQid(proper(X))
proper(isNePal(X))isNePal(proper(X))proper(isPal(X))isPal(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))
and(ok(X1), ok(X2))ok(and(X1, X2))isList(ok(X))ok(isList(X))
isNeList(ok(X))ok(isNeList(X))isQid(ok(X))ok(isQid(X))
isNePal(ok(X))ok(isNePal(X))isPal(ok(X))ok(isPal(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, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, ok, proper, isQid, top, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

__#(X1, mark(X2))__#(X1, X2)

Problem 9: 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(and(tt, X))mark(X)
active(isList(V))mark(isNeList(V))active(isList(nil))mark(tt)
active(isList(__(V1, V2)))mark(and(isList(V1), isList(V2)))active(isNeList(V))mark(isQid(V))
active(isNeList(__(V1, V2)))mark(and(isList(V1), isNeList(V2)))active(isNeList(__(V1, V2)))mark(and(isNeList(V1), isList(V2)))
active(isNePal(V))mark(isQid(V))active(isNePal(__(I, __(P, I))))mark(and(isQid(I), isPal(P)))
active(isPal(V))mark(isNePal(V))active(isPal(nil))mark(tt)
active(isQid(a))mark(tt)active(isQid(e))mark(tt)
active(isQid(i))mark(tt)active(isQid(o))mark(tt)
active(isQid(u))mark(tt)active(__(X1, X2))__(active(X1), X2)
active(__(X1, X2))__(X1, active(X2))active(and(X1, X2))and(active(X1), X2)
__(mark(X1), X2)mark(__(X1, X2))__(X1, mark(X2))mark(__(X1, X2))
and(mark(X1), X2)mark(and(X1, X2))proper(__(X1, X2))__(proper(X1), proper(X2))
proper(nil)ok(nil)proper(and(X1, X2))and(proper(X1), proper(X2))
proper(tt)ok(tt)proper(isList(X))isList(proper(X))
proper(isNeList(X))isNeList(proper(X))proper(isQid(X))isQid(proper(X))
proper(isNePal(X))isNePal(proper(X))proper(isPal(X))isPal(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))
and(ok(X1), ok(X2))ok(and(X1, X2))isList(ok(X))ok(isList(X))
isNeList(ok(X))ok(isNeList(X))isQid(ok(X))ok(isQid(X))
isNePal(ok(X))ok(isNePal(X))isPal(ok(X))ok(isPal(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, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, ok, isQid, proper, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isQid#(ok(X))isQid#(X)

Problem 10: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

proper#(__(X1, X2))proper#(X1)proper#(isPal(X))proper#(X)
proper#(and(X1, X2))proper#(X2)proper#(isList(X))proper#(X)
proper#(isQid(X))proper#(X)proper#(isNePal(X))proper#(X)
proper#(isNeList(X))proper#(X)proper#(__(X1, X2))proper#(X2)
proper#(and(X1, X2))proper#(X1)

Rewrite Rules

active(__(__(X, Y), Z))mark(__(X, __(Y, Z)))active(__(X, nil))mark(X)
active(__(nil, X))mark(X)active(and(tt, X))mark(X)
active(isList(V))mark(isNeList(V))active(isList(nil))mark(tt)
active(isList(__(V1, V2)))mark(and(isList(V1), isList(V2)))active(isNeList(V))mark(isQid(V))
active(isNeList(__(V1, V2)))mark(and(isList(V1), isNeList(V2)))active(isNeList(__(V1, V2)))mark(and(isNeList(V1), isList(V2)))
active(isNePal(V))mark(isQid(V))active(isNePal(__(I, __(P, I))))mark(and(isQid(I), isPal(P)))
active(isPal(V))mark(isNePal(V))active(isPal(nil))mark(tt)
active(isQid(a))mark(tt)active(isQid(e))mark(tt)
active(isQid(i))mark(tt)active(isQid(o))mark(tt)
active(isQid(u))mark(tt)active(__(X1, X2))__(active(X1), X2)
active(__(X1, X2))__(X1, active(X2))active(and(X1, X2))and(active(X1), X2)
__(mark(X1), X2)mark(__(X1, X2))__(X1, mark(X2))mark(__(X1, X2))
and(mark(X1), X2)mark(and(X1, X2))proper(__(X1, X2))__(proper(X1), proper(X2))
proper(nil)ok(nil)proper(and(X1, X2))and(proper(X1), proper(X2))
proper(tt)ok(tt)proper(isList(X))isList(proper(X))
proper(isNeList(X))isNeList(proper(X))proper(isQid(X))isQid(proper(X))
proper(isNePal(X))isNePal(proper(X))proper(isPal(X))isPal(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))
and(ok(X1), ok(X2))ok(and(X1, X2))isList(ok(X))ok(isList(X))
isNeList(ok(X))ok(isNeList(X))isQid(ok(X))ok(isQid(X))
isNePal(ok(X))ok(isNePal(X))isPal(ok(X))ok(isPal(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, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, ok, isQid, proper, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

proper#(__(X1, X2))proper#(X1)proper#(isPal(X))proper#(X)
proper#(and(X1, X2))proper#(X2)proper#(isQid(X))proper#(X)
proper#(isList(X))proper#(X)proper#(isNePal(X))proper#(X)
proper#(isNeList(X))proper#(X)proper#(__(X1, X2))proper#(X2)
proper#(and(X1, X2))proper#(X1)

Problem 11: 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(and(tt, X))mark(X)
active(isList(V))mark(isNeList(V))active(isList(nil))mark(tt)
active(isList(__(V1, V2)))mark(and(isList(V1), isList(V2)))active(isNeList(V))mark(isQid(V))
active(isNeList(__(V1, V2)))mark(and(isList(V1), isNeList(V2)))active(isNeList(__(V1, V2)))mark(and(isNeList(V1), isList(V2)))
active(isNePal(V))mark(isQid(V))active(isNePal(__(I, __(P, I))))mark(and(isQid(I), isPal(P)))
active(isPal(V))mark(isNePal(V))active(isPal(nil))mark(tt)
active(isQid(a))mark(tt)active(isQid(e))mark(tt)
active(isQid(i))mark(tt)active(isQid(o))mark(tt)
active(isQid(u))mark(tt)active(__(X1, X2))__(active(X1), X2)
active(__(X1, X2))__(X1, active(X2))active(and(X1, X2))and(active(X1), X2)
__(mark(X1), X2)mark(__(X1, X2))__(X1, mark(X2))mark(__(X1, X2))
and(mark(X1), X2)mark(and(X1, X2))proper(__(X1, X2))__(proper(X1), proper(X2))
proper(nil)ok(nil)proper(and(X1, X2))and(proper(X1), proper(X2))
proper(tt)ok(tt)proper(isList(X))isList(proper(X))
proper(isNeList(X))isNeList(proper(X))proper(isQid(X))isQid(proper(X))
proper(isNePal(X))isNePal(proper(X))proper(isPal(X))isPal(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))
and(ok(X1), ok(X2))ok(and(X1, X2))isList(ok(X))ok(isList(X))
isNeList(ok(X))ok(isNeList(X))isQid(ok(X))ok(isQid(X))
isNePal(ok(X))ok(isNePal(X))isPal(ok(X))ok(isPal(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, e, a, isNeList, o, __, mark, isPal, i, and, u, tt, isNePal, active, ok, isQid, proper, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isList#(ok(X))isList#(X)