Termination proof of /tmp/tmpp0U02Q/PALINDROME

Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
and: {1}
tt: empty set
isList: empty set
isNeList: empty set
isQid: empty set
isNePal: empty set
isPal: empty set
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set

↳ CSR

  ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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

The replacement map contains the following entries:

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, __¹} are replacing on all positions.
For all symbols f in {and, AND} we have µ(f) = {1}.
The symbols in {isList, isNeList, isQid, isNePal, isPal, ISNELIST, ISLIST, ISQID, ISNEPAL, ISPAL, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DP_o are:

__¹(__(X, Y), Z) → __¹(X, __(Y, Z))
__¹(__(X, Y), Z) → __¹(Y, Z)
ISLIST(V) → ISNELIST(V)
ISLIST(__(V1, V2)) → AND(isList(V1), isList(V2))
ISLIST(__(V1, V2)) → ISLIST(V1)
ISNELIST(V) → ISQID(V)
ISNELIST(__(V1, V2)) → AND(isList(V1), isNeList(V2))
ISNELIST(__(V1, V2)) → ISLIST(V1)
ISNELIST(__(V1, V2)) → AND(isNeList(V1), isList(V2))
ISNELIST(__(V1, V2)) → ISNELIST(V1)
ISNEPAL(V) → ISQID(V)
ISNEPAL(__(I, __(P, I))) → AND(isQid(I), isPal(P))
ISNEPAL(__(I, __(P, I))) → ISQID(I)
ISPAL(V) → ISNEPAL(V)

The collapsing dependency pairs are DP_c:

AND(tt, X) → X

The hidden terms of R are:

isList(V2)
isNeList(V2)
isPal(P)

Every hiding context is built from:none

Hence, the new unhiding pairs DP_u are :

AND(tt, X) → U(X)
U(isList(V2)) → ISLIST(V2)
U(isNeList(V2)) → ISNELIST(V2)
U(isPal(P)) → ISPAL(P)

The TRS R consists of the following rules:

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

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 2 SCCs with 3 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__} are replacing on all positions.
For all symbols f in {and, AND} we have µ(f) = {1}.
The symbols in {isList, isNeList, isQid, isNePal, isPal, ISNELIST, U, ISLIST, ISPAL, ISNEPAL} are not replacing on any position.

The TRS P consists of the following rules:

ISNELIST(__(V1, V2)) → AND(isList(V1), isNeList(V2))
AND(tt, X) → U(X)
U(isList(V2)) → ISLIST(V2)
ISLIST(V) → ISNELIST(V)
ISNELIST(__(V1, V2)) → ISLIST(V1)
ISLIST(__(V1, V2)) → AND(isList(V1), isList(V2))
ISLIST(__(V1, V2)) → ISLIST(V1)
ISNELIST(__(V1, V2)) → AND(isNeList(V1), isList(V2))
ISNELIST(__(V1, V2)) → ISNELIST(V1)
U(isNeList(V2)) → ISNELIST(V2)
U(isPal(P)) → ISPAL(P)
ISPAL(V) → ISNEPAL(V)
ISNEPAL(__(I, __(P, I))) → AND(isQid(I), isPal(P))

The TRS R consists of the following rules:

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

Q is empty.

Using the order
Polynomial interpretation with max and min functions [25]:

POL(AND(x₁, x₂)) = x₂
POL(ISLIST(x₁)) = 0
POL(ISNELIST(x₁)) = 0
POL(ISNEPAL(x₁)) = x₁
POL(ISPAL(x₁)) = x₁
POL(U(x₁)) = x₁
POL(__(x₁, x₂)) = 1 + x₁ + x₂
POL(a) = 0
POL(and(x₁, x₂)) = x₂
POL(e) = 0
POL(i) = 0
POL(isList(x₁)) = 0
POL(isNeList(x₁)) = 0
POL(isNePal(x₁)) = x₁
POL(isPal(x₁)) = 1 + x₁
POL(isQid(x₁)) = 0
POL(nil) = 0
POL(o) = 0
POL(tt) = 0
POL(u) = 0

the following usable rules

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

could all be oriented weakly.
Furthermore, the pairs

U(isPal(P)) → ISPAL(P)
ISNEPAL(__(I, __(P, I))) → AND(isQid(I), isPal(P))

could be oriented strictly and thus removed.
The pairs

ISNELIST(__(V1, V2)) → AND(isList(V1), isNeList(V2))
AND(tt, X) → U(X)
U(isList(V2)) → ISLIST(V2)
ISLIST(V) → ISNELIST(V)
ISNELIST(__(V1, V2)) → ISLIST(V1)
ISLIST(__(V1, V2)) → AND(isList(V1), isList(V2))
ISLIST(__(V1, V2)) → ISLIST(V1)
ISNELIST(__(V1, V2)) → AND(isNeList(V1), isList(V2))
ISNELIST(__(V1, V2)) → ISNELIST(V1)
U(isNeList(V2)) → ISNELIST(V2)
ISPAL(V) → ISNEPAL(V)

could only be oriented weakly and must be analyzed further.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__} are replacing on all positions.
For all symbols f in {and, AND} we have µ(f) = {1}.
The symbols in {isList, isNeList, isQid, isNePal, isPal, ISNELIST, U, ISLIST, ISNEPAL, ISPAL} are not replacing on any position.

The TRS P consists of the following rules:

ISNELIST(__(V1, V2)) → AND(isList(V1), isNeList(V2))
AND(tt, X) → U(X)
U(isList(V2)) → ISLIST(V2)
ISLIST(V) → ISNELIST(V)
ISNELIST(__(V1, V2)) → ISLIST(V1)
ISLIST(__(V1, V2)) → AND(isList(V1), isList(V2))
ISLIST(__(V1, V2)) → ISLIST(V1)
ISNELIST(__(V1, V2)) → AND(isNeList(V1), isList(V2))
ISNELIST(__(V1, V2)) → ISNELIST(V1)
U(isNeList(V2)) → ISNELIST(V2)
ISPAL(V) → ISNEPAL(V)

The TRS R consists of the following rules:

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

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 1 SCC.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ QCSDP

                    ↳ QCSDPReductionPairProof

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__} are replacing on all positions.
For all symbols f in {and, AND} we have µ(f) = {1}.
The symbols in {isList, isNeList, isQid, isNePal, isPal, U, ISLIST, ISNELIST} are not replacing on any position.

The TRS P consists of the following rules:

AND(tt, X) → U(X)
U(isList(V2)) → ISLIST(V2)
ISLIST(V) → ISNELIST(V)
ISNELIST(__(V1, V2)) → AND(isList(V1), isNeList(V2))
ISNELIST(__(V1, V2)) → ISLIST(V1)
ISLIST(__(V1, V2)) → AND(isList(V1), isList(V2))
ISLIST(__(V1, V2)) → ISLIST(V1)
ISNELIST(__(V1, V2)) → AND(isNeList(V1), isList(V2))
ISNELIST(__(V1, V2)) → ISNELIST(V1)
U(isNeList(V2)) → ISNELIST(V2)

The TRS R consists of the following rules:

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

Q is empty.

Using the order
Polynomial Order [21,25] with Interpretation:

POL( i ) = 1

POL( a ) = max{0, -1}

POL( __(x₁, x₂) ) = 2x₁ + x₂ + 2

POL( isList(x₁) ) = x₁ + 2

POL( ISNELIST(x₁) ) = 2x₁ + 1

POL( e ) = max{0, -1}

POL( isNePal(x₁) ) = x₁ + 1

POL( and(x₁, x₂) ) = x₂ + 2

POL( o ) = 2

POL( isQid(x₁) ) = max{0, x₁ - 1}

POL( isPal(x₁) ) = 2x₁ + 2

POL( tt ) = max{0, -1}

POL( u ) = max{0, -1}

POL( AND(x₁, x₂) ) = 2x₂

POL( U(x₁) ) = max{0, 2x₁ - 1}

POL( isNeList(x₁) ) = x₁ + 2

POL( ISLIST(x₁) ) = 2x₁ + 2

POL( nil ) = max{0, -1}

the following usable rules

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

could all be oriented weakly.
Furthermore, the pairs

U(isList(V2)) → ISLIST(V2)
ISLIST(V) → ISNELIST(V)
ISNELIST(__(V1, V2)) → AND(isList(V1), isNeList(V2))
ISNELIST(__(V1, V2)) → ISLIST(V1)
ISLIST(__(V1, V2)) → AND(isList(V1), isList(V2))
ISLIST(__(V1, V2)) → ISLIST(V1)
ISNELIST(__(V1, V2)) → AND(isNeList(V1), isList(V2))
ISNELIST(__(V1, V2)) → ISNELIST(V1)
U(isNeList(V2)) → ISNELIST(V2)

could be oriented strictly and thus removed.
The pairs

AND(tt, X) → U(X)

could only be oriented weakly and must be analyzed further.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ QCSDP

                    ↳ QCSDPReductionPairProof

                      ↳ QCSDP

                        ↳ QCSDependencyGraphProof

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__} are replacing on all positions.
For all symbols f in {and, AND} we have µ(f) = {1}.
The symbols in {isList, isNeList, isQid, isNePal, isPal, U} are not replacing on any position.

The TRS P consists of the following rules:

AND(tt, X) → U(X)

The TRS R consists of the following rules:

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

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, __¹} are replacing on all positions.
For all symbols f in {and} we have µ(f) = {1}.
The symbols in {isList, isNeList, isQid, isNePal, isPal} are not replacing on any position.

The TRS P consists of the following rules:

__¹(__(X, Y), Z) → __¹(X, __(Y, Z))
__¹(__(X, Y), Z) → __¹(Y, Z)

The TRS R consists of the following rules:

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

Q is empty.

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

__¹(__(X, Y), Z) → __¹(X, __(Y, Z))
__¹(__(X, Y), Z) → __¹(Y, Z)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
__¹(x1, x2) = x1

Subterm Order

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSDPSubtermProof

              ↳ QCSDP

                ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {__} are replacing on all positions.
For all symbols f in {and} we have µ(f) = {1}.
The symbols in {isList, isNeList, isQid, isNePal, isPal} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

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

Q is empty.

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.