Termination Proof using AProVE

YES Termination Proof using AProVETerm Rewriting System R:
[V2, L, N, V1, V]
zeros -> cons(0, zeros)
U11(tt) -> tt
U21(tt) -> tt
U31(tt) -> tt
U41(tt, V2) -> U42(isNatIList(V2))
U42(tt) -> tt
U51(tt, V2) -> U52(isNatList(V2))
U52(tt) -> tt
U61(tt, L, N) -> U62(isNat(N), L)
U62(tt, L) -> s(length(L))
isNat(0) -> tt
isNat(length(V1)) -> U11(isNatList(V1))
isNat(s(V1)) -> U21(isNat(V1))
isNatIList(V) -> U31(isNatList(V))
isNatIList(zeros) -> tt
isNatIList(cons(V1, V2)) -> U41(isNat(V1), V2)
isNatList(nil) -> tt
isNatList(cons(V1, V2)) -> U51(isNat(V1), V2)
length(nil) -> 0
length(cons(N, L)) -> U61(isNatList(L), L, N)

Termination of R to be shown.

TRS

     ↳CSR to TRS Transformation

incomplete Giesl-Middeldorp-Transformation successful.
Replacement map:

isNatList(1)
U31(1)
U42(1)
U52(1)
U11(1)
isNat(1)
U51(1, 2)
U62(1, 2)
U41(1, 2)
cons(1, 2)
U21(1)
U61(1, 2, 3)
s(1)
length(1)
isNatIList(1)

Old CSR:

zeros -> cons(0, zeros)
U11(tt) -> tt
U21(tt) -> tt
U31(tt) -> tt
U41(tt, V2) -> U42(isNatIList(V2))
U42(tt) -> tt
U51(tt, V2) -> U52(isNatList(V2))
U52(tt) -> tt
U61(tt, L, N) -> U62(isNat(N), L)
U62(tt, L) -> s(length(L))
isNat(0) -> tt
isNat(length(V1)) -> U11(isNatList(V1))
isNat(s(V1)) -> U21(isNat(V1))
isNatIList(V) -> U31(isNatList(V))
isNatIList(zeros) -> tt
isNatIList(cons(V1, V2)) -> U41(isNat(V1), V2)
isNatList(nil) -> tt
isNatList(cons(V1, V2)) -> U51(isNat(V1), V2)
length(nil) -> 0
length(cons(N, L)) -> U61(isNatList(L), L, N)

new TRS:

zeros -> cons(0, zeros)
zeros -> zeros
U11(tt) -> tt
U11(x0) -> U11(x0)
U21(tt) -> tt
U21(x0) -> U21(x0)
U31(tt) -> tt
U31(x0) -> U31(x0)
U41(tt, V2) -> U42(isNatIList(V2))
U41(x0, x1) -> U41(x0, x1)
U42(tt) -> tt
U42(x0) -> U42(x0)
isNatIList(V) -> U31(isNatList(V))
isNatIList(zeros) -> tt
isNatIList(cons(V1, V2)) -> U41(isNat(V1), V2)
isNatIList(x0) -> isNatIList(x0)
U51(tt, V2) -> U52(isNatList(V2))
U51(x0, x1) -> U51(x0, x1)
U52(tt) -> tt
U52(x0) -> U52(x0)
isNatList(nil) -> tt
isNatList(cons(V1, V2)) -> U51(isNat(V1), V2)
isNatList(x0) -> isNatList(x0)
U61(tt, L, N) -> U62(isNat(N), L)
U61(x0, x1, x2) -> U61(x0, x1, x2)
U62(tt, L) -> s(length(mark(L)))
U62(x0, x1) -> U62(x0, x1)
isNat(0) -> tt
isNat(length(V1)) -> U11(isNatList(V1))
isNat(s(V1)) -> U21(isNat(V1))
isNat(x0) -> isNat(x0)
length(nil) -> 0
length(cons(N, L)) -> U61(isNatList(L), L, N)
length(x0) -> length(x0)
mark(isNatList(x0)) -> isNatList(x0)
mark(U31(x0)) -> U31(mark(x0))
mark(U42(x0)) -> U42(mark(x0))
mark(U52(x0)) -> U52(mark(x0))
mark(U11(x0)) -> U11(mark(x0))
mark(isNat(x0)) -> isNat(x0)
mark(U51(x0, x1)) -> U51(mark(x0), x1)
mark(U62(x0, x1)) -> U62(mark(x0), x1)
mark(U41(x0, x1)) -> U41(mark(x0), x1)
mark(U21(x0)) -> U21(mark(x0))
mark(U61(x0, x1, x2)) -> U61(mark(x0), x1, x2)
mark(zeros) -> zeros
mark(length(x0)) -> length(mark(x0))
mark(isNatIList(x0)) -> isNatIList(x0)
mark(cons(x0, x1)) -> cons(mark(x0), x1)
mark(0) -> 0
mark(tt) -> tt
mark(s(x0)) -> s(mark(x0))
mark(nil) -> nil

TRS

     ↳CSRtoTRS

       →TRS1

         ↳Removing Redundant Rules

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

zeros -> cons(0, zeros)
zeros -> zeros
isNatIList(V) -> U31(isNatList(V))
isNatIList(cons(V1, V2)) -> U41(isNat(V1), V2)
isNatIList(x0) -> isNatIList(x0)
U51(tt, V2) -> U52(isNatList(V2))
mark(isNatList(x0)) -> isNatList(x0)
mark(isNat(x0)) -> isNat(x0)
mark(isNatIList(x0)) -> isNatIList(x0)
mark(0) -> 0
mark(tt) -> tt
mark(nil) -> nil

where the Polynomial interpretation:

POL(_U61_(x₁, x₂, x₃)) = x₁ + x₂ + x₃

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

POL(isNatList(x₁)) = x₁

POL(_isNatList_(x₁)) = x₁

POL(_length_(x₁)) = x₁

POL(_U52_(x₁)) = x₁

POL(_U31_(x₁)) = x₁

POL(_isNat_(x₁)) = x₁

POL(U42(x₁)) = x₁

POL(U52(x₁)) = x₁

POL(*mark*(x₁)) = 2 + x₁

POL(U11(x₁)) = x₁

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

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

POL(_zeros_) = 2

POL(_U11_(x₁)) = x₁

POL(cons(x₁, x₂)) = x₁ + 2·x₂

POL(U21(x₁)) = x₁

POL(_U42_(x₁)) = x₁

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

POL(nil) = 1

POL(zeros) = 0

POL(length(x₁)) = x₁

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

POL(_U21_(x₁)) = x₁

POL(U31(x₁)) = x₁

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

POL(isNat(x₁)) = x₁

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

POL(0) = 1

POL(tt) = 1

POL(U61(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(s(x₁)) = x₁

POL(isNatIList(x₁)) = x₁

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

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

isNat(s(V1)) -> U21(isNat(V1))
isNatList(cons(V1, V2)) -> U51(isNat(V1), V2)

where the Polynomial interpretation:

POL(_U61_(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃

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

POL(_isNatList_(x₁)) = x₁

POL(_length_(x₁)) = x₁

POL(isNatList(x₁)) = x₁

POL(_U52_(x₁)) = x₁

POL(_U31_(x₁)) = x₁

POL(_isNat_(x₁)) = x₁

POL(U42(x₁)) = x₁

POL(U52(x₁)) = x₁

POL(*mark*(x₁)) = x₁

POL(U11(x₁)) = x₁

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

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

POL(_zeros_) = 0

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

POL(_U11_(x₁)) = x₁

POL(U21(x₁)) = x₁

POL(_U42_(x₁)) = x₁

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

POL(nil) = 0

POL(zeros) = 0

POL(_isNatIList_(x₁)) = x₁

POL(length(x₁)) = x₁

POL(_U21_(x₁)) = x₁

POL(U31(x₁)) = x₁

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

POL(isNat(x₁)) = x₁

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

POL(0) = 0

POL(tt) = 0

POL(U61(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃

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

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

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

length(nil) -> 0
isNatList(nil) -> tt

where the Polynomial interpretation:

POL(_U61_(x₁, x₂, x₃)) = x₁ + x₂ + x₃

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

POL(_length_(x₁)) = x₁

POL(_isNatList_(x₁)) = x₁

POL(isNatList(x₁)) = x₁

POL(_U31_(x₁)) = x₁

POL(_U52_(x₁)) = x₁

POL(U42(x₁)) = x₁

POL(_isNat_(x₁)) = x₁

POL(U52(x₁)) = x₁

POL(*mark*(x₁)) = x₁

POL(U11(x₁)) = x₁

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

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

POL(_zeros_) = 0

POL(cons(x₁, x₂)) = x₁ + 2·x₂

POL(_U11_(x₁)) = x₁

POL(U21(x₁)) = x₁

POL(nil) = 1

POL(_U42_(x₁)) = x₁

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

POL(zeros) = 0

POL(_isNatIList_(x₁)) = x₁

POL(length(x₁)) = x₁

POL(_U21_(x₁)) = x₁

POL(U31(x₁)) = x₁

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

POL(isNat(x₁)) = x₁

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

POL(0) = 0

POL(tt) = 0

POL(s(x₁)) = x₁

POL(U61(x₁, x₂, x₃)) = x₁ + x₂ + x₃

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

R contains the following Dependency Pairs:

MARK(U31(x0)) -> _{U31_'}(mark(x0))
MARK(U31(x0)) -> MARK(x0)
MARK(U21(x0)) -> _{U21_'}(mark(x0))
MARK(U21(x0)) -> MARK(x0)
MARK(U61(x0, x1, x2)) -> _{U61_'}(mark(x0), x1, x2)
MARK(U61(x0, x1, x2)) -> MARK(x0)
MARK(U52(x0)) -> _{U52_'}(mark(x0))
MARK(U52(x0)) -> MARK(x0)
MARK(U62(x0, x1)) -> _{U62_'}(mark(x0), x1)
MARK(U62(x0, x1)) -> MARK(x0)
MARK(U41(x0, x1)) -> _{U41_'}(mark(x0), x1)
MARK(U41(x0, x1)) -> MARK(x0)
MARK(U51(x0, x1)) -> _{U51_'}(mark(x0), x1)
MARK(U51(x0, x1)) -> MARK(x0)
MARK(s(x0)) -> MARK(x0)
MARK(length(x0)) -> LENGTH(mark(x0))
MARK(length(x0)) -> MARK(x0)
MARK(U11(x0)) -> _{U11_'}(mark(x0))
MARK(U11(x0)) -> MARK(x0)
MARK(cons(x0, x1)) -> MARK(x0)
MARK(U42(x0)) -> _{U42_'}(mark(x0))
MARK(U42(x0)) -> MARK(x0)
_{U61_'}(tt, L, N) -> _{U62_'}(isNat(N), L)
_{U61_'}(tt, L, N) -> ISNAT(N)
_{U62_'}(tt, L) -> LENGTH(mark(L))
_{U62_'}(tt, L) -> MARK(L)
LENGTH(cons(N, L)) -> _{U61_'}(isNatList(L), L, N)
LENGTH(cons(N, L)) -> ISNATLIST(L)
ISNAT(length(V1)) -> _{U11_'}(isNatList(V1))
ISNAT(length(V1)) -> ISNATLIST(V1)
_{U41_'}(tt, V2) -> _{U42_'}(isNatIList(V2))
_{U41_'}(tt, V2) -> ISNATILIST(V2)

Furthermore, R contains one SCC.

TRS

     ↳CSRtoTRS

       →TRS1

         ↳RRRPolo

           →TRS2

             ↳RRRPolo

...

               →DP Problem 1

                 ↳Negative Polynomial Order

Dependency Pairs:

MARK(U42(x0)) -> MARK(x0)
MARK(cons(x0, x1)) -> MARK(x0)
MARK(U11(x0)) -> MARK(x0)
MARK(length(x0)) -> MARK(x0)
MARK(length(x0)) -> LENGTH(mark(x0))
MARK(s(x0)) -> MARK(x0)
MARK(U51(x0, x1)) -> MARK(x0)
MARK(U41(x0, x1)) -> MARK(x0)
MARK(U62(x0, x1)) -> MARK(x0)
MARK(U62(x0, x1)) -> _{U62_'}(mark(x0), x1)
MARK(U52(x0)) -> MARK(x0)
MARK(U61(x0, x1, x2)) -> MARK(x0)
_{U62_'}(tt, L) -> MARK(L)
LENGTH(cons(N, L)) -> _{U61_'}(isNatList(L), L, N)
_{U62_'}(tt, L) -> LENGTH(mark(L))
_{U61_'}(tt, L, N) -> _{U62_'}(isNat(N), L)
MARK(U61(x0, x1, x2)) -> _{U61_'}(mark(x0), x1, x2)
MARK(U21(x0)) -> MARK(x0)
MARK(U31(x0)) -> MARK(x0)

Rules:

mark(U31(x0)) -> U31(mark(x0))
mark(U21(x0)) -> U21(mark(x0))
mark(U61(x0, x1, x2)) -> U61(mark(x0), x1, x2)
mark(U52(x0)) -> U52(mark(x0))
mark(U62(x0, x1)) -> U62(mark(x0), x1)
mark(zeros) -> zeros
mark(U41(x0, x1)) -> U41(mark(x0), x1)
mark(U51(x0, x1)) -> U51(mark(x0), x1)
mark(s(x0)) -> s(mark(x0))
mark(length(x0)) -> length(mark(x0))
mark(U11(x0)) -> U11(mark(x0))
mark(cons(x0, x1)) -> cons(mark(x0), x1)
mark(U42(x0)) -> U42(mark(x0))
U31(x0) -> U31(x0)
U31(tt) -> tt
U42(tt) -> tt
U42(x0) -> U42(x0)
U21(x0) -> U21(x0)
U21(tt) -> tt
U61(x0, x1, x2) -> U61(x0, x1, x2)
U61(tt, L, N) -> U62(isNat(N), L)
U62(tt, L) -> s(length(mark(L)))
U62(x0, x1) -> U62(x0, x1)
length(cons(N, L)) -> U61(isNatList(L), L, N)
length(x0) -> length(x0)
U52(x0) -> U52(x0)
U52(tt) -> tt
isNat(x0) -> isNat(x0)
isNat(length(V1)) -> U11(isNatList(V1))
isNat(0) -> tt
U11(x0) -> U11(x0)
U11(tt) -> tt
U51(x0, x1) -> U51(x0, x1)
U41(tt, V2) -> U42(isNatIList(V2))
U41(x0, x1) -> U41(x0, x1)
isNatList(x0) -> isNatList(x0)
isNatIList(zeros) -> tt

The following Dependency Pairs can be strictly oriented using the given order.

MARK(U42(x0)) -> MARK(x0)
MARK(U41(x0, x1)) -> MARK(x0)

Moreover, the following usable rules (regarding the implicit AFS) are oriented.

mark(U31(x0)) -> U31(mark(x0))
mark(U21(x0)) -> U21(mark(x0))
mark(U61(x0, x1, x2)) -> U61(mark(x0), x1, x2)
mark(U52(x0)) -> U52(mark(x0))
mark(U62(x0, x1)) -> U62(mark(x0), x1)
mark(zeros) -> zeros
mark(U41(x0, x1)) -> U41(mark(x0), x1)
mark(U51(x0, x1)) -> U51(mark(x0), x1)
mark(s(x0)) -> s(mark(x0))
mark(length(x0)) -> length(mark(x0))
mark(U11(x0)) -> U11(mark(x0))
mark(cons(x0, x1)) -> cons(mark(x0), x1)
mark(U42(x0)) -> U42(mark(x0))
isNatList(x0) -> isNatList(x0)
isNat(x0) -> isNat(x0)
isNat(length(V1)) -> U11(isNatList(V1))
isNat(0) -> tt
U31(x0) -> U31(x0)
U31(tt) -> tt
U21(x0) -> U21(x0)
U21(tt) -> tt
U61(x0, x1, x2) -> U61(x0, x1, x2)
U61(tt, L, N) -> U62(isNat(N), L)
U52(x0) -> U52(x0)
U52(tt) -> tt
U62(tt, L) -> s(length(mark(L)))
U62(x0, x1) -> U62(x0, x1)
U41(tt, V2) -> U42(isNatIList(V2))
U41(x0, x1) -> U41(x0, x1)
U51(x0, x1) -> U51(x0, x1)
length(cons(N, L)) -> U61(isNatList(L), L, N)
length(x0) -> length(x0)
U11(x0) -> U11(x0)
U11(tt) -> tt
U42(tt) -> tt
U42(x0) -> U42(x0)
isNatIList(zeros) -> tt

Used ordering:
Polynomial Order with Interpretation:

POL( MARK(x₁) ) = x₁

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

POL( LENGTH(x₁) ) = x₁

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

POL( _{U61_'}(x₁, ..., x₃) ) = x₂

POL( U52(x₁) ) = x₁

POL( s(x₁) ) = x₁

POL( U21(x₁) ) = x₁

POL( U61(x₁, ..., x₃) ) = x₁ + x₂

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

POL( _{U62_'}(x₁, x₂) ) = x₂

POL( mark(x₁) ) = x₁

POL( length(x₁) ) = x₁

POL( U11(x₁) ) = x₁

POL( U31(x₁) ) = x₁

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

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

POL( U31(x₁) ) = x₁

POL( U21(x₁) ) = x₁

POL( U61(x₁, ..., x₃) ) = x₁ + x₂

POL( U52(x₁) ) = x₁

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

POL( zeros ) = 0

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

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

POL( length(x₁) ) = x₁

POL( U11(x₁) ) = x₁

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

POL( isNatList(x₁) ) = 0

POL( isNat(x₁) ) = 0

POL( tt ) = 0

POL( isNatIList(x₁) ) = 0

This results in one new DP problem.

TRS

     ↳CSRtoTRS

       →TRS1

         ↳RRRPolo

           →TRS2

             ↳RRRPolo

...

               →DP Problem 2

                 ↳Negative Polynomial Order

Dependency Pairs:

MARK(cons(x0, x1)) -> MARK(x0)
MARK(U11(x0)) -> MARK(x0)
MARK(length(x0)) -> MARK(x0)
MARK(length(x0)) -> LENGTH(mark(x0))
MARK(s(x0)) -> MARK(x0)
MARK(U51(x0, x1)) -> MARK(x0)
MARK(U62(x0, x1)) -> MARK(x0)
MARK(U62(x0, x1)) -> _{U62_'}(mark(x0), x1)
MARK(U52(x0)) -> MARK(x0)
MARK(U61(x0, x1, x2)) -> MARK(x0)
_{U62_'}(tt, L) -> MARK(L)
LENGTH(cons(N, L)) -> _{U61_'}(isNatList(L), L, N)
_{U62_'}(tt, L) -> LENGTH(mark(L))
_{U61_'}(tt, L, N) -> _{U62_'}(isNat(N), L)
MARK(U61(x0, x1, x2)) -> _{U61_'}(mark(x0), x1, x2)
MARK(U21(x0)) -> MARK(x0)
MARK(U31(x0)) -> MARK(x0)

Rules:

mark(U31(x0)) -> U31(mark(x0))
mark(U21(x0)) -> U21(mark(x0))
mark(U61(x0, x1, x2)) -> U61(mark(x0), x1, x2)
mark(U52(x0)) -> U52(mark(x0))
mark(U62(x0, x1)) -> U62(mark(x0), x1)
mark(zeros) -> zeros
mark(U41(x0, x1)) -> U41(mark(x0), x1)
mark(U51(x0, x1)) -> U51(mark(x0), x1)
mark(s(x0)) -> s(mark(x0))
mark(length(x0)) -> length(mark(x0))
mark(U11(x0)) -> U11(mark(x0))
mark(cons(x0, x1)) -> cons(mark(x0), x1)
mark(U42(x0)) -> U42(mark(x0))
U31(x0) -> U31(x0)
U31(tt) -> tt
U42(tt) -> tt
U42(x0) -> U42(x0)
U21(x0) -> U21(x0)
U21(tt) -> tt
U61(x0, x1, x2) -> U61(x0, x1, x2)
U61(tt, L, N) -> U62(isNat(N), L)
U62(tt, L) -> s(length(mark(L)))
U62(x0, x1) -> U62(x0, x1)
length(cons(N, L)) -> U61(isNatList(L), L, N)
length(x0) -> length(x0)
U52(x0) -> U52(x0)
U52(tt) -> tt
isNat(x0) -> isNat(x0)
isNat(length(V1)) -> U11(isNatList(V1))
isNat(0) -> tt
U11(x0) -> U11(x0)
U11(tt) -> tt
U51(x0, x1) -> U51(x0, x1)
U41(tt, V2) -> U42(isNatIList(V2))
U41(x0, x1) -> U41(x0, x1)
isNatList(x0) -> isNatList(x0)
isNatIList(zeros) -> tt

The following Dependency Pairs can be strictly oriented using the given order.

MARK(cons(x0, x1)) -> MARK(x0)
LENGTH(cons(N, L)) -> _{U61_'}(isNatList(L), L, N)

Moreover, the following usable rules (regarding the implicit AFS) are oriented.

mark(U31(x0)) -> U31(mark(x0))
mark(U21(x0)) -> U21(mark(x0))
mark(U61(x0, x1, x2)) -> U61(mark(x0), x1, x2)
mark(U52(x0)) -> U52(mark(x0))
mark(U62(x0, x1)) -> U62(mark(x0), x1)
mark(zeros) -> zeros
mark(U41(x0, x1)) -> U41(mark(x0), x1)
mark(U51(x0, x1)) -> U51(mark(x0), x1)
mark(s(x0)) -> s(mark(x0))
mark(length(x0)) -> length(mark(x0))
mark(U11(x0)) -> U11(mark(x0))
mark(cons(x0, x1)) -> cons(mark(x0), x1)
mark(U42(x0)) -> U42(mark(x0))
isNatList(x0) -> isNatList(x0)
isNat(x0) -> isNat(x0)
isNat(length(V1)) -> U11(isNatList(V1))
isNat(0) -> tt
U31(x0) -> U31(x0)
U31(tt) -> tt
U21(x0) -> U21(x0)
U21(tt) -> tt
U61(x0, x1, x2) -> U61(x0, x1, x2)
U61(tt, L, N) -> U62(isNat(N), L)
U52(x0) -> U52(x0)
U52(tt) -> tt
U62(tt, L) -> s(length(mark(L)))
U62(x0, x1) -> U62(x0, x1)
U41(tt, V2) -> U42(isNatIList(V2))
U41(x0, x1) -> U41(x0, x1)
U51(x0, x1) -> U51(x0, x1)
length(cons(N, L)) -> U61(isNatList(L), L, N)
length(x0) -> length(x0)
U11(x0) -> U11(x0)
U11(tt) -> tt
U42(tt) -> tt
U42(x0) -> U42(x0)
isNatIList(zeros) -> tt

Used ordering:
Polynomial Order with Interpretation:

POL( MARK(x₁) ) = x₁

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

POL( LENGTH(x₁) ) = x₁

POL( _{U61_'}(x₁, ..., x₃) ) = x₂

POL( U52(x₁) ) = x₁

POL( s(x₁) ) = x₁

POL( U21(x₁) ) = x₁

POL( U61(x₁, ..., x₃) ) = x₁ + x₂

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

POL( _{U62_'}(x₁, x₂) ) = x₂

POL( mark(x₁) ) = x₁

POL( length(x₁) ) = x₁

POL( U11(x₁) ) = x₁

POL( U31(x₁) ) = x₁

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

POL( U31(x₁) ) = x₁

POL( U21(x₁) ) = x₁

POL( U61(x₁, ..., x₃) ) = x₁ + x₂

POL( U52(x₁) ) = x₁

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

POL( zeros ) = 0

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

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

POL( length(x₁) ) = x₁

POL( U11(x₁) ) = x₁

POL( U42(x₁) ) = 0

POL( isNatList(x₁) ) = 0

POL( isNat(x₁) ) = 0

POL( tt ) = 0

This results in one new DP problem.

TRS

     ↳CSRtoTRS

       →TRS1

         ↳RRRPolo

           →TRS2

             ↳RRRPolo

...

               →DP Problem 3

                 ↳Dependency Graph

Dependency Pairs:

MARK(U11(x0)) -> MARK(x0)
MARK(length(x0)) -> MARK(x0)
MARK(length(x0)) -> LENGTH(mark(x0))
MARK(s(x0)) -> MARK(x0)
MARK(U51(x0, x1)) -> MARK(x0)
MARK(U62(x0, x1)) -> MARK(x0)
MARK(U62(x0, x1)) -> _{U62_'}(mark(x0), x1)
MARK(U52(x0)) -> MARK(x0)
MARK(U61(x0, x1, x2)) -> MARK(x0)
_{U62_'}(tt, L) -> MARK(L)
_{U62_'}(tt, L) -> LENGTH(mark(L))
_{U61_'}(tt, L, N) -> _{U62_'}(isNat(N), L)
MARK(U61(x0, x1, x2)) -> _{U61_'}(mark(x0), x1, x2)
MARK(U21(x0)) -> MARK(x0)
MARK(U31(x0)) -> MARK(x0)

Rules:

mark(U31(x0)) -> U31(mark(x0))
mark(U21(x0)) -> U21(mark(x0))
mark(U61(x0, x1, x2)) -> U61(mark(x0), x1, x2)
mark(U52(x0)) -> U52(mark(x0))
mark(U62(x0, x1)) -> U62(mark(x0), x1)
mark(zeros) -> zeros
mark(U41(x0, x1)) -> U41(mark(x0), x1)
mark(U51(x0, x1)) -> U51(mark(x0), x1)
mark(s(x0)) -> s(mark(x0))
mark(length(x0)) -> length(mark(x0))
mark(U11(x0)) -> U11(mark(x0))
mark(cons(x0, x1)) -> cons(mark(x0), x1)
mark(U42(x0)) -> U42(mark(x0))
U31(x0) -> U31(x0)
U31(tt) -> tt
U42(tt) -> tt
U42(x0) -> U42(x0)
U21(x0) -> U21(x0)
U21(tt) -> tt
U61(x0, x1, x2) -> U61(x0, x1, x2)
U61(tt, L, N) -> U62(isNat(N), L)
U62(tt, L) -> s(length(mark(L)))
U62(x0, x1) -> U62(x0, x1)
length(cons(N, L)) -> U61(isNatList(L), L, N)
length(x0) -> length(x0)
U52(x0) -> U52(x0)
U52(tt) -> tt
isNat(x0) -> isNat(x0)
isNat(length(V1)) -> U11(isNatList(V1))
isNat(0) -> tt
U11(x0) -> U11(x0)
U11(tt) -> tt
U51(x0, x1) -> U51(x0, x1)
U41(tt, V2) -> U42(isNatIList(V2))
U41(x0, x1) -> U41(x0, x1)
isNatList(x0) -> isNatList(x0)
isNatIList(zeros) -> tt

Using the Dependency Graph the DP problem was split into 1 DP problems.

TRS

     ↳CSRtoTRS

       →TRS1

         ↳RRRPolo

           →TRS2

             ↳RRRPolo

...

               →DP Problem 4

                 ↳Size-Change Principle

Dependency Pairs:

MARK(length(x0)) -> MARK(x0)
MARK(s(x0)) -> MARK(x0)
MARK(U51(x0, x1)) -> MARK(x0)
MARK(U62(x0, x1)) -> MARK(x0)
MARK(U62(x0, x1)) -> _{U62_'}(mark(x0), x1)
MARK(U52(x0)) -> MARK(x0)
MARK(U61(x0, x1, x2)) -> MARK(x0)
_{U62_'}(tt, L) -> MARK(L)
_{U61_'}(tt, L, N) -> _{U62_'}(isNat(N), L)
MARK(U61(x0, x1, x2)) -> _{U61_'}(mark(x0), x1, x2)
MARK(U21(x0)) -> MARK(x0)
MARK(U31(x0)) -> MARK(x0)
MARK(U11(x0)) -> MARK(x0)

Rules:

mark(U31(x0)) -> U31(mark(x0))
mark(U21(x0)) -> U21(mark(x0))
mark(U61(x0, x1, x2)) -> U61(mark(x0), x1, x2)
mark(U52(x0)) -> U52(mark(x0))
mark(U62(x0, x1)) -> U62(mark(x0), x1)
mark(zeros) -> zeros
mark(U41(x0, x1)) -> U41(mark(x0), x1)
mark(U51(x0, x1)) -> U51(mark(x0), x1)
mark(s(x0)) -> s(mark(x0))
mark(length(x0)) -> length(mark(x0))
mark(U11(x0)) -> U11(mark(x0))
mark(cons(x0, x1)) -> cons(mark(x0), x1)
mark(U42(x0)) -> U42(mark(x0))
U31(x0) -> U31(x0)
U31(tt) -> tt
U42(tt) -> tt
U42(x0) -> U42(x0)
U21(x0) -> U21(x0)
U21(tt) -> tt
U61(x0, x1, x2) -> U61(x0, x1, x2)
U61(tt, L, N) -> U62(isNat(N), L)
U62(tt, L) -> s(length(mark(L)))
U62(x0, x1) -> U62(x0, x1)
length(cons(N, L)) -> U61(isNatList(L), L, N)
length(x0) -> length(x0)
U52(x0) -> U52(x0)
U52(tt) -> tt
isNat(x0) -> isNat(x0)
isNat(length(V1)) -> U11(isNatList(V1))
isNat(0) -> tt
U11(x0) -> U11(x0)
U11(tt) -> tt
U51(x0, x1) -> U51(x0, x1)
U41(tt, V2) -> U42(isNatIList(V2))
U41(x0, x1) -> U41(x0, x1)
isNatList(x0) -> isNatList(x0)
isNatIList(zeros) -> tt

We number the DPs as follows:

MARK(length(x0)) -> MARK(x0)
MARK(s(x0)) -> MARK(x0)
MARK(U51(x0, x1)) -> MARK(x0)
MARK(U62(x0, x1)) -> MARK(x0)
MARK(U62(x0, x1)) -> _{U62_'}(mark(x0), x1)
MARK(U52(x0)) -> MARK(x0)
MARK(U61(x0, x1, x2)) -> MARK(x0)
_{U62_'}(tt, L) -> MARK(L)
_{U61_'}(tt, L, N) -> _{U62_'}(isNat(N), L)
MARK(U61(x0, x1, x2)) -> _{U61_'}(mark(x0), x1, x2)
MARK(U21(x0)) -> MARK(x0)
MARK(U31(x0)) -> MARK(x0)
MARK(U11(x0)) -> MARK(x0)

and get the following Size-Change Graph(s):

{12, 11, 7, 6, 4, 3, 2, 1, 13}	,	{12, 11, 7, 6, 4, 3, 2, 1, 13}
1	>	1

{5}	,	{5}
1	>	2

{8}	,	{8}
2	=	1

{9}	,	{9}
2	=	2

{10}	,	{10}
1	>	2
1	>	3

which lead(s) to this/these maximal multigraph(s):

{12, 11, 7, 6, 4, 3, 2, 1, 13}	,	{12, 11, 7, 6, 4, 3, 2, 1, 13}
1	>	1

{8}	,	{5}
2	>	2

{5}	,	{8}
1	>	1

{5}	,	{12, 11, 7, 6, 4, 3, 2, 1, 13}
1	>	1

{8}	,	{9}
2	>	2

{10}	,	{8}
1	>	1

{9}	,	{10}
2	>	2
2	>	3

{12, 11, 7, 6, 4, 3, 2, 1, 13}	,	{8}
1	>	1

{10}	,	{12, 11, 7, 6, 4, 3, 2, 1, 13}
1	>	1

D_P: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.

trivial

with Argument Filtering System:

U51(x₁, x₂) -> U51(x₁, x₂)
U62(x₁, x₂) -> U62(x₁, x₂)
U31(x₁) -> U31(x₁)
U21(x₁) -> U21(x₁)
U52(x₁) -> U52(x₁)
U61(x₁, x₂, x₃) -> U61(x₁, x₂, x₃)
s(x₁) -> s(x₁)
U11(x₁) -> U11(x₁)
length(x₁) -> length(x₁)

We obtain no new DP problems.

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

POL(_U61_(x₁, x₂, x₃))	= x₁ + x₂ + x₃
POL(_U41_(x₁, x₂))	= x₁ + x₂
POL(isNatList(x₁))	= x₁
POL(_isNatList_(x₁))	= x₁
POL(_length_(x₁))	= x₁
POL(_U52_(x₁))	= x₁
POL(_U31_(x₁))	= x₁
POL(_isNat_(x₁))	= x₁
POL(U42(x₁))	= x₁
POL(U52(x₁))	= x₁
POL(mark(x₁))	= 2 + x₁
POL(U11(x₁))	= x₁
POL(U51(x₁, x₂))	= x₁ + x₂
POL(U62(x₁, x₂))	= 1 + x₁ + x₂
POL(_zeros_)	= 2
POL(_U11_(x₁))	= x₁
POL(cons(x₁, x₂))	= x₁ + 2·x₂
POL(U21(x₁))	= x₁
POL(_U42_(x₁))	= x₁
POL(_U51_(x₁, x₂))	= x₁ + x₂
POL(nil)	= 1
POL(zeros)	= 0
POL(length(x₁))	= x₁
POL(_isNatIList_(x₁))	= 1 + x₁
POL(_U21_(x₁))	= x₁
POL(U31(x₁))	= x₁
POL(_U62_(x₁, x₂))	= 1 + x₁ + x₂
POL(isNat(x₁))	= x₁
POL(U41(x₁, x₂))	= x₁ + x₂
POL(0)	= 1
POL(tt)	= 1
POL(U61(x₁, x₂, x₃))	= x₁ + x₂ + x₃
POL(s(x₁))	= x₁
POL(isNatIList(x₁))	= x₁

POL(_U61_(x₁, x₂, x₃))	= 1 + x₁ + x₂ + x₃
POL(_U41_(x₁, x₂))	= x₁ + x₂
POL(_isNatList_(x₁))	= x₁
POL(_length_(x₁))	= x₁
POL(isNatList(x₁))	= x₁
POL(_U52_(x₁))	= x₁
POL(_U31_(x₁))	= x₁
POL(_isNat_(x₁))	= x₁
POL(U42(x₁))	= x₁
POL(U52(x₁))	= x₁
POL(mark(x₁))	= x₁
POL(U11(x₁))	= x₁
POL(U51(x₁, x₂))	= x₁ + x₂
POL(U62(x₁, x₂))	= 1 + x₁ + x₂
POL(_zeros_)	= 0
POL(cons(x₁, x₂))	= 1 + x₁ + 2·x₂
POL(_U11_(x₁))	= x₁
POL(U21(x₁))	= x₁
POL(_U42_(x₁))	= x₁
POL(_U51_(x₁, x₂))	= x₁ + x₂
POL(nil)	= 0
POL(zeros)	= 0
POL(_isNatIList_(x₁))	= x₁
POL(length(x₁))	= x₁
POL(_U21_(x₁))	= x₁
POL(U31(x₁))	= x₁
POL(_U62_(x₁, x₂))	= 1 + x₁ + x₂
POL(isNat(x₁))	= x₁
POL(U41(x₁, x₂))	= x₁ + x₂
POL(0)	= 0
POL(tt)	= 0
POL(U61(x₁, x₂, x₃))	= 1 + x₁ + x₂ + x₃
POL(s(x₁))	= 1 + x₁