Termination Proof using AProVE

YES Termination Proof using AProVETerm Rewriting System R:
[X, Y, Z, V2, P, V, V1, I]
((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

Termination of R to be shown.

TRS

     ↳CSR to TRS Transformation

     ↳CSRtoTRS

Lucas-Transformation successful.
Replacement map:

U71(1, 2)
U42(1)
U52(1)
U11(1)
U51(1, 2)
U21(1, 2)
U72(1)
isNePal(1)
isNeList(1)
U31(1)
(1, 2)
U22(1)
U81(1)
isPal(1)
U41(1, 2)
U61(1)
isList(1)
isQid(1)

Old CSR:

((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

new TRS:

((X, Y), Z) -> (X, (Y, Z))
(X, nil) -> X
(nil, X) -> X
U11(tt) -> tt
U21(tt) -> U22(isList)
U22(tt) -> tt
isList -> U11(isNeList)
isList -> tt
isList -> U21(isList)
U31(tt) -> tt
U41(tt) -> U42(isNeList)
U42(tt) -> tt
isNeList -> U31(isQid)
isNeList -> U41(isList)
isNeList -> U51(isNeList)
U51(tt) -> U52(isList)
U52(tt) -> tt
U61(tt) -> tt
U71(tt) -> U72(isPal)
U72(tt) -> tt
isPal -> U81(isNePal)
isPal -> tt
U81(tt) -> tt
isQid -> tt
isNePal -> U61(isQid)
isNePal -> U71(isQid)

TRS

     ↳CSRtoTRS

       →TRS1

         ↳Removing Redundant Rules

     ↳CSRtoTRS

Removing the following rules from R which fullfill a polynomial ordering:

((X, Y), Z) -> (X, (Y, Z))
(X, nil) -> X
(nil, X) -> X

where the Polynomial interpretation:

POL(U71(x₁)) = x₁

POL(U31(x₁)) = x₁

POL(U42(x₁)) = x₁

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

POL(U52(x₁)) = x₁

POL(U11(x₁)) = x₁

POL(U22(x₁)) = x₁

POL(U81(x₁)) = x₁

POL(U51(x₁)) = x₁

POL(isPal) = 0

POL(U41(x₁)) = x₁

POL(U21(x₁)) = x₁

POL(tt) = 0

POL(nil) = 0

POL(U72(x₁)) = x₁

POL(U61(x₁)) = x₁

POL(isNePal) = 0

POL(isList) = 0

POL(isQid) = 0

POL(isNeList) = 0

was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

TRS

     ↳CSRtoTRS

       →TRS1

         ↳RRRPolo

           →TRS2

             ↳Removing Redundant Rules

     ↳CSRtoTRS

Removing the following rules from R which fullfill a polynomial ordering:

U61(tt) -> tt
isPal -> tt

where the Polynomial interpretation:

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

POL(U31(x₁)) = x₁

POL(U42(x₁)) = x₁

POL(U52(x₁)) = x₁

POL(U11(x₁)) = x₁

POL(U22(x₁)) = x₁

POL(U81(x₁)) = x₁

POL(U51(x₁)) = x₁

POL(isPal) = 1

POL(U41(x₁)) = x₁

POL(U21(x₁)) = x₁

POL(tt) = 0

POL(U72(x₁)) = x₁

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

POL(isNePal) = 1

POL(isList) = 0

POL(isQid) = 0

POL(isNeList) = 0

was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

TRS

     ↳CSRtoTRS

       →TRS1

         ↳RRRPolo

           →TRS2

             ↳RRRPolo

...

               →TRS3

                 ↳Removing Redundant Rules

     ↳CSRtoTRS

Removing the following rules from R which fullfill a polynomial ordering:

isNePal -> U61(isQid)

where the Polynomial interpretation:

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

POL(U31(x₁)) = x₁

POL(U42(x₁)) = x₁

POL(U52(x₁)) = x₁

POL(U11(x₁)) = x₁

POL(U22(x₁)) = x₁

POL(U81(x₁)) = x₁

POL(U51(x₁)) = x₁

POL(isPal) = 1

POL(U41(x₁)) = x₁

POL(U21(x₁)) = x₁

POL(tt) = 0

POL(U72(x₁)) = x₁

POL(isNePal) = 1

POL(U61(x₁)) = x₁

POL(isList) = 0

POL(isNeList) = 0

POL(isQid) = 0

was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

TRS

     ↳CSRtoTRS

       →TRS1

         ↳RRRPolo

           →TRS2

             ↳RRRPolo

...

               →TRS4

                 ↳Dependency Pair Analysis

     ↳CSRtoTRS

R contains the following Dependency Pairs:

ISPAL -> U81'(isNePal)
ISPAL -> ISNEPAL
ISNEPAL -> U71'(isQid)
ISNEPAL -> ISQID
U71'(tt) -> U72'(isPal)
U71'(tt) -> ISPAL
U51'(tt) -> U52'(isList)
U51'(tt) -> ISLIST
ISLIST -> U11'(isNeList)
ISLIST -> ISNELIST
ISLIST -> U21'(isList)
ISLIST -> ISLIST
ISNELIST -> U31'(isQid)
ISNELIST -> ISQID
ISNELIST -> U41'(isList)
ISNELIST -> ISLIST
ISNELIST -> U51'(isNeList)
ISNELIST -> ISNELIST
U21'(tt) -> U22'(isList)
U21'(tt) -> ISLIST
U41'(tt) -> U42'(isNeList)
U41'(tt) -> ISNELIST

Furthermore, R contains two SCCs.

TRS

     ↳CSRtoTRS

       →TRS1

         ↳RRRPolo

           →TRS2

             ↳RRRPolo

...

               →DP Problem 1

                 ↳Modular Removal of Rules

     ↳CSRtoTRS

Dependency Pairs:

U71'(tt) -> ISPAL
ISNEPAL -> U71'(isQid)
ISPAL -> ISNEPAL

Rules:

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

We have the following set of usable rules:

isQid -> tt

To remove rules and DPs from this DP problem we used the following monotonic and C_E-compatible order: Polynomial ordering.
Polynomial interpretation:

POL(ISPAL) = 0

POL(U71'(x₁)) = x₁

POL(ISNEPAL) = 0

POL(tt) = 0

POL(isQid) = 0

We have the following set D of usable symbols: {ISPAL, U71', ISNEPAL, tt, isQid}
No Dependency Pairs can be deleted.
19 non usable rules have been deleted.

The result of this processor delivers one new DP problem.

TRS

     ↳CSRtoTRS

       →TRS1

         ↳RRRPolo

           →TRS2

             ↳RRRPolo

...

               →DP Problem 3

                 ↳Non-Overlappingness Check

     ↳CSRtoTRS

Dependency Pairs:

U71'(tt) -> ISPAL
ISNEPAL -> U71'(isQid)
ISPAL -> ISNEPAL

Rule:

isQid -> tt

R does not overlap into P. Moreover, R is locally confluent (all critical pairs are trivially joinable). Hence we can switch to innermost.
The transformation is resulting in one subcycle:

TRS

     ↳CSRtoTRS

       →TRS1

         ↳RRRPolo

           →TRS2

             ↳RRRPolo

...

               →DP Problem 4

                 ↳Rewriting Transformation

     ↳CSRtoTRS

Dependency Pairs:

U71'(tt) -> ISPAL
ISNEPAL -> U71'(isQid)
ISPAL -> ISNEPAL

Rule:

isQid -> tt

Strategy:

innermost

On this DP problem, a Rewriting SCC transformation can be performed.
As a result of transforming the rule

ISNEPAL -> U71'(isQid)

one new Dependency Pair is created:

ISNEPAL -> U71'(tt)

The transformation is resulting in one new DP problem:

TRS

     ↳CSRtoTRS

       →TRS1

         ↳RRRPolo

           →TRS2

             ↳RRRPolo

...

               →DP Problem 5

                 ↳Usable Rules (Innermost)

     ↳CSRtoTRS

Dependency Pairs:

ISNEPAL -> U71'(tt)
ISPAL -> ISNEPAL
U71'(tt) -> ISPAL

Rule:

isQid -> tt

Strategy:

innermost

As we are in the innermost case, we can delete all 1 non-usable-rules.

TRS

     ↳CSRtoTRS

       →TRS1

         ↳RRRPolo

           →TRS2

             ↳RRRPolo

...

               →DP Problem 6

                 ↳Non Termination

     ↳CSRtoTRS

Dependency Pairs:

ISNEPAL -> U71'(tt)
ISPAL -> ISNEPAL
U71'(tt) -> ISPAL

Rule:

none

Strategy:

innermost

Found an infinite P-chain over R:
P =

ISNEPAL -> U71'(tt)
ISPAL -> ISNEPAL
U71'(tt) -> ISPAL

R = none

s = U71'(tt)
evaluates to t =U71'(tt)

Thus, s starts an infinite chain.

Trying another alternative:

TRS

     ↳CSRtoTRS

     ↳CSR to TRS Transformation

Zantema-Transformation successful.
Replacement map:

U71(1, 2)
U42(1)
U52(1)
U11(1)
U51(1, 2)
U21(1, 2)
U72(1)
isNePal(1)
isNeList(1)
U31(1)
(1, 2)
U22(1)
U81(1)
isPal(1)
U41(1, 2)
U61(1)
isList(1)
isQid(1)

Old CSR:

((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

new TRS:

((X, Y), Z) -> (X, (Y, Z))
(X, nil) -> X
(nil, X) -> X
(x0, x1) -> (x0, x1)
nil -> nil
U11(tt) -> tt
U21(tt, V2) -> U22(isList(a(V2)))
U22(tt) -> tt
isList(V) -> U11(isNeList(a(V)))
isList(nil) -> tt
isList((V1, V2)) -> U21(isList(a(V1)), a(V2))
a(i) -> i
a(e) -> e
a((x0, x1)) -> (x0, x1)
a(o) -> o
a(nil) -> nil
a(a) -> a
a(u) -> u
U31(tt) -> tt
U41(tt, V2) -> U42(isNeList(a(V2)))
U42(tt) -> tt
isNeList(V) -> U31(isQid(a(V)))
isNeList((V1, V2)) -> U41(isList(a(V1)), a(V2))
isNeList((V1, V2)) -> U51(isNeList(a(V1)), a(V2))
U51(tt, V2) -> U52(isList(a(V2)))
U52(tt) -> tt
U61(tt) -> tt
U71(tt, P) -> U72(isPal(a(P)))
U72(tt) -> tt
isPal(V) -> U81(isNePal(a(V)))
isPal(nil) -> tt
U81(tt) -> tt
isQid(a) -> tt
isQid(e) -> tt
isQid(i) -> tt
isQid(o) -> tt
isQid(u) -> tt
isNePal(V) -> U61(isQid(a(V)))
isNePal((I, (P, I))) -> U71(isQid(a(I)), a(P))
i -> i
e -> e
o -> o
a -> a
u -> u

TRS

     ↳CSRtoTRS

     ↳CSRtoTRS

       →TRS5

         ↳Removing Redundant Rules

Removing the following rules from R which fullfill a polynomial ordering:

((X, Y), Z) -> (X, (Y, Z))
(X, nil) -> X
(nil, X) -> X
isList((V1, V2)) -> U21(isList(a(V1)), a(V2))
isNeList((V1, V2)) -> U41(isList(a(V1)), a(V2))
isNeList((V1, V2)) -> U51(isNeList(a(V1)), a(V2))
isNePal((I, (P, I))) -> U71(isQid(a(I)), a(P))

where the Polynomial interpretation:

POL(U71(x₁, x₂)) = x₁ + x₂

POL(i) = 0

POL(U42(x₁)) = x₁

POL(U52(x₁)) = x₁

POL(U11(x₁)) = x₁

POL(_i_) = 0

POL(U51(x₁, x₂)) = x₁ + x₂

POL(*a*(x₁)) = x₁

POL(U21(x₁, x₂)) = x₁ + x₂

POL(nil) = 0

POL(U72(x₁)) = x₁

POL(isNePal(x₁)) = x₁

POL(_o_) = 0

POL(isNeList(x₁)) = x₁

POL(____(x₁, x₂)) = 1 + 2·x₁ + x₂

POL(U31(x₁)) = x₁

POL(e) = 0

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

POL(_u_) = 0

POL(U22(x₁)) = x₁

POL(u) = 0

POL(U81(x₁)) = x₁

POL(_e_) = 0

POL(_nil_) = 0

POL(isPal(x₁)) = x₁

POL(U41(x₁, x₂)) = x₁ + x₂

POL(o) = 0

POL(tt) = 0

POL(U61(x₁)) = x₁

POL(a) = 0

POL(isList(x₁)) = x₁

POL(isQid(x₁)) = x₁

POL(_a_) = 0

was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

TRS

     ↳CSRtoTRS

     ↳CSRtoTRS

       →TRS5

         ↳RRRPolo

           →TRS6

             ↳Removing Redundant Rules

Removing the following rules from R which fullfill a polynomial ordering:

isQid(e) -> tt

where the Polynomial interpretation:

POL(U71(x₁, x₂)) = x₁ + x₂

POL(i) = 0

POL(U42(x₁)) = x₁

POL(U52(x₁)) = x₁

POL(U11(x₁)) = x₁

POL(_i_) = 0

POL(U51(x₁, x₂)) = x₁ + x₂

POL(*a*(x₁)) = x₁

POL(U21(x₁, x₂)) = x₁ + x₂

POL(nil) = 0

POL(U72(x₁)) = x₁

POL(isNePal(x₁)) = x₁

POL(_o_) = 0

POL(isNeList(x₁)) = x₁

POL(____(x₁, x₂)) = x₁ + x₂

POL(U31(x₁)) = x₁

POL(e) = 1

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

POL(_u_) = 0

POL(U22(x₁)) = x₁

POL(u) = 0

POL(U81(x₁)) = x₁

POL(_e_) = 1

POL(_nil_) = 0

POL(isPal(x₁)) = x₁

POL(U41(x₁, x₂)) = x₁ + x₂

POL(o) = 0

POL(tt) = 0

POL(U61(x₁)) = x₁

POL(a) = 0

POL(isList(x₁)) = x₁

POL(isQid(x₁)) = x₁

POL(_a_) = 0

was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

TRS

     ↳CSRtoTRS

     ↳CSRtoTRS

       →TRS5

         ↳RRRPolo

           →TRS6

             ↳RRRPolo

...

               →TRS7

                 ↳Removing Redundant Rules

Removing the following rules from R which fullfill a polynomial ordering:

isQid(u) -> tt

where the Polynomial interpretation:

POL(U71(x₁, x₂)) = x₁ + x₂

POL(i) = 0

POL(U42(x₁)) = x₁

POL(U52(x₁)) = x₁

POL(U11(x₁)) = x₁

POL(_i_) = 0

POL(U51(x₁, x₂)) = x₁ + x₂

POL(*a*(x₁)) = x₁

POL(U21(x₁, x₂)) = x₁ + x₂

POL(nil) = 0

POL(U72(x₁)) = x₁

POL(isNePal(x₁)) = x₁

POL(_o_) = 0

POL(isNeList(x₁)) = x₁

POL(____(x₁, x₂)) = x₁ + x₂

POL(U31(x₁)) = x₁

POL(e) = 0

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

POL(_u_) = 1

POL(U22(x₁)) = x₁

POL(u) = 1

POL(U81(x₁)) = x₁

POL(_e_) = 0

POL(_nil_) = 0

POL(isPal(x₁)) = x₁

POL(U41(x₁, x₂)) = x₁ + x₂

POL(o) = 0

POL(tt) = 0

POL(U61(x₁)) = x₁

POL(a) = 0

POL(isList(x₁)) = x₁

POL(isQid(x₁)) = x₁

POL(_a_) = 0

was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

TRS

     ↳CSRtoTRS

     ↳CSRtoTRS

       →TRS5

         ↳RRRPolo

           →TRS6

             ↳RRRPolo

...

               →TRS8

                 ↳Removing Redundant Rules

Removing the following rules from R which fullfill a polynomial ordering:

isList(V) -> U11(isNeList(a(V)))
isList(nil) -> tt

where the Polynomial interpretation:

POL(U71(x₁, x₂)) = x₁ + x₂

POL(i) = 0

POL(U42(x₁)) = x₁

POL(U52(x₁)) = x₁

POL(U11(x₁)) = x₁

POL(_i_) = 0

POL(U51(x₁, x₂)) = 1 + x₁ + x₂

POL(*a*(x₁)) = x₁

POL(U21(x₁, x₂)) = 1 + x₁ + x₂

POL(nil) = 0

POL(U72(x₁)) = x₁

POL(isNePal(x₁)) = x₁

POL(_o_) = 0

POL(isNeList(x₁)) = x₁

POL(____(x₁, x₂)) = x₁ + x₂

POL(U31(x₁)) = x₁

POL(e) = 0

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

POL(_u_) = 0

POL(U22(x₁)) = x₁

POL(u) = 0

POL(U81(x₁)) = x₁

POL(_e_) = 0

POL(_nil_) = 0

POL(isPal(x₁)) = x₁

POL(U41(x₁, x₂)) = x₁ + x₂

POL(o) = 0

POL(tt) = 0

POL(U61(x₁)) = x₁

POL(a) = 0

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

POL(isQid(x₁)) = x₁

POL(_a_) = 0

was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

TRS

     ↳CSRtoTRS

     ↳CSRtoTRS

       →TRS5

         ↳RRRPolo

           →TRS6

             ↳RRRPolo

...

               →TRS9

                 ↳Removing Redundant Rules

Removing the following rules from R which fullfill a polynomial ordering:

U61(tt) -> tt
isPal(nil) -> tt

where the Polynomial interpretation:

POL(U71(x₁, x₂)) = 1 + x₁ + x₂

POL(i) = 0

POL(U42(x₁)) = x₁

POL(U52(x₁)) = x₁

POL(U11(x₁)) = x₁

POL(_i_) = 0

POL(U51(x₁, x₂)) = x₁ + x₂

POL(*a*(x₁)) = x₁

POL(U21(x₁, x₂)) = x₁ + x₂

POL(nil) = 0

POL(U72(x₁)) = x₁

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

POL(_o_) = 0

POL(isNeList(x₁)) = x₁

POL(____(x₁, x₂)) = x₁ + x₂

POL(U31(x₁)) = x₁

POL(e) = 0

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

POL(_u_) = 0

POL(u) = 0

POL(U22(x₁)) = x₁

POL(U81(x₁)) = x₁

POL(_e_) = 0

POL(_nil_) = 0

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

POL(U41(x₁, x₂)) = x₁ + x₂

POL(o) = 0

POL(tt) = 0

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

POL(a) = 0

POL(isList(x₁)) = x₁

POL(isQid(x₁)) = x₁

POL(_a_) = 0

was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

TRS

     ↳CSRtoTRS

     ↳CSRtoTRS

       →TRS5

         ↳RRRPolo

           →TRS6

             ↳RRRPolo

...

               →TRS10

                 ↳Removing Redundant Rules

Removing the following rules from R which fullfill a polynomial ordering:

U52(tt) -> tt

where the Polynomial interpretation:

POL(U71(x₁, x₂)) = x₁ + x₂

POL(i) = 0

POL(U42(x₁)) = x₁

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

POL(U11(x₁)) = x₁

POL(_i_) = 0

POL(U51(x₁, x₂)) = 1 + x₁ + x₂

POL(*a*(x₁)) = x₁

POL(U21(x₁, x₂)) = x₁ + x₂

POL(nil) = 0

POL(U72(x₁)) = x₁

POL(isNePal(x₁)) = x₁

POL(_o_) = 0

POL(isNeList(x₁)) = x₁

POL(____(x₁, x₂)) = x₁ + x₂

POL(U31(x₁)) = x₁

POL(e) = 0

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

POL(_u_) = 0

POL(u) = 0

POL(U22(x₁)) = x₁

POL(U81(x₁)) = x₁

POL(_e_) = 0

POL(_nil_) = 0

POL(isPal(x₁)) = x₁

POL(U41(x₁, x₂)) = x₁ + x₂

POL(tt) = 0

POL(o) = 0

POL(U61(x₁)) = x₁

POL(isList(x₁)) = x₁

POL(a) = 0

POL(isQid(x₁)) = x₁

POL(_a_) = 0

was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

TRS

     ↳CSRtoTRS

     ↳CSRtoTRS

       →TRS5

         ↳RRRPolo

           →TRS6

             ↳RRRPolo

...

               →TRS11

                 ↳Overlay and local confluence Check

The TRS is overlay and locally confluent (all critical pairs are trivially joinable).Hence, we can switch to innermost.

TRS

     ↳CSRtoTRS

     ↳CSRtoTRS

       →TRS5

         ↳RRRPolo

           →TRS6

             ↳RRRPolo

...

               →TRS12

                 ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

A(i) -> I
A(e) -> E
A(a) -> A
A(u) -> U
A(nil) -> NIL
A((x0, x1)) -> _{_'}(x0, x1)
A(o) -> O
ISPAL(V) -> U81'(isNePal(a(V)))
ISPAL(V) -> ISNEPAL(a(V))
ISPAL(V) -> A(V)
ISNEPAL(V) -> ISQID(a(V))
ISNEPAL(V) -> A(V)
U21'(tt, V2) -> U22'(isList(a(V2)))
U21'(tt, V2) -> A(V2)
ISNELIST(V) -> U31'(isQid(a(V)))
ISNELIST(V) -> ISQID(a(V))
ISNELIST(V) -> A(V)
U71'(tt, P) -> U72'(isPal(a(P)))
U71'(tt, P) -> ISPAL(a(P))
U71'(tt, P) -> A(P)
U41'(tt, V2) -> U42'(isNeList(a(V2)))
U41'(tt, V2) -> ISNELIST(a(V2))
U41'(tt, V2) -> A(V2)
U51'(tt, V2) -> A(V2)

R contains no SCCs.

Termination of R successfully shown.
Duration:
0:13 minutes

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

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

POL(ISPAL)	= 0
POL(U71'(x₁))	= x₁
POL(ISNEPAL)	= 0
POL(tt)	= 0
POL(isQid)	= 0

POL(U71(x₁, x₂))	= x₁ + x₂
POL(i)	= 0
POL(U42(x₁))	= x₁
POL(U52(x₁))	= x₁
POL(U11(x₁))	= x₁
POL(_i_)	= 0
POL(U51(x₁, x₂))	= x₁ + x₂
POL(a(x₁))	= x₁
POL(U21(x₁, x₂))	= x₁ + x₂
POL(nil)	= 0
POL(U72(x₁))	= x₁
POL(isNePal(x₁))	= x₁
POL(_o_)	= 0
POL(isNeList(x₁))	= x₁
POL(____(x₁, x₂))	= 1 + 2·x₁ + x₂
POL(U31(x₁))	= x₁
POL(e)	= 0
POL(__(x₁, x₂))	= 1 + 2·x₁ + x₂
POL(_u_)	= 0
POL(U22(x₁))	= x₁
POL(u)	= 0
POL(U81(x₁))	= x₁
POL(_e_)	= 0
POL(_nil_)	= 0
POL(isPal(x₁))	= x₁
POL(U41(x₁, x₂))	= x₁ + x₂
POL(o)	= 0
POL(tt)	= 0
POL(U61(x₁))	= x₁
POL(a)	= 0
POL(isList(x₁))	= x₁
POL(isQid(x₁))	= x₁
POL(_a_)	= 0

POL(U71(x₁, x₂))	= 1 + x₁ + x₂
POL(i)	= 0
POL(U42(x₁))	= x₁
POL(U52(x₁))	= x₁
POL(U11(x₁))	= x₁
POL(_i_)	= 0
POL(U51(x₁, x₂))	= x₁ + x₂
POL(a(x₁))	= x₁
POL(U21(x₁, x₂))	= x₁ + x₂
POL(nil)	= 0
POL(U72(x₁))	= x₁
POL(isNePal(x₁))	= 1 + x₁
POL(_o_)	= 0
POL(isNeList(x₁))	= x₁
POL(____(x₁, x₂))	= x₁ + x₂
POL(U31(x₁))	= x₁
POL(e)	= 0
POL(__(x₁, x₂))	= x₁ + x₂
POL(_u_)	= 0
POL(u)	= 0
POL(U22(x₁))	= x₁
POL(U81(x₁))	= x₁
POL(_e_)	= 0
POL(_nil_)	= 0
POL(isPal(x₁))	= 1 + x₁
POL(U41(x₁, x₂))	= x₁ + x₂
POL(o)	= 0
POL(tt)	= 0
POL(U61(x₁))	= 1 + x₁
POL(a)	= 0
POL(isList(x₁))	= x₁
POL(isQid(x₁))	= x₁
POL(_a_)	= 0