YES Termination proof of ../tpdb/TRS/CSR_Maude/palindrome/PALINDROME_nokinds-noand.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
U11(tt) → tt
U21(tt, V2) → U22(isList(V2))
U22(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNeList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isList(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt, P) → U72(isPal(P))
U72(tt) → tt
U81(tt) → tt
isList(V) → U11(isNeList(V))
isList(nil) → tt
isList(__(V1, V2)) → U21(isList(V1), V2)
isNeList(V) → U31(isQid(V))
isNeList(__(V1, V2)) → U41(isList(V1), V2)
isNeList(__(V1, V2)) → U51(isNeList(V1), V2)
isNePal(V) → U61(isQid(V))
isNePal(__(I, __(P, I))) → U71(isQid(I), P)
isPal(V) → U81(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
U11: {1}
tt: empty set
U21: {1}
U22: {1}
isList: empty set
U31: {1}
U41: {1}
U42: {1}
isNeList: empty set
U51: {1}
U52: {1}
U61: {1}
U71: {1}
U72: {1}
isPal: empty set
U81: {1}
isQid: empty set
isNePal: empty set
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set


↳ CSR
  ↳ Lucas-Transformation
  ↳ 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
U11(tt) → tt
U21(tt, V2) → U22(isList(V2))
U22(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNeList(V2))
U42(tt) → tt
U51(tt, V2) → U52(isList(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt, P) → U72(isPal(P))
U72(tt) → tt
U81(tt) → tt
isList(V) → U11(isNeList(V))
isList(nil) → tt
isList(__(V1, V2)) → U21(isList(V1), V2)
isNeList(V) → U31(isQid(V))
isNeList(__(V1, V2)) → U41(isList(V1), V2)
isNeList(__(V1, V2)) → U51(isNeList(V1), V2)
isNePal(V) → U61(isQid(V))
isNePal(__(I, __(P, I))) → U71(isQid(I), P)
isPal(V) → U81(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
U11: {1}
tt: empty set
U21: {1}
U22: {1}
isList: empty set
U31: {1}
U41: {1}
U42: {1}
isNeList: empty set
U51: {1}
U52: {1}
U61: {1}
U71: {1}
U72: {1}
isPal: empty set
U81: {1}
isQid: empty set
isNePal: empty set
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set

We applied the Lucas [26] to transform the context-sensitive TRS to an usual TRS.

↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
  ↳ 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
U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U61(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U61(isQid)
isNePal → U71(isQid)
isPal → U81(isNePal)
isPal → tt
isQid → tt

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
U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U61(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U61(isQid)
isNePal → U71(isQid)
isPal → U81(isNePal)
isPal → tt
isQid → tt

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))
__(X, nil) → X
__(nil, X) → X
Used ordering:
Polynomial interpretation [25]:

POL(U11(x1)) = x1   
POL(U21(x1)) = x1   
POL(U22(x1)) = 2·x1   
POL(U31(x1)) = 2·x1   
POL(U41(x1)) = x1   
POL(U42(x1)) = 2·x1   
POL(U51(x1)) = 2·x1   
POL(U52(x1)) = x1   
POL(U61(x1)) = x1   
POL(U71(x1)) = 2·x1   
POL(U72(x1)) = 2·x1   
POL(U81(x1)) = 2·x1   
POL(__(x1, x2)) = 2 + 2·x1 + x2   
POL(isList) = 0   
POL(isNeList) = 0   
POL(isNePal) = 0   
POL(isPal) = 0   
POL(isQid) = 0   
POL(nil) = 2   
POL(tt) = 0   




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

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

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U61(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U61(isQid)
isNePal → U71(isQid)
isPal → U81(isNePal)
isPal → tt
isQid → tt

Q is empty.

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

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U61(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U61(isQid)
isNePal → U71(isQid)
isPal → U81(isNePal)
isPal → tt
isQid → tt

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

U61(tt) → tt
isNePal → U61(isQid)
isPal → tt
Used ordering:
Polynomial interpretation [25]:

POL(U11(x1)) = 2·x1   
POL(U21(x1)) = 2·x1   
POL(U22(x1)) = x1   
POL(U31(x1)) = x1   
POL(U41(x1)) = 2·x1   
POL(U42(x1)) = 2·x1   
POL(U51(x1)) = 2·x1   
POL(U52(x1)) = 2·x1   
POL(U61(x1)) = 1 + 2·x1   
POL(U71(x1)) = 2 + 2·x1   
POL(U72(x1)) = x1   
POL(U81(x1)) = x1   
POL(isList) = 0   
POL(isNeList) = 0   
POL(isNePal) = 2   
POL(isPal) = 2   
POL(isQid) = 0   
POL(tt) = 0   




↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
  ↳ Zantema-Transformation

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

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U71(isQid)
isPal → U81(isNePal)
isQid → tt

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

ISNELIST → U511(isNeList)
ISNEPAL → ISQID
U211(tt) → ISLIST
ISNELIST → ISNELIST
U411(tt) → ISNELIST
ISNELIST → ISLIST
U411(tt) → U421(isNeList)
U211(tt) → U221(isList)
U511(tt) → U521(isList)
U511(tt) → ISLIST
U711(tt) → ISPAL
ISLIST → ISLIST
ISNELIST → U411(isList)
ISLIST → U111(isNeList)
ISNEPAL → U711(isQid)
ISNELIST → U311(isQid)
ISNELIST → ISQID
U711(tt) → U721(isPal)
ISPAL → ISNEPAL
ISLIST → U211(isList)
ISPAL → U811(isNePal)
ISLIST → ISNELIST

The TRS R consists of the following rules:

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U71(isQid)
isPal → U81(isNePal)
isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
  ↳ Zantema-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNELIST → U511(isNeList)
ISNEPAL → ISQID
U211(tt) → ISLIST
ISNELIST → ISNELIST
U411(tt) → ISNELIST
ISNELIST → ISLIST
U411(tt) → U421(isNeList)
U211(tt) → U221(isList)
U511(tt) → U521(isList)
U511(tt) → ISLIST
U711(tt) → ISPAL
ISLIST → ISLIST
ISNELIST → U411(isList)
ISLIST → U111(isNeList)
ISNEPAL → U711(isQid)
ISNELIST → U311(isQid)
ISNELIST → ISQID
U711(tt) → U721(isPal)
ISPAL → ISNEPAL
ISLIST → U211(isList)
ISPAL → U811(isNePal)
ISLIST → ISNELIST

The TRS R consists of the following rules:

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U71(isQid)
isPal → U81(isNePal)
isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 9 less nodes.

↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                        ↳ UsableRulesProof
                      ↳ QDP
  ↳ Zantema-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNEPAL → U711(isQid)
ISPAL → ISNEPAL
U711(tt) → ISPAL

The TRS R consists of the following rules:

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U71(isQid)
isPal → U81(isNePal)
isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ MNOCProof
                      ↳ QDP
  ↳ Zantema-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNEPAL → U711(isQid)
ISPAL → ISNEPAL
U711(tt) → ISPAL

The TRS R consists of the following rules:

isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the modular non-overlap check [15] to enlarge Q to all left-hand sides of R.

↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ MNOCProof
                              ↳ QDP
                                ↳ Rewriting
                      ↳ QDP
  ↳ Zantema-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNEPAL → U711(isQid)
ISPAL → ISNEPAL
U711(tt) → ISPAL

The TRS R consists of the following rules:

isQid → tt

The set Q consists of the following terms:

isQid

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule ISNEPAL → U711(isQid) at position [0] we obtained the following new rules:

ISNEPAL → U711(tt)



↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ MNOCProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ UsableRulesProof
                      ↳ QDP
  ↳ Zantema-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISPAL → ISNEPAL
ISNEPAL → U711(tt)
U711(tt) → ISPAL

The TRS R consists of the following rules:

isQid → tt

The set Q consists of the following terms:

isQid

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ MNOCProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ UsableRulesProof
                                      ↳ QDP
                                        ↳ QReductionProof
                      ↳ QDP
  ↳ Zantema-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISPAL → ISNEPAL
ISNEPAL → U711(tt)
U711(tt) → ISPAL

R is empty.
The set Q consists of the following terms:

isQid

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

isQid



↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ MNOCProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ UsableRulesProof
                                      ↳ QDP
                                        ↳ QReductionProof
                                          ↳ QDP
                                            ↳ NonTerminationProof
                      ↳ QDP
  ↳ Zantema-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISPAL → ISNEPAL
ISNEPAL → U711(tt)
U711(tt) → ISPAL

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

ISPAL → ISNEPAL
ISNEPAL → U711(tt)
U711(tt) → ISPAL

The TRS R consists of the following rules:none


s = ISNEPAL evaluates to t =ISNEPAL

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

ISNEPAL → U711(tt)
with rule ISNEPAL → U711(tt) at position [] and matcher [ ]

U711(tt) → ISPAL
with rule U711(tt) → ISPAL at position [] and matcher [ ]

ISPAL → ISNEPAL
with rule ISPAL → ISNEPAL

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.





↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
  ↳ Zantema-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNELIST → U511(isNeList)
U211(tt) → ISLIST
ISNELIST → ISNELIST
ISLIST → ISLIST
U411(tt) → ISNELIST
ISNELIST → U411(isList)
ISNELIST → ISLIST
ISLIST → U211(isList)
U511(tt) → ISLIST
ISLIST → ISNELIST

The TRS R consists of the following rules:

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U71(isQid)
isPal → U81(isNePal)
isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ Narrowing
  ↳ Zantema-Transformation

Q DP problem:
The TRS P consists of the following rules:

ISNELIST → U511(isNeList)
U211(tt) → ISLIST
U411(tt) → ISNELIST
ISLIST → ISLIST
ISNELIST → ISNELIST
ISNELIST → U411(isList)
ISNELIST → ISLIST
ISLIST → U211(isList)
U511(tt) → ISLIST
ISLIST → ISNELIST

The TRS R consists of the following rules:

isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
U51(tt) → U52(isList)
isList → U11(isNeList)
isList → tt
isList → U21(isList)
U52(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U11(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
isQid → tt
U31(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISNELIST → U511(isNeList) at position [0] we obtained the following new rules:

ISNELIST → U511(U31(isQid))
ISNELIST → U511(U41(isList))
ISNELIST → U511(U51(isNeList))



↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
  ↳ Zantema-Transformation

Q DP problem:
The TRS P consists of the following rules:

U211(tt) → ISLIST
U411(tt) → ISNELIST
ISNELIST → ISNELIST
ISNELIST → U511(U41(isList))
ISNELIST → ISLIST
U511(tt) → ISLIST
ISNELIST → U511(U51(isNeList))
ISLIST → ISLIST
ISNELIST → U411(isList)
ISNELIST → U511(U31(isQid))
ISLIST → U211(isList)
ISLIST → ISNELIST

The TRS R consists of the following rules:

isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
U51(tt) → U52(isList)
isList → U11(isNeList)
isList → tt
isList → U21(isList)
U52(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U11(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
isQid → tt
U31(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISNELIST → U411(isList) at position [0] we obtained the following new rules:

ISNELIST → U411(U21(isList))
ISNELIST → U411(U11(isNeList))
ISNELIST → U411(tt)



↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
  ↳ Zantema-Transformation

Q DP problem:
The TRS P consists of the following rules:

U211(tt) → ISLIST
ISNELIST → ISNELIST
U411(tt) → ISNELIST
ISNELIST → U511(U41(isList))
ISNELIST → ISLIST
U511(tt) → ISLIST
ISNELIST → U511(U51(isNeList))
ISNELIST → U411(U21(isList))
ISLIST → ISLIST
ISNELIST → U511(U31(isQid))
ISNELIST → U411(U11(isNeList))
ISLIST → U211(isList)
ISNELIST → U411(tt)
ISLIST → ISNELIST

The TRS R consists of the following rules:

isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
U51(tt) → U52(isList)
isList → U11(isNeList)
isList → tt
isList → U21(isList)
U52(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U11(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
isQid → tt
U31(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISLIST → U211(isList) at position [0] we obtained the following new rules:

ISLIST → U211(U11(isNeList))
ISLIST → U211(U21(isList))
ISLIST → U211(tt)



↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Narrowing
                                  ↳ QDP
                                    ↳ Narrowing
                                      ↳ QDP
                                        ↳ NonTerminationProof
  ↳ Zantema-Transformation

Q DP problem:
The TRS P consists of the following rules:

U211(tt) → ISLIST
U411(tt) → ISNELIST
ISNELIST → ISNELIST
ISNELIST → U511(U41(isList))
ISNELIST → ISLIST
U511(tt) → ISLIST
ISNELIST → U511(U51(isNeList))
ISLIST → ISLIST
ISNELIST → U411(U21(isList))
ISNELIST → U511(U31(isQid))
ISNELIST → U411(U11(isNeList))
ISLIST → U211(U11(isNeList))
ISLIST → U211(U21(isList))
ISNELIST → U411(tt)
ISLIST → U211(tt)
ISLIST → ISNELIST

The TRS R consists of the following rules:

isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
U51(tt) → U52(isList)
isList → U11(isNeList)
isList → tt
isList → U21(isList)
U52(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U11(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
isQid → tt
U31(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

U211(tt) → ISLIST
U411(tt) → ISNELIST
ISNELIST → ISNELIST
ISNELIST → U511(U41(isList))
ISNELIST → ISLIST
U511(tt) → ISLIST
ISNELIST → U511(U51(isNeList))
ISLIST → ISLIST
ISNELIST → U411(U21(isList))
ISNELIST → U511(U31(isQid))
ISNELIST → U411(U11(isNeList))
ISLIST → U211(U11(isNeList))
ISLIST → U211(U21(isList))
ISNELIST → U411(tt)
ISLIST → U211(tt)
ISLIST → ISNELIST

The TRS R consists of the following rules:

isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
U51(tt) → U52(isList)
isList → U11(isNeList)
isList → tt
isList → U21(isList)
U52(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U11(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
isQid → tt
U31(tt) → tt


s = ISNELIST evaluates to t =ISNELIST

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from ISNELIST to ISNELIST.




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

↳ CSR
  ↳ Lucas-Transformation
  ↳ 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
U11(tt) → tt
U21(tt, V2) → U22(isList(a(V2)))
U22(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNeList(a(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isList(a(V2)))
U52(tt) → tt
U61(tt) → tt
U71(tt, P) → U72(isPal(a(P)))
U72(tt) → tt
U81(tt) → tt
isList(V) → U11(isNeList(a(V)))
isList(nilInact) → tt
isList(__Inact(V1, V2)) → U21(isList(a(V1)), a(V2))
isNeList(V) → U31(isQid(a(V)))
isNeList(__Inact(V1, V2)) → U41(isList(a(V1)), a(V2))
isNeList(__Inact(V1, V2)) → U51(isNeList(a(V1)), a(V2))
isNePal(V) → U61(isQid(a(V)))
isNePal(__Inact(I, __(P, I))) → U71(isQid(a(I)), a(P))
isPal(V) → U81(isNePal(a(V)))
isPal(nilInact) → tt
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u

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
U11(tt) → tt
U21(tt, V2) → U22(isList(a(V2)))
U22(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNeList(a(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isList(a(V2)))
U52(tt) → tt
U61(tt) → tt
U71(tt, P) → U72(isPal(a(P)))
U72(tt) → tt
U81(tt) → tt
isList(V) → U11(isNeList(a(V)))
isList(nilInact) → tt
isList(__Inact(V1, V2)) → U21(isList(a(V1)), a(V2))
isNeList(V) → U31(isQid(a(V)))
isNeList(__Inact(V1, V2)) → U41(isList(a(V1)), a(V2))
isNeList(__Inact(V1, V2)) → U51(isNeList(a(V1)), a(V2))
isNePal(V) → U61(isQid(a(V)))
isNePal(__Inact(I, __(P, I))) → U71(isQid(a(I)), a(P))
isPal(V) → U81(isNePal(a(V)))
isPal(nilInact) → tt
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u

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
U22(tt) → tt
U41(tt, V2) → U42(isNeList(a(V2)))
U52(tt) → tt
isList(nilInact) → tt
isNePal(V) → U61(isQid(a(V)))
isNePal(__Inact(I, __(P, I))) → U71(isQid(a(I)), a(P))
isPal(nilInact) → tt
isQid(aInact) → tt
isQid(eInact) → tt
isQid(iInact) → tt
isQid(oInact) → tt
isQid(uInact) → tt
Used ordering:
Polynomial interpretation [25]:

POL(U11(x1)) = x1   
POL(U21(x1, x2)) = x1 + 2·x2   
POL(U22(x1)) = 1 + x1   
POL(U31(x1)) = x1   
POL(U41(x1, x2)) = x1 + 2·x2   
POL(U42(x1)) = x1   
POL(U51(x1, x2)) = x1 + 2·x2   
POL(U52(x1)) = 1 + x1   
POL(U61(x1)) = x1   
POL(U71(x1, x2)) = 1 + x1 + 2·x2   
POL(U72(x1)) = x1   
POL(U81(x1)) = x1   
POL(__(x1, x2)) = x1 + x2   
POL(__Inact(x1, x2)) = x1 + x2   
POL(a) = 1   
POL(a(x1)) = x1   
POL(aInact) = 1   
POL(e) = 2   
POL(eInact) = 2   
POL(i) = 1   
POL(iInact) = 1   
POL(isList(x1)) = 2·x1   
POL(isNeList(x1)) = 2·x1   
POL(isNePal(x1)) = 2 + 2·x1   
POL(isPal(x1)) = 2 + 2·x1   
POL(isQid(x1)) = 2·x1   
POL(nil) = 2   
POL(nilInact) = 2   
POL(o) = 1   
POL(oInact) = 1   
POL(tt) = 1   
POL(u) = 1   
POL(uInact) = 1   




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

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

__(__(X, Y), Z) → __(X, __(Y, Z))
U11(tt) → tt
U21(tt, V2) → U22(isList(a(V2)))
U31(tt) → tt
U42(tt) → tt
U51(tt, V2) → U52(isList(a(V2)))
U61(tt) → tt
U71(tt, P) → U72(isPal(a(P)))
U72(tt) → tt
U81(tt) → tt
isList(V) → U11(isNeList(a(V)))
isList(__Inact(V1, V2)) → U21(isList(a(V1)), a(V2))
isNeList(V) → U31(isQid(a(V)))
isNeList(__Inact(V1, V2)) → U41(isList(a(V1)), a(V2))
isNeList(__Inact(V1, V2)) → U51(isNeList(a(V1)), a(V2))
isPal(V) → U81(isNePal(a(V)))
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u

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))
U11(tt) → tt
U21(tt, V2) → U22(isList(a(V2)))
U31(tt) → tt
U42(tt) → tt
U51(tt, V2) → U52(isList(a(V2)))
U61(tt) → tt
U71(tt, P) → U72(isPal(a(P)))
U72(tt) → tt
U81(tt) → tt
isList(V) → U11(isNeList(a(V)))
isList(__Inact(V1, V2)) → U21(isList(a(V1)), a(V2))
isNeList(V) → U31(isQid(a(V)))
isNeList(__Inact(V1, V2)) → U41(isList(a(V1)), a(V2))
isNeList(__Inact(V1, V2)) → U51(isNeList(a(V1)), a(V2))
isPal(V) → U81(isNePal(a(V)))
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u

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

U42(tt) → tt
Used ordering:
Polynomial interpretation [25]:

POL(U11(x1)) = x1   
POL(U21(x1, x2)) = x1 + x2   
POL(U22(x1)) = x1   
POL(U31(x1)) = x1   
POL(U41(x1, x2)) = 2·x1 + x2   
POL(U42(x1)) = 2 + x1   
POL(U51(x1, x2)) = x1 + x2   
POL(U52(x1)) = x1   
POL(U61(x1)) = 2·x1   
POL(U71(x1, x2)) = 2·x1 + 2·x2   
POL(U72(x1)) = x1   
POL(U81(x1)) = x1   
POL(__(x1, x2)) = 2·x1 + x2   
POL(__Inact(x1, x2)) = 2·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)) = x1   
POL(isNeList(x1)) = x1   
POL(isNePal(x1)) = 2·x1   
POL(isPal(x1)) = 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
  ↳ Lucas-Transformation
  ↳ 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))
U11(tt) → tt
U21(tt, V2) → U22(isList(a(V2)))
U31(tt) → tt
U51(tt, V2) → U52(isList(a(V2)))
U61(tt) → tt
U71(tt, P) → U72(isPal(a(P)))
U72(tt) → tt
U81(tt) → tt
isList(V) → U11(isNeList(a(V)))
isList(__Inact(V1, V2)) → U21(isList(a(V1)), a(V2))
isNeList(V) → U31(isQid(a(V)))
isNeList(__Inact(V1, V2)) → U41(isList(a(V1)), a(V2))
isNeList(__Inact(V1, V2)) → U51(isNeList(a(V1)), a(V2))
isPal(V) → U81(isNePal(a(V)))
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u

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))
U11(tt) → tt
U21(tt, V2) → U22(isList(a(V2)))
U31(tt) → tt
U51(tt, V2) → U52(isList(a(V2)))
U61(tt) → tt
U71(tt, P) → U72(isPal(a(P)))
U72(tt) → tt
U81(tt) → tt
isList(V) → U11(isNeList(a(V)))
isList(__Inact(V1, V2)) → U21(isList(a(V1)), a(V2))
isNeList(V) → U31(isQid(a(V)))
isNeList(__Inact(V1, V2)) → U41(isList(a(V1)), a(V2))
isNeList(__Inact(V1, V2)) → U51(isNeList(a(V1)), a(V2))
isPal(V) → U81(isNePal(a(V)))
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u

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

U51(tt, V2) → U52(isList(a(V2)))
U61(tt) → tt
U71(tt, P) → U72(isPal(a(P)))
U72(tt) → tt
U81(tt) → tt
Used ordering:
Polynomial interpretation [25]:

POL(U11(x1)) = x1   
POL(U21(x1, x2)) = x1 + 2·x2   
POL(U22(x1)) = 1 + x1   
POL(U31(x1)) = x1   
POL(U41(x1, x2)) = x1 + 2·x2   
POL(U51(x1, x2)) = x1 + 2·x2   
POL(U52(x1)) = x1   
POL(U61(x1)) = 2 + 2·x1   
POL(U71(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(U72(x1)) = 1 + x1   
POL(U81(x1)) = 2·x1   
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·x1   
POL(isNeList(x1)) = 2·x1   
POL(isNePal(x1)) = x1   
POL(isPal(x1)) = 2·x1   
POL(isQid(x1)) = 2·x1   
POL(nil) = 0   
POL(nilInact) = 0   
POL(o) = 0   
POL(oInact) = 0   
POL(tt) = 1   
POL(u) = 0   
POL(uInact) = 0   




↳ CSR
  ↳ Lucas-Transformation
  ↳ 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))
U11(tt) → tt
U21(tt, V2) → U22(isList(a(V2)))
U31(tt) → tt
isList(V) → U11(isNeList(a(V)))
isList(__Inact(V1, V2)) → U21(isList(a(V1)), a(V2))
isNeList(V) → U31(isQid(a(V)))
isNeList(__Inact(V1, V2)) → U41(isList(a(V1)), a(V2))
isNeList(__Inact(V1, V2)) → U51(isNeList(a(V1)), a(V2))
isPal(V) → U81(isNePal(a(V)))
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u

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))
U11(tt) → tt
U21(tt, V2) → U22(isList(a(V2)))
U31(tt) → tt
isList(V) → U11(isNeList(a(V)))
isList(__Inact(V1, V2)) → U21(isList(a(V1)), a(V2))
isNeList(V) → U31(isQid(a(V)))
isNeList(__Inact(V1, V2)) → U41(isList(a(V1)), a(V2))
isNeList(__Inact(V1, V2)) → U51(isNeList(a(V1)), a(V2))
isPal(V) → U81(isNePal(a(V)))
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u

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(V) → U81(isNePal(a(V)))
Used ordering:
Polynomial interpretation [25]:

POL(U11(x1)) = x1   
POL(U21(x1, x2)) = 2·x1 + 2·x2   
POL(U22(x1)) = x1   
POL(U31(x1)) = x1   
POL(U41(x1, x2)) = x1 + 2·x2   
POL(U51(x1, x2)) = x1 + 2·x2   
POL(U81(x1)) = x1   
POL(__(x1, x2)) = 2·x1 + x2   
POL(__Inact(x1, x2)) = 2·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·x1   
POL(isNeList(x1)) = 2·x1   
POL(isNePal(x1)) = 2·x1   
POL(isPal(x1)) = 1 + 2·x1   
POL(isQid(x1)) = 2·x1   
POL(nil) = 0   
POL(nilInact) = 0   
POL(o) = 0   
POL(oInact) = 0   
POL(tt) = 0   
POL(u) = 0   
POL(uInact) = 0   




↳ CSR
  ↳ Lucas-Transformation
  ↳ 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))
U11(tt) → tt
U21(tt, V2) → U22(isList(a(V2)))
U31(tt) → tt
isList(V) → U11(isNeList(a(V)))
isList(__Inact(V1, V2)) → U21(isList(a(V1)), a(V2))
isNeList(V) → U31(isQid(a(V)))
isNeList(__Inact(V1, V2)) → U41(isList(a(V1)), a(V2))
isNeList(__Inact(V1, V2)) → U51(isNeList(a(V1)), a(V2))
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u

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))
U11(tt) → tt
U21(tt, V2) → U22(isList(a(V2)))
U31(tt) → tt
isList(V) → U11(isNeList(a(V)))
isList(__Inact(V1, V2)) → U21(isList(a(V1)), a(V2))
isNeList(V) → U31(isQid(a(V)))
isNeList(__Inact(V1, V2)) → U41(isList(a(V1)), a(V2))
isNeList(__Inact(V1, V2)) → U51(isNeList(a(V1)), a(V2))
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u

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))
U21(tt, V2) → U22(isList(a(V2)))
isList(__Inact(V1, V2)) → U21(isList(a(V1)), a(V2))
isNeList(__Inact(V1, V2)) → U41(isList(a(V1)), a(V2))
isNeList(__Inact(V1, V2)) → U51(isNeList(a(V1)), a(V2))
Used ordering:
Polynomial interpretation [25]:

POL(U11(x1)) = x1   
POL(U21(x1, x2)) = 1 + 2·x1 + x2   
POL(U22(x1)) = 2 + x1   
POL(U31(x1)) = x1   
POL(U41(x1, x2)) = 1 + 2·x1 + x2   
POL(U51(x1, x2)) = 1 + 2·x1 + x2   
POL(__(x1, x2)) = 2 + 2·x1 + x2   
POL(__Inact(x1, x2)) = 2 + 2·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)) = x1   
POL(isNeList(x1)) = x1   
POL(isQid(x1)) = x1   
POL(nil) = 1   
POL(nilInact) = 1   
POL(o) = 0   
POL(oInact) = 0   
POL(tt) = 2   
POL(u) = 0   
POL(uInact) = 0   




↳ CSR
  ↳ Lucas-Transformation
  ↳ 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:

U11(tt) → tt
U31(tt) → tt
isList(V) → U11(isNeList(a(V)))
isNeList(V) → U31(isQid(a(V)))
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u

Q is empty.

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

U11(tt) → tt
U31(tt) → tt
isList(V) → U11(isNeList(a(V)))
isNeList(V) → U31(isQid(a(V)))
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u

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

U11(tt) → tt
isList(V) → U11(isNeList(a(V)))
Used ordering:
Polynomial interpretation [25]:

POL(U11(x1)) = 1 + x1   
POL(U31(x1)) = 2·x1   
POL(__(x1, x2)) = x1 + x2   
POL(__Inact(x1, x2)) = x1 + x2   
POL(a) = 0   
POL(a(x1)) = x1   
POL(aInact) = 0   
POL(e) = 1   
POL(eInact) = 1   
POL(i) = 0   
POL(iInact) = 0   
POL(isList(x1)) = 2 + 2·x1   
POL(isNeList(x1)) = 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
  ↳ Lucas-Transformation
  ↳ 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:

U31(tt) → tt
isNeList(V) → U31(isQid(a(V)))
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u

Q is empty.

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

U31(tt) → tt
isNeList(V) → U31(isQid(a(V)))
a(x) → x
a → aInact
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
a(iInact) → i
nil → nilInact
a(nilInact) → nil
o → oInact
a(oInact) → o
e → eInact
a(eInact) → e
u → uInact
a(uInact) → u

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
a → aInact
a(__Inact(x1, x2)) → __(x1, x2)
i → iInact
nil → nilInact
o → oInact
a(oInact) → o
a(eInact) → e
u → uInact
Used ordering:
Polynomial interpretation [25]:

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




↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ 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:

U31(tt) → tt
isNeList(V) → U31(isQid(a(V)))
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(iInact) → i
a(nilInact) → nil
e → eInact
a(uInact) → u

Q is empty.

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

U31(tt) → tt
isNeList(V) → U31(isQid(a(V)))
a(aInact) → a
__(x1, x2) → __Inact(x1, x2)
a(iInact) → i
a(nilInact) → nil
e → eInact
a(uInact) → u

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

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

POL(U31(x1)) = 1 + 2·x1   
POL(__(x1, x2)) = 2 + 2·x1 + x2   
POL(__Inact(x1, x2)) = 1 + x1 + x2   
POL(a) = 1   
POL(a(x1)) = x1   
POL(aInact) = 2   
POL(e) = 2   
POL(eInact) = 2   
POL(i) = 1   
POL(iInact) = 2   
POL(isNeList(x1)) = 2 + 2·x1   
POL(isQid(x1)) = x1   
POL(nil) = 1   
POL(nilInact) = 2   
POL(tt) = 2   
POL(u) = 0   
POL(uInact) = 0   




↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ 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:

e → eInact
a(uInact) → u

Q is empty.

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

e → eInact
a(uInact) → u

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

e → eInact
a(uInact) → u
Used ordering:
Polynomial interpretation [25]:

POL(a(x1)) = 2 + 2·x1   
POL(e) = 2   
POL(eInact) = 1   
POL(u) = 1   
POL(uInact) = 2   




↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ 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.