YES Termination proof of ../tpdb/TRS/CSR_Maude/palindrome/PALINDROME_nokinds.trs
Termination of the following Term Rewriting System could be proven:

Q restricted 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
  ↳ Zantema-Transformation

Q restricted 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

We applied the Zantema [34] to transform the context-sensitive TRS to an usual TRS.

↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof

Q restricted 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) → a(X)
isList(V) → isNeList(a(V))
isList(nilInact) → tt
isList(__Inact(V1, V2)) → and(isList(a(V1)), isListInact(a(V2)))
isNeList(V) → isQid(a(V))
isNeList(__Inact(V1, V2)) → and(isList(a(V1)), isNeListInact(a(V2)))
isNeList(__Inact(V1, V2)) → and(isNeList(a(V1)), isListInact(a(V2)))
isNePal(V) → isQid(a(V))
isNePal(__Inact(I, __(P, I))) → and(isQid(a(I)), isPalInact(a(P)))
isPal(V) → isNePal(a(V))
isPal(nilInact) → tt
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
isNeList(x1) → isNeListInact(x1)
a(isNeListInact(x1)) → isNeList(x1)
isPal(x1) → isPalInact(x1)
a(isPalInact(x1)) → isPal(x1)
i → iInact
a(iInact) → i
isList(x1) → isListInact(x1)
a(isListInact(x1)) → isList(x1)
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o

Q is empty.

The following Q TRS is given: Q restricted 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) → a(X)
isList(V) → isNeList(a(V))
isList(nilInact) → tt
isList(__Inact(V1, V2)) → and(isList(a(V1)), isListInact(a(V2)))
isNeList(V) → isQid(a(V))
isNeList(__Inact(V1, V2)) → and(isList(a(V1)), isNeListInact(a(V2)))
isNeList(__Inact(V1, V2)) → and(isNeList(a(V1)), isListInact(a(V2)))
isNePal(V) → isQid(a(V))
isNePal(__Inact(I, __(P, I))) → and(isQid(a(I)), isPalInact(a(P)))
isPal(V) → isNePal(a(V))
isPal(nilInact) → tt
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
isNeList(x1) → isNeListInact(x1)
a(isNeListInact(x1)) → isNeList(x1)
isPal(x1) → isPalInact(x1)
a(isPalInact(x1)) → isPal(x1)
i → iInact
a(iInact) → i
isList(x1) → isListInact(x1)
a(isListInact(x1)) → isList(x1)
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

isNePal(V) → isQid(a(V))
isPal(nilInact) → tt
Used ordering:
Polynomial interpretation [25]:

POL(__(x1, x2)) = 2·x1 + x2   
POL(__Inact(x1, x2)) = 2·x1 + x2   
POL(a) = 0   
POL(a(x1)) = x1   
POL(aInact) = 0   
POL(and(x1, x2)) = x1 + x2   
POL(e) = 0   
POL(eInact) = 0   
POL(i) = 0   
POL(iInact) = 0   
POL(isList(x1)) = x1   
POL(isListInact(x1)) = x1   
POL(isNeList(x1)) = x1   
POL(isNeListInact(x1)) = x1   
POL(isNePal(x1)) = 1 + x1   
POL(isPal(x1)) = 1 + 2·x1   
POL(isPalInact(x1)) = 1 + 2·x1   
POL(isQid(x1)) = x1   
POL(nil) = 0   
POL(nilInact) = 0   
POL(o) = 0   
POL(oInact) = 0   
POL(tt) = 0   
POL(u) = 0   
POL(uInact) = 0   




↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof

Q restricted 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) → a(X)
isList(V) → isNeList(a(V))
isList(nilInact) → tt
isList(__Inact(V1, V2)) → and(isList(a(V1)), isListInact(a(V2)))
isNeList(V) → isQid(a(V))
isNeList(__Inact(V1, V2)) → and(isList(a(V1)), isNeListInact(a(V2)))
isNeList(__Inact(V1, V2)) → and(isNeList(a(V1)), isListInact(a(V2)))
isNePal(__Inact(I, __(P, I))) → and(isQid(a(I)), isPalInact(a(P)))
isPal(V) → isNePal(a(V))
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
isNeList(x1) → isNeListInact(x1)
a(isNeListInact(x1)) → isNeList(x1)
isPal(x1) → isPalInact(x1)
a(isPalInact(x1)) → isPal(x1)
i → iInact
a(iInact) → i
isList(x1) → isListInact(x1)
a(isListInact(x1)) → isList(x1)
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o

Q is empty.

The following Q TRS is given: Q restricted 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) → a(X)
isList(V) → isNeList(a(V))
isList(nilInact) → tt
isList(__Inact(V1, V2)) → and(isList(a(V1)), isListInact(a(V2)))
isNeList(V) → isQid(a(V))
isNeList(__Inact(V1, V2)) → and(isList(a(V1)), isNeListInact(a(V2)))
isNeList(__Inact(V1, V2)) → and(isNeList(a(V1)), isListInact(a(V2)))
isNePal(__Inact(I, __(P, I))) → and(isQid(a(I)), isPalInact(a(P)))
isPal(V) → isNePal(a(V))
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
isNeList(x1) → isNeListInact(x1)
a(isNeListInact(x1)) → isNeList(x1)
isPal(x1) → isPalInact(x1)
a(isPalInact(x1)) → isPal(x1)
i → iInact
a(iInact) → i
isList(x1) → isListInact(x1)
a(isListInact(x1)) → isList(x1)
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

__(X, nil) → X
__(nil, X) → X
and(tt, X) → a(X)
isList(__Inact(V1, V2)) → and(isList(a(V1)), isListInact(a(V2)))
isNeList(__Inact(V1, V2)) → and(isList(a(V1)), isNeListInact(a(V2)))
isNeList(__Inact(V1, V2)) → and(isNeList(a(V1)), isListInact(a(V2)))
isNePal(__Inact(I, __(P, I))) → and(isQid(a(I)), isPalInact(a(P)))
isPal(V) → isNePal(a(V))
Used ordering:
Polynomial interpretation [25]:

POL(__(x1, x2)) = 2 + x1 + x2   
POL(__Inact(x1, x2)) = 2 + x1 + x2   
POL(a) = 0   
POL(a(x1)) = x1   
POL(aInact) = 0   
POL(and(x1, x2)) = 1 + x1 + x2   
POL(e) = 0   
POL(eInact) = 0   
POL(i) = 0   
POL(iInact) = 0   
POL(isList(x1)) = x1   
POL(isListInact(x1)) = x1   
POL(isNeList(x1)) = x1   
POL(isNeListInact(x1)) = x1   
POL(isNePal(x1)) = 2·x1   
POL(isPal(x1)) = 2 + 2·x1   
POL(isPalInact(x1)) = 2 + 2·x1   
POL(isQid(x1)) = x1   
POL(nil) = 0   
POL(nilInact) = 0   
POL(o) = 0   
POL(oInact) = 0   
POL(tt) = 0   
POL(u) = 0   
POL(uInact) = 0   




↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
isList(V) → isNeList(a(V))
isList(nilInact) → tt
isNeList(V) → isQid(a(V))
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
isNeList(x1) → isNeListInact(x1)
a(isNeListInact(x1)) → isNeList(x1)
isPal(x1) → isPalInact(x1)
a(isPalInact(x1)) → isPal(x1)
i → iInact
a(iInact) → i
isList(x1) → isListInact(x1)
a(isListInact(x1)) → isList(x1)
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
isList(V) → isNeList(a(V))
isList(nilInact) → tt
isNeList(V) → isQid(a(V))
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
isNeList(x1) → isNeListInact(x1)
a(isNeListInact(x1)) → isNeList(x1)
isPal(x1) → isPalInact(x1)
a(isPalInact(x1)) → isPal(x1)
i → iInact
a(iInact) → i
isList(x1) → isListInact(x1)
a(isListInact(x1)) → isList(x1)
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

isList(V) → isNeList(a(V))
isList(nilInact) → tt
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
Used ordering:
Polynomial interpretation [25]:

POL(__(x1, x2)) = x1 + x2   
POL(__Inact(x1, x2)) = x1 + x2   
POL(a) = 0   
POL(a(x1)) = x1   
POL(aInact) = 0   
POL(e) = 0   
POL(eInact) = 0   
POL(i) = 0   
POL(iInact) = 0   
POL(isList(x1)) = 2 + 2·x1   
POL(isListInact(x1)) = 2 + 2·x1   
POL(isNeList(x1)) = 1 + 2·x1   
POL(isNeListInact(x1)) = 1 + 2·x1   
POL(isPal(x1)) = x1   
POL(isPalInact(x1)) = x1   
POL(isQid(x1)) = 1 + x1   
POL(nil) = 0   
POL(nilInact) = 0   
POL(o) = 0   
POL(oInact) = 0   
POL(tt) = 0   
POL(u) = 0   
POL(uInact) = 0   




↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
isNeList(V) → isQid(a(V))
a(x) → x
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
isNeList(x1) → isNeListInact(x1)
a(isNeListInact(x1)) → isNeList(x1)
isPal(x1) → isPalInact(x1)
a(isPalInact(x1)) → isPal(x1)
i → iInact
a(iInact) → i
isList(x1) → isListInact(x1)
a(isListInact(x1)) → isList(x1)
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
isNeList(V) → isQid(a(V))
a(x) → x
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
isNeList(x1) → isNeListInact(x1)
a(isNeListInact(x1)) → isNeList(x1)
isPal(x1) → isPalInact(x1)
a(isPalInact(x1)) → isPal(x1)
i → iInact
a(iInact) → i
isList(x1) → isListInact(x1)
a(isListInact(x1)) → isList(x1)
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

a(x) → x
e → eInact
a(eInact) → e
a(uInact) → u
a → aInact
a(aInact) → a
a(__Inact(x1, x2)) → __(x1, x2)
isNeList(x1) → isNeListInact(x1)
a(isPalInact(x1)) → isPal(x1)
i → iInact
a(iInact) → i
a(isListInact(x1)) → isList(x1)
nil → nilInact
o → oInact
a(oInact) → o
Used ordering:
Polynomial interpretation [25]:

POL(__(x1, x2)) = 2·x1 + x2   
POL(__Inact(x1, x2)) = 2·x1 + x2   
POL(a) = 2   
POL(a(x1)) = 2 + x1   
POL(aInact) = 1   
POL(e) = 1   
POL(eInact) = 0   
POL(i) = 1   
POL(iInact) = 0   
POL(isList(x1)) = 1 + x1   
POL(isListInact(x1)) = 1 + x1   
POL(isNeList(x1)) = 2 + x1   
POL(isNeListInact(x1)) = x1   
POL(isPal(x1)) = 2·x1   
POL(isPalInact(x1)) = 2·x1   
POL(isQid(x1)) = x1   
POL(nil) = 2   
POL(nilInact) = 0   
POL(o) = 1   
POL(oInact) = 0   
POL(u) = 0   
POL(uInact) = 0   




↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
isNeList(V) → isQid(a(V))
u → uInact
__(x1, x2) → __Inact(x1, x2)
a(isNeListInact(x1)) → isNeList(x1)
isPal(x1) → isPalInact(x1)
isList(x1) → isListInact(x1)
a(nilInact) → nil

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
isNeList(V) → isQid(a(V))
u → uInact
__(x1, x2) → __Inact(x1, x2)
a(isNeListInact(x1)) → isNeList(x1)
isPal(x1) → isPalInact(x1)
isList(x1) → isListInact(x1)
a(nilInact) → nil

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

__(__(X, Y), Z) → __(X, __(Y, Z))
u → uInact
a(isNeListInact(x1)) → isNeList(x1)
isList(x1) → isListInact(x1)
Used ordering:
Polynomial interpretation [25]:

POL(__(x1, x2)) = 1 + 2·x1 + x2   
POL(__Inact(x1, x2)) = 1 + 2·x1 + x2   
POL(a(x1)) = x1   
POL(isList(x1)) = 2 + 2·x1   
POL(isListInact(x1)) = 1 + x1   
POL(isNeList(x1)) = 2·x1   
POL(isNeListInact(x1)) = 2 + 2·x1   
POL(isPal(x1)) = 2 + 2·x1   
POL(isPalInact(x1)) = 2 + x1   
POL(isQid(x1)) = x1   
POL(nil) = 2   
POL(nilInact) = 2   
POL(u) = 2   
POL(uInact) = 0   




↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

isNeList(V) → isQid(a(V))
__(x1, x2) → __Inact(x1, x2)
isPal(x1) → isPalInact(x1)
a(nilInact) → nil

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

isNeList(V) → isQid(a(V))
__(x1, x2) → __Inact(x1, x2)
isPal(x1) → isPalInact(x1)
a(nilInact) → nil

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

isNeList(V) → isQid(a(V))
__(x1, x2) → __Inact(x1, x2)
a(nilInact) → nil
Used ordering:
Polynomial interpretation [25]:

POL(__(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(__Inact(x1, x2)) = x1 + 2·x2   
POL(a(x1)) = x1   
POL(isNeList(x1)) = 1 + 2·x1   
POL(isPal(x1)) = 1 + x1   
POL(isPalInact(x1)) = 1 + x1   
POL(isQid(x1)) = 2·x1   
POL(nil) = 0   
POL(nilInact) = 1   




↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

isPal(x1) → isPalInact(x1)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

isPal(x1) → isPalInact(x1)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

isPal(x1) → isPalInact(x1)
Used ordering:
Polynomial interpretation [25]:

POL(isPal(x1)) = 2 + 2·x1   
POL(isPalInact(x1)) = 1 + x1   




↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ RRRPoloQTRSProof
                ↳ QTRS
                  ↳ RRRPoloQTRSProof
                    ↳ QTRS
                      ↳ RRRPoloQTRSProof
                        ↳ QTRS
                          ↳ RRRPoloQTRSProof
                            ↳ QTRS
                              ↳ RRRPoloQTRSProof
                                ↳ QTRS
                                  ↳ RisEmptyProof

Q restricted rewrite system:
R is empty.
Q is empty.

The TRS R is empty. Hence, termination is trivially proven.