Termination w.r.t. Q of the given QTRS could be disproven:

0 QTRS
↳1 QTRSRRRProof (⇔)
↳2 QTRS
↳3 QTRSRRRProof (⇔)
↳4 QTRS
↳5 QTRSRRRProof (⇔)
↳6 QTRS
↳7 QTRSRRRProof (⇔)
↳8 QTRS
↳9 QTRSRRRProof (⇔)
↳10 QTRS
↳11 DependencyPairsProof (⇔)
↳12 QDP
↳13 DependencyGraphProof (⇔)
↳14 AND
  ↳15 QDP
    ↳16 UsableRulesReductionPairsProof (⇔)
    ↳17 QDP
    ↳18 MRRProof (⇔)
    ↳19 QDP
    ↳20 DependencyGraphProof (⇔)
    ↳21 AND
      ↳22 QDP
        ↳23 UsableRulesProof (⇔)
        ↳24 QDP
        ↳25 QDPSizeChangeProof (⇔)
        ↳26 TRUE
      ↳27 QDP
        ↳28 QDPOrderProof (⇔)
        ↳29 QDP
        ↳30 PisEmptyProof (⇔)
        ↳31 TRUE
      ↳32 QDP
        ↳33 Narrowing (⇔)
        ↳34 QDP
        ↳35 Narrowing (⇔)
        ↳36 QDP
        ↳37 Narrowing (⇔)
        ↳38 QDP
        ↳39 DependencyGraphProof (⇔)
        ↳40 QDP
        ↳41 Narrowing (⇔)
        ↳42 QDP
        ↳43 DependencyGraphProof (⇔)
        ↳44 QDP
        ↳45 Narrowing (⇔)
        ↳46 QDP
        ↳47 Narrowing (⇔)
        ↳48 QDP
        ↳49 DependencyGraphProof (⇔)
        ↳50 QDP
        ↳51 Narrowing (⇔)
        ↳52 QDP
        ↳53 DependencyGraphProof (⇔)
        ↳54 QDP
        ↳55 Narrowing (⇔)
        ↳56 QDP
        ↳57 DependencyGraphProof (⇔)
        ↳58 QDP
        ↳59 Narrowing (⇔)
        ↳60 QDP
        ↳61 Narrowing (⇔)
        ↳62 QDP
        ↳63 DependencyGraphProof (⇔)
        ↳64 QDP
        ↳65 Narrowing (⇔)
        ↳66 QDP
        ↳67 DependencyGraphProof (⇔)
        ↳68 QDP
        ↳69 Narrowing (⇔)
        ↳70 QDP
        ↳71 MRRProof (⇔)
        ↳72 QDP
        ↳73 MRRProof (⇔)
        ↳74 QDP
        ↳75 QDPOrderProof (⇔)
        ↳76 QDP
        ↳77 QDPOrderProof (⇔)
        ↳78 QDP
        ↳79 QDPOrderProof (⇔)
        ↳80 QDP
        ↳81 NonTerminationProof (⇔)
        ↳82 FALSE
      ↳83 QDP
  ↳84 QDP
    ↳85 UsableRulesReductionPairsProof (⇔)
    ↳86 QDP
    ↳87 Narrowing (⇔)
    ↳88 QDP
    ↳89 Narrowing (⇔)
    ↳90 QDP
    ↳91 Narrowing (⇔)
    ↳92 QDP
    ↳93 DependencyGraphProof (⇔)
    ↳94 QDP
    ↳95 Narrowing (⇔)
    ↳96 QDP
    ↳97 DependencyGraphProof (⇔)
    ↳98 QDP
    ↳99 Narrowing (⇔)
    ↳100 QDP
    ↳101 Narrowing (⇔)
    ↳102 QDP
    ↳103 DependencyGraphProof (⇔)
    ↳104 QDP
    ↳105 Narrowing (⇔)
    ↳106 QDP
    ↳107 DependencyGraphProof (⇔)
    ↳108 QDP
    ↳109 Narrowing (⇔)
    ↳110 QDP
    ↳111 DependencyGraphProof (⇔)
    ↳112 QDP
    ↳113 Narrowing (⇔)
    ↳114 QDP
    ↳115 Narrowing (⇔)
    ↳116 QDP
    ↳117 DependencyGraphProof (⇔)
    ↳118 QDP
    ↳119 Narrowing (⇔)
    ↳120 QDP
    ↳121 DependencyGraphProof (⇔)
    ↳122 QDP
    ↳123 Narrowing (⇔)
    ↳124 QDP
    ↳125 MRRProof (⇔)
    ↳126 QDP
    ↳127 MRRProof (⇔)
    ↳128 QDP
    ↳129 QDPOrderProof (⇔)
    ↳130 QDP
    ↳131 QDPOrderProof (⇔)
    ↳132 QDP
    ↳133 QDPOrderProof (⇔)
    ↳134 QDP
    ↳135 NonTerminationProof (⇔)
    ↳136 FALSE

(0) Obligation:

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

zeros → cons(0, n__zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(activate(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNat(n__length(V1)) → U11(isNatList(activate(V1)))
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNatIList(V) → U31(isNatList(activate(V)))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → U41(isNat(activate(V1)), activate(V2))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
length(nil) → 0
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X

Q is empty.

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(U11(x1)) = 2·x1   
POL(U21(x1)) = x1   
POL(U31(x1)) = x1   
POL(U41(x1, x2)) = x1 + 2·x2   
POL(U42(x1)) = 2·x1   
POL(U51(x1, x2)) = x1 + 2·x2   
POL(U52(x1)) = 2·x1   
POL(U61(x1, x2, x3)) = 2·x1 + 2·x2 + 2·x3   
POL(U62(x1, x2)) = x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = 2·x1   
POL(isNatIList(x1)) = x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = 2·x1   
POL(n__nil) = 1   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 1   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

isNatList(n__nil) → tt
length(nil) → 0


(2) Obligation:

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

zeros → cons(0, n__zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(activate(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNat(n__length(V1)) → U11(isNatList(activate(V1)))
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNatIList(V) → U31(isNatList(activate(V)))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → U41(isNat(activate(V1)), activate(V2))
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(U11(x1)) = 1 + x1   
POL(U21(x1)) = x1   
POL(U31(x1)) = x1   
POL(U41(x1, x2)) = 2·x1 + 2·x2   
POL(U42(x1)) = 2·x1   
POL(U51(x1, x2)) = 2·x1 + 2·x2   
POL(U52(x1)) = x1   
POL(U61(x1, x2, x3)) = 1 + 2·x1 + 2·x2 + x3   
POL(U62(x1, x2)) = 1 + x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatIList(x1)) = x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 1 + 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = 1 + 2·x1   
POL(n__nil) = 0   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

U11(tt) → tt


(4) Obligation:

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

zeros → cons(0, n__zeros)
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(activate(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNat(n__length(V1)) → U11(isNatList(activate(V1)))
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNatIList(V) → U31(isNatList(activate(V)))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → U41(isNat(activate(V1)), activate(V2))
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(U11(x1)) = x1   
POL(U21(x1)) = x1   
POL(U31(x1)) = x1   
POL(U41(x1, x2)) = 1 + 2·x1 + x2   
POL(U42(x1)) = x1   
POL(U51(x1, x2)) = x1 + x2   
POL(U52(x1)) = x1   
POL(U61(x1, x2, x3)) = x1 + x2 + 2·x3   
POL(U62(x1, x2)) = 2·x1 + x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatIList(x1)) = 1 + x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = x1   
POL(n__nil) = 0   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

isNatIList(V) → U31(isNatList(activate(V)))
isNatIList(n__zeros) → tt


(6) Obligation:

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

zeros → cons(0, n__zeros)
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(activate(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNat(n__length(V1)) → U11(isNatList(activate(V1)))
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNatIList(n__cons(V1, V2)) → U41(isNat(activate(V1)), activate(V2))
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X

Q is empty.

(7) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(U11(x1)) = x1   
POL(U21(x1)) = x1   
POL(U31(x1)) = 1 + x1   
POL(U41(x1, x2)) = x1 + 2·x2   
POL(U42(x1)) = 2·x1   
POL(U51(x1, x2)) = x1 + x2   
POL(U52(x1)) = x1   
POL(U61(x1, x2, x3)) = 2·x1 + 2·x2 + x3   
POL(U62(x1, x2)) = x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatIList(x1)) = x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = 2·x1   
POL(n__nil) = 0   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

U31(tt) → tt


(8) Obligation:

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

zeros → cons(0, n__zeros)
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(activate(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNat(n__length(V1)) → U11(isNatList(activate(V1)))
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNatIList(n__cons(V1, V2)) → U41(isNat(activate(V1)), activate(V2))
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X

Q is empty.

(9) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(U11(x1)) = 1 + x1   
POL(U21(x1)) = x1   
POL(U41(x1, x2)) = 2·x1 + 2·x2   
POL(U42(x1)) = x1   
POL(U51(x1, x2)) = 2·x1 + x2   
POL(U52(x1)) = x1   
POL(U61(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + 2·x3   
POL(U62(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatIList(x1)) = x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 2 + 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = 2 + 2·x1   
POL(n__nil) = 0   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

isNat(n__length(V1)) → U11(isNatList(activate(V1)))


(10) Obligation:

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

zeros → cons(0, n__zeros)
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(activate(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNatIList(n__cons(V1, V2)) → U41(isNat(activate(V1)), activate(V2))
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X

Q is empty.

(11) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(12) Obligation:

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

ZEROS → CONS(0, n__zeros)
ZEROS → 01
U411(tt, V2) → U421(isNatIList(activate(V2)))
U411(tt, V2) → ISNATILIST(activate(V2))
U411(tt, V2) → ACTIVATE(V2)
U511(tt, V2) → U521(isNatList(activate(V2)))
U511(tt, V2) → ISNATLIST(activate(V2))
U511(tt, V2) → ACTIVATE(V2)
U611(tt, L, N) → U621(isNat(activate(N)), activate(L))
U611(tt, L, N) → ISNAT(activate(N))
U611(tt, L, N) → ACTIVATE(N)
U611(tt, L, N) → ACTIVATE(L)
U621(tt, L) → S(length(activate(L)))
U621(tt, L) → LENGTH(activate(L))
U621(tt, L) → ACTIVATE(L)
ISNAT(n__s(V1)) → U211(isNat(activate(V1)))
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
ISNATILIST(n__cons(V1, V2)) → U411(isNat(activate(V1)), activate(V2))
ISNATILIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNATILIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATILIST(n__cons(V1, V2)) → ACTIVATE(V2)
ISNATLIST(n__cons(V1, V2)) → U511(isNat(activate(V1)), activate(V2))
ISNATLIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V2)
LENGTH(cons(N, L)) → U611(isNatList(activate(L)), activate(L), N)
LENGTH(cons(N, L)) → ISNATLIST(activate(L))
LENGTH(cons(N, L)) → ACTIVATE(L)
ACTIVATE(n__zeros) → ZEROS
ACTIVATE(n__0) → 01
ACTIVATE(n__length(X)) → LENGTH(activate(X))
ACTIVATE(n__length(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → S(activate(X))
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → CONS(activate(X1), X2)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__nil) → NIL

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(activate(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNatIList(n__cons(V1, V2)) → U41(isNat(activate(V1)), activate(V2))
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X

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

(13) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 15 less nodes.

(14) Complex Obligation (AND)

(15) Obligation:

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

ACTIVATE(n__length(X)) → LENGTH(activate(X))
LENGTH(cons(N, L)) → U611(isNatList(activate(L)), activate(L), N)
U611(tt, L, N) → U621(isNat(activate(N)), activate(L))
U621(tt, L) → LENGTH(activate(L))
LENGTH(cons(N, L)) → ISNATLIST(activate(L))
ISNATLIST(n__cons(V1, V2)) → U511(isNat(activate(V1)), activate(V2))
U511(tt, V2) → ISNATLIST(activate(V2))
ISNATLIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
ACTIVATE(n__length(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V2)
U511(tt, V2) → ACTIVATE(V2)
LENGTH(cons(N, L)) → ACTIVATE(L)
U621(tt, L) → ACTIVATE(L)
U611(tt, L, N) → ISNAT(activate(N))
U611(tt, L, N) → ACTIVATE(N)
U611(tt, L, N) → ACTIVATE(L)

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(activate(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNatIList(n__cons(V1, V2)) → U41(isNat(activate(V1)), activate(V2))
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X

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

(16) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVATE(x1)) = x1   
POL(ISNAT(x1)) = x1   
POL(ISNATLIST(x1)) = 2·x1   
POL(LENGTH(x1)) = 2·x1   
POL(U21(x1)) = x1   
POL(U51(x1, x2)) = 2·x1 + 2·x2   
POL(U511(x1, x2)) = 2·x1 + 2·x2   
POL(U52(x1)) = 2·x1   
POL(U61(x1, x2, x3)) = 2·x1 + 2·x2 + 2·x3   
POL(U611(x1, x2, x3)) = 2·x1 + 2·x2 + x3   
POL(U62(x1, x2)) = 2·x1 + 2·x2   
POL(U621(x1, x2)) = x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = 2·x1   
POL(n__nil) = 0   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   

(17) Obligation:

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

ACTIVATE(n__length(X)) → LENGTH(activate(X))
LENGTH(cons(N, L)) → U611(isNatList(activate(L)), activate(L), N)
U611(tt, L, N) → U621(isNat(activate(N)), activate(L))
U621(tt, L) → LENGTH(activate(L))
LENGTH(cons(N, L)) → ISNATLIST(activate(L))
ISNATLIST(n__cons(V1, V2)) → U511(isNat(activate(V1)), activate(V2))
U511(tt, V2) → ISNATLIST(activate(V2))
ISNATLIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
ACTIVATE(n__length(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V2)
U511(tt, V2) → ACTIVATE(V2)
LENGTH(cons(N, L)) → ACTIVATE(L)
U621(tt, L) → ACTIVATE(L)
U611(tt, L, N) → ISNAT(activate(N))
U611(tt, L, N) → ACTIVATE(N)
U611(tt, L, N) → ACTIVATE(L)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(18) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

ACTIVATE(n__length(X)) → LENGTH(activate(X))
ACTIVATE(n__length(X)) → ACTIVATE(X)


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVATE(x1)) = x1   
POL(ISNAT(x1)) = 2·x1   
POL(ISNATLIST(x1)) = 2·x1   
POL(LENGTH(x1)) = 2·x1   
POL(U21(x1)) = x1   
POL(U51(x1, x2)) = x1 + 2·x2   
POL(U511(x1, x2)) = x1 + 2·x2   
POL(U52(x1)) = x1   
POL(U61(x1, x2, x3)) = 1 + x1 + 2·x2 + 2·x3   
POL(U611(x1, x2, x3)) = x1 + 2·x2 + 2·x3   
POL(U62(x1, x2)) = 1 + x1 + 2·x2   
POL(U621(x1, x2)) = x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatList(x1)) = 2·x1   
POL(length(x1)) = 1 + 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = 1 + 2·x1   
POL(n__nil) = 0   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   

(19) Obligation:

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

LENGTH(cons(N, L)) → U611(isNatList(activate(L)), activate(L), N)
U611(tt, L, N) → U621(isNat(activate(N)), activate(L))
U621(tt, L) → LENGTH(activate(L))
LENGTH(cons(N, L)) → ISNATLIST(activate(L))
ISNATLIST(n__cons(V1, V2)) → U511(isNat(activate(V1)), activate(V2))
U511(tt, V2) → ISNATLIST(activate(V2))
ISNATLIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V2)
U511(tt, V2) → ACTIVATE(V2)
LENGTH(cons(N, L)) → ACTIVATE(L)
U621(tt, L) → ACTIVATE(L)
U611(tt, L, N) → ISNAT(activate(N))
U611(tt, L, N) → ACTIVATE(N)
U611(tt, L, N) → ACTIVATE(L)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(20) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 4 SCCs with 11 less nodes.

(21) Complex Obligation (AND)

(22) Obligation:

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

ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(23) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(24) Obligation:

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

ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)

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

(25) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
    The graph contains the following edges 1 > 1

  • ACTIVATE(n__s(X)) → ACTIVATE(X)
    The graph contains the following edges 1 > 1

(26) TRUE

(27) Obligation:

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

ISNAT(n__s(V1)) → ISNAT(activate(V1))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(28) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNAT(n__s(V1)) → ISNAT(activate(V1))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ISNAT(x1)) = x1   
POL(U21(x1)) = 1   
POL(U51(x1, x2)) = 0   
POL(U52(x1)) = x1   
POL(U61(x1, x2, x3)) = x1   
POL(U62(x1, x2)) = 1   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 0   
POL(isNat(x1)) = x1   
POL(isNatList(x1)) = 0   
POL(length(x1)) = 0   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 0   
POL(n__length(x1)) = 0   
POL(n__nil) = 1   
POL(n__s(x1)) = 1 + x1   
POL(n__zeros) = 0   
POL(nil) = 1   
POL(s(x1)) = 1 + x1   
POL(tt) = 1   
POL(zeros) = 0   

The following usable rules [FROCOS05] were oriented:

activate(n__zeros) → zeros
activate(n__length(X)) → length(activate(X))
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__s(X)) → s(activate(X))
activate(X) → X
activate(n__nil) → nil
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))

(29) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(30) PisEmptyProof (EQUIVALENT transformation)

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

(31) TRUE

(32) Obligation:

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

U511(tt, V2) → ISNATLIST(activate(V2))
ISNATLIST(n__cons(V1, V2)) → U511(isNat(activate(V1)), activate(V2))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(33) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U511(tt, V2) → ISNATLIST(activate(V2)) at position [0] we obtained the following new rules [LPAR04]:

U511(tt, n__zeros) → ISNATLIST(zeros)
U511(tt, n__0) → ISNATLIST(0)
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
U511(tt, n__nil) → ISNATLIST(nil)
U511(tt, x0) → ISNATLIST(x0)

(34) Obligation:

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

ISNATLIST(n__cons(V1, V2)) → U511(isNat(activate(V1)), activate(V2))
U511(tt, n__zeros) → ISNATLIST(zeros)
U511(tt, n__0) → ISNATLIST(0)
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
U511(tt, n__nil) → ISNATLIST(nil)
U511(tt, x0) → ISNATLIST(x0)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(35) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATLIST(n__cons(V1, V2)) → U511(isNat(activate(V1)), activate(V2)) at position [0] we obtained the following new rules [LPAR04]:

ISNATLIST(n__cons(n__zeros, y1)) → U511(isNat(zeros), activate(y1))
ISNATLIST(n__cons(n__0, y1)) → U511(isNat(0), activate(y1))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))

(36) Obligation:

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

U511(tt, n__zeros) → ISNATLIST(zeros)
U511(tt, n__0) → ISNATLIST(0)
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
U511(tt, n__nil) → ISNATLIST(nil)
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(n__zeros, y1)) → U511(isNat(zeros), activate(y1))
ISNATLIST(n__cons(n__0, y1)) → U511(isNat(0), activate(y1))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(37) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U511(tt, n__zeros) → ISNATLIST(zeros) at position [0] we obtained the following new rules [LPAR04]:

U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))
U511(tt, n__zeros) → ISNATLIST(n__zeros)

(38) Obligation:

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

U511(tt, n__0) → ISNATLIST(0)
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
U511(tt, n__nil) → ISNATLIST(nil)
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(n__zeros, y1)) → U511(isNat(zeros), activate(y1))
ISNATLIST(n__cons(n__0, y1)) → U511(isNat(0), activate(y1))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))
U511(tt, n__zeros) → ISNATLIST(n__zeros)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(39) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(40) Obligation:

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

ISNATLIST(n__cons(n__zeros, y1)) → U511(isNat(zeros), activate(y1))
U511(tt, n__0) → ISNATLIST(0)
ISNATLIST(n__cons(n__0, y1)) → U511(isNat(0), activate(y1))
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, n__nil) → ISNATLIST(nil)
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(41) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATLIST(n__cons(n__zeros, y1)) → U511(isNat(zeros), activate(y1)) at position [0] we obtained the following new rules [LPAR04]:

ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(n__zeros), activate(y0))

(42) Obligation:

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

U511(tt, n__0) → ISNATLIST(0)
ISNATLIST(n__cons(n__0, y1)) → U511(isNat(0), activate(y1))
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, n__nil) → ISNATLIST(nil)
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(n__zeros), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(43) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(44) Obligation:

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

ISNATLIST(n__cons(n__0, y1)) → U511(isNat(0), activate(y1))
U511(tt, n__0) → ISNATLIST(0)
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
U511(tt, n__nil) → ISNATLIST(nil)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(45) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATLIST(n__cons(n__0, y1)) → U511(isNat(0), activate(y1)) at position [0] we obtained the following new rules [LPAR04]:

ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))

(46) Obligation:

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

U511(tt, n__0) → ISNATLIST(0)
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
U511(tt, n__nil) → ISNATLIST(nil)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(47) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U511(tt, n__0) → ISNATLIST(0) at position [0] we obtained the following new rules [LPAR04]:

U511(tt, n__0) → ISNATLIST(n__0)

(48) Obligation:

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

ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
U511(tt, n__nil) → ISNATLIST(nil)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__0) → ISNATLIST(n__0)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(49) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(50) Obligation:

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

U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, n__nil) → ISNATLIST(nil)
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(51) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U511(tt, n__nil) → ISNATLIST(nil) at position [0] we obtained the following new rules [LPAR04]:

U511(tt, n__nil) → ISNATLIST(n__nil)

(52) Obligation:

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

U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__nil) → ISNATLIST(n__nil)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(53) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(54) Obligation:

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

ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(55) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1)) at position [0] we obtained the following new rules [LPAR04]:

ISNATLIST(n__cons(n__nil, y0)) → U511(isNat(n__nil), activate(y0))

(56) Obligation:

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

ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
ISNATLIST(n__cons(n__nil, y0)) → U511(isNat(n__nil), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(57) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(58) Obligation:

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

U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(59) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros)) at position [0] we obtained the following new rules [LPAR04]:

U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
U511(tt, n__zeros) → ISNATLIST(cons(n__0, n__zeros))

(60) Obligation:

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

U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
U511(tt, n__zeros) → ISNATLIST(cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(61) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0)) at position [0] we obtained the following new rules [LPAR04]:

ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(n__cons(0, n__zeros)), activate(y0))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(n__0, n__zeros)), activate(y0))

(62) Obligation:

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

U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
U511(tt, n__zeros) → ISNATLIST(cons(n__0, n__zeros))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(n__cons(0, n__zeros)), activate(y0))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(n__0, n__zeros)), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(63) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(64) Obligation:

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

ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(n__0, n__zeros)), activate(y0))
U511(tt, n__zeros) → ISNATLIST(cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(65) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(n__0, n__zeros)), activate(y0)) at position [0] we obtained the following new rules [LPAR04]:

ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(n__cons(n__0, n__zeros)), activate(y0))

(66) Obligation:

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

ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
U511(tt, n__zeros) → ISNATLIST(cons(n__0, n__zeros))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(n__cons(n__0, n__zeros)), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(67) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(68) Obligation:

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

U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(69) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U511(tt, n__zeros) → ISNATLIST(cons(n__0, n__zeros)) at position [0] we obtained the following new rules [LPAR04]:

U511(tt, n__zeros) → ISNATLIST(n__cons(n__0, n__zeros))

(70) Obligation:

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

U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(71) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ISNATLIST(x1)) = 2·x1   
POL(U21(x1)) = x1   
POL(U51(x1, x2)) = x1 + x2   
POL(U511(x1, x2)) = x1 + 2·x2   
POL(U52(x1)) = x1   
POL(U61(x1, x2, x3)) = 1 + 2·x1 + 2·x2 + 2·x3   
POL(U62(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 1 + 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = 1 + 2·x1   
POL(n__nil) = 0   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   

(72) Obligation:

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

U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(73) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ISNATLIST(x1)) = x1   
POL(U21(x1)) = x1   
POL(U51(x1, x2)) = x1 + 2·x2   
POL(U511(x1, x2)) = 2·x1 + 2·x2   
POL(U52(x1)) = 2·x1   
POL(U61(x1, x2, x3)) = 1 + 2·x1 + 2·x2 + x3   
POL(U62(x1, x2)) = 1 + x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 1 + 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = 1 + 2·x1   
POL(n__nil) = 0   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   

(74) Obligation:

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

U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(75) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ISNATLIST(x1)) = x1   
POL(U21(x1)) = 0   
POL(U51(x1, x2)) = 0   
POL(U511(x1, x2)) = x2   
POL(U52(x1)) = 0   
POL(U61(x1, x2, x3)) = 1   
POL(U62(x1, x2)) = 1   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = x1 + x2   
POL(isNat(x1)) = 0   
POL(isNatList(x1)) = 1   
POL(length(x1)) = 1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = x1 + x2   
POL(n__length(x1)) = 1   
POL(n__nil) = 0   
POL(n__s(x1)) = 1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = 1   
POL(tt) = 0   
POL(zeros) = 0   

The following usable rules [FROCOS05] were oriented:

activate(n__zeros) → zeros
activate(n__length(X)) → length(activate(X))
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__s(X)) → s(activate(X))
activate(X) → X
activate(n__nil) → nil
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))

(76) Obligation:

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

U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(77) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(U511(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/11\
\11/
·x2

POL(tt) =
/1\
\0/

POL(n__s(x1)) =
/0\
\1/
 +
/00\
\00/
·x1

POL(ISNATLIST(x1)) =
/0\
\0/
 +
/10\
\11/
·x1

POL(s(x1)) =
/0\
\1/
 +
/00\
\00/
·x1

POL(activate(x1)) =
/0\
\0/
 +
/10\
\01/
·x1

POL(n__cons(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/11\
\00/
·x2

POL(cons(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/11\
\00/
·x2

POL(isNat(x1)) =
/0\
\1/
 +
/01\
\00/
·x1

POL(n__zeros) =
/0\
\0/

POL(0) =
/0\
\0/

POL(n__0) =
/0\
\0/

POL(zeros) =
/0\
\0/

POL(n__length(x1)) =
/1\
\1/
 +
/10\
\10/
·x1

POL(length(x1)) =
/1\
\1/
 +
/10\
\10/
·x1

POL(n__nil) =
/0\
\0/

POL(nil) =
/0\
\0/

POL(U21(x1)) =
/1\
\0/
 +
/00\
\00/
·x1

POL(U62(x1, x2)) =
/0\
\1/
 +
/00\
\00/
·x1 +
/00\
\00/
·x2

POL(U51(x1, x2)) =
/0\
\1/
 +
/00\
\00/
·x1 +
/00\
\00/
·x2

POL(U52(x1)) =
/0\
\0/
 +
/10\
\00/
·x1

POL(isNatList(x1)) =
/0\
\1/
 +
/00\
\00/
·x1

POL(U61(x1, x2, x3)) =
/1\
\0/
 +
/10\
\10/
·x1 +
/00\
\10/
·x2 +
/00\
\00/
·x3

The following usable rules [FROCOS05] were oriented:

activate(n__zeros) → zeros
activate(n__length(X)) → length(activate(X))
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__s(X)) → s(activate(X))
activate(X) → X
activate(n__nil) → nil
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))

(78) Obligation:

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

U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(79) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(U511(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/01\
\00/
·x2

POL(tt) =
/1\
\0/

POL(n__cons(x1, x2)) =
/1\
\0/
 +
/00\
\10/
·x1 +
/00\
\01/
·x2

POL(ISNATLIST(x1)) =
/0\
\0/
 +
/01\
\00/
·x1

POL(cons(x1, x2)) =
/1\
\0/
 +
/00\
\10/
·x1 +
/00\
\01/
·x2

POL(activate(x1)) =
/0\
\0/
 +
/10\
\01/
·x1

POL(isNat(x1)) =
/0\
\0/
 +
/01\
\00/
·x1

POL(n__zeros) =
/1\
\0/

POL(0) =
/0\
\0/

POL(n__0) =
/0\
\0/

POL(zeros) =
/1\
\0/

POL(n__length(x1)) =
/1\
\0/
 +
/10\
\01/
·x1

POL(length(x1)) =
/1\
\0/
 +
/10\
\01/
·x1

POL(n__s(x1)) =
/0\
\1/
 +
/00\
\00/
·x1

POL(s(x1)) =
/0\
\1/
 +
/00\
\00/
·x1

POL(n__nil) =
/0\
\1/

POL(nil) =
/0\
\1/

POL(U21(x1)) =
/1\
\0/
 +
/00\
\00/
·x1

POL(U62(x1, x2)) =
/1\
\1/
 +
/00\
\00/
·x1 +
/00\
\01/
·x2

POL(U51(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/00\
\01/
·x2

POL(U52(x1)) =
/0\
\0/
 +
/10\
\10/
·x1

POL(isNatList(x1)) =
/0\
\0/
 +
/00\
\01/
·x1

POL(U61(x1, x2, x3)) =
/1\
\0/
 +
/10\
\10/
·x1 +
/00\
\01/
·x2 +
/00\
\10/
·x3

The following usable rules [FROCOS05] were oriented:

activate(n__zeros) → zeros
activate(n__length(X)) → length(activate(X))
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__s(X)) → s(activate(X))
activate(X) → X
activate(n__nil) → nil
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))

(80) Obligation:

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

U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(81) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = U511(isNat(n__0), activate(n__zeros)) evaluates to t =U511(isNat(n__0), activate(n__zeros))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [ ]



Rewriting sequence

U511(isNat(n__0), activate(n__zeros)) → U511(isNat(n__0), n__zeros)
with rule activate(X) → X at position [1] and matcher [X / n__zeros]

U511(isNat(n__0), n__zeros) → U511(tt, n__zeros)
with rule isNat(n__0) → tt at position [0] and matcher [ ]

U511(tt, n__zeros) → ISNATLIST(n__cons(n__0, n__zeros))
with rule U511(tt, n__zeros) → ISNATLIST(n__cons(n__0, n__zeros)) at position [] and matcher [ ]

ISNATLIST(n__cons(n__0, n__zeros)) → U511(isNat(n__0), activate(n__zeros))
with rule ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))

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.



(82) FALSE

(83) Obligation:

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

U611(tt, L, N) → U621(isNat(activate(N)), activate(L))
U621(tt, L) → LENGTH(activate(L))
LENGTH(cons(N, L)) → U611(isNatList(activate(L)), activate(L), N)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(84) Obligation:

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

U411(tt, V2) → ISNATILIST(activate(V2))
ISNATILIST(n__cons(V1, V2)) → U411(isNat(activate(V1)), activate(V2))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(activate(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNatIList(n__cons(V1, V2)) → U41(isNat(activate(V1)), activate(V2))
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X

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

(85) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ISNATILIST(x1)) = 2·x1   
POL(U21(x1)) = x1   
POL(U411(x1, x2)) = x1 + 2·x2   
POL(U51(x1, x2)) = x1 + 2·x2   
POL(U52(x1)) = x1   
POL(U61(x1, x2, x3)) = 1 + x1 + 2·x2 + 2·x3   
POL(U62(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatList(x1)) = 2·x1   
POL(length(x1)) = 1 + 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = x1 + 2·x2   
POL(n__length(x1)) = 1 + 2·x1   
POL(n__nil) = 1   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 1   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   

(86) Obligation:

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

U411(tt, V2) → ISNATILIST(activate(V2))
ISNATILIST(n__cons(V1, V2)) → U411(isNat(activate(V1)), activate(V2))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(87) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U411(tt, V2) → ISNATILIST(activate(V2)) at position [0] we obtained the following new rules [LPAR04]:

U411(tt, n__zeros) → ISNATILIST(zeros)
U411(tt, n__0) → ISNATILIST(0)
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
U411(tt, n__nil) → ISNATILIST(nil)
U411(tt, x0) → ISNATILIST(x0)

(88) Obligation:

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

ISNATILIST(n__cons(V1, V2)) → U411(isNat(activate(V1)), activate(V2))
U411(tt, n__zeros) → ISNATILIST(zeros)
U411(tt, n__0) → ISNATILIST(0)
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
U411(tt, n__nil) → ISNATILIST(nil)
U411(tt, x0) → ISNATILIST(x0)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(89) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATILIST(n__cons(V1, V2)) → U411(isNat(activate(V1)), activate(V2)) at position [0] we obtained the following new rules [LPAR04]:

ISNATILIST(n__cons(n__zeros, y1)) → U411(isNat(zeros), activate(y1))
ISNATILIST(n__cons(n__0, y1)) → U411(isNat(0), activate(y1))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))

(90) Obligation:

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

U411(tt, n__zeros) → ISNATILIST(zeros)
U411(tt, n__0) → ISNATILIST(0)
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
U411(tt, n__nil) → ISNATILIST(nil)
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(n__zeros, y1)) → U411(isNat(zeros), activate(y1))
ISNATILIST(n__cons(n__0, y1)) → U411(isNat(0), activate(y1))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(91) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U411(tt, n__zeros) → ISNATILIST(zeros) at position [0] we obtained the following new rules [LPAR04]:

U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))
U411(tt, n__zeros) → ISNATILIST(n__zeros)

(92) Obligation:

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

U411(tt, n__0) → ISNATILIST(0)
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
U411(tt, n__nil) → ISNATILIST(nil)
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(n__zeros, y1)) → U411(isNat(zeros), activate(y1))
ISNATILIST(n__cons(n__0, y1)) → U411(isNat(0), activate(y1))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))
U411(tt, n__zeros) → ISNATILIST(n__zeros)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(93) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(94) Obligation:

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

ISNATILIST(n__cons(n__zeros, y1)) → U411(isNat(zeros), activate(y1))
U411(tt, n__0) → ISNATILIST(0)
ISNATILIST(n__cons(n__0, y1)) → U411(isNat(0), activate(y1))
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, n__nil) → ISNATILIST(nil)
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(95) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATILIST(n__cons(n__zeros, y1)) → U411(isNat(zeros), activate(y1)) at position [0] we obtained the following new rules [LPAR04]:

ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(n__zeros), activate(y0))

(96) Obligation:

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

U411(tt, n__0) → ISNATILIST(0)
ISNATILIST(n__cons(n__0, y1)) → U411(isNat(0), activate(y1))
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, n__nil) → ISNATILIST(nil)
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(n__zeros), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(97) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(98) Obligation:

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

ISNATILIST(n__cons(n__0, y1)) → U411(isNat(0), activate(y1))
U411(tt, n__0) → ISNATILIST(0)
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
U411(tt, n__nil) → ISNATILIST(nil)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(99) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATILIST(n__cons(n__0, y1)) → U411(isNat(0), activate(y1)) at position [0] we obtained the following new rules [LPAR04]:

ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))

(100) Obligation:

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

U411(tt, n__0) → ISNATILIST(0)
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
U411(tt, n__nil) → ISNATILIST(nil)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(101) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U411(tt, n__0) → ISNATILIST(0) at position [0] we obtained the following new rules [LPAR04]:

U411(tt, n__0) → ISNATILIST(n__0)

(102) Obligation:

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

ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
U411(tt, n__nil) → ISNATILIST(nil)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__0) → ISNATILIST(n__0)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(103) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(104) Obligation:

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

U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, n__nil) → ISNATILIST(nil)
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(105) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U411(tt, n__nil) → ISNATILIST(nil) at position [0] we obtained the following new rules [LPAR04]:

U411(tt, n__nil) → ISNATILIST(n__nil)

(106) Obligation:

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

U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__nil) → ISNATILIST(n__nil)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(107) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(108) Obligation:

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

ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(109) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1)) at position [0] we obtained the following new rules [LPAR04]:

ISNATILIST(n__cons(n__nil, y0)) → U411(isNat(n__nil), activate(y0))

(110) Obligation:

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

ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
ISNATILIST(n__cons(n__nil, y0)) → U411(isNat(n__nil), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(111) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(112) Obligation:

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

U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(113) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros)) at position [0] we obtained the following new rules [LPAR04]:

U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
U411(tt, n__zeros) → ISNATILIST(cons(n__0, n__zeros))

(114) Obligation:

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

U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
U411(tt, n__zeros) → ISNATILIST(cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(115) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0)) at position [0] we obtained the following new rules [LPAR04]:

ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(n__cons(0, n__zeros)), activate(y0))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(n__0, n__zeros)), activate(y0))

(116) Obligation:

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

U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
U411(tt, n__zeros) → ISNATILIST(cons(n__0, n__zeros))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(n__cons(0, n__zeros)), activate(y0))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(n__0, n__zeros)), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(117) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(118) Obligation:

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

ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(n__0, n__zeros)), activate(y0))
U411(tt, n__zeros) → ISNATILIST(cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(119) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(n__0, n__zeros)), activate(y0)) at position [0] we obtained the following new rules [LPAR04]:

ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(n__cons(n__0, n__zeros)), activate(y0))

(120) Obligation:

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

ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
U411(tt, n__zeros) → ISNATILIST(cons(n__0, n__zeros))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(n__cons(n__0, n__zeros)), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(121) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(122) Obligation:

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

U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(123) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U411(tt, n__zeros) → ISNATILIST(cons(n__0, n__zeros)) at position [0] we obtained the following new rules [LPAR04]:

U411(tt, n__zeros) → ISNATILIST(n__cons(n__0, n__zeros))

(124) Obligation:

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

U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(125) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ISNATILIST(x1)) = x1   
POL(U21(x1)) = x1   
POL(U411(x1, x2)) = 2·x1 + 2·x2   
POL(U51(x1, x2)) = 2·x1 + 2·x2   
POL(U52(x1)) = 2·x1   
POL(U61(x1, x2, x3)) = 1 + 2·x1 + 2·x2 + x3   
POL(U62(x1, x2)) = 1 + x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 1 + 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = 1 + 2·x1   
POL(n__nil) = 0   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   

(126) Obligation:

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

ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(127) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ISNATILIST(x1)) = 2·x1   
POL(U21(x1)) = x1   
POL(U411(x1, x2)) = x1 + 2·x2   
POL(U51(x1, x2)) = x1 + x2   
POL(U52(x1)) = x1   
POL(U61(x1, x2, x3)) = 1 + 2·x1 + 2·x2 + 2·x3   
POL(U62(x1, x2)) = 1 + x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = 2·x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 1 + 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = 1 + 2·x1   
POL(n__nil) = 0   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   

(128) Obligation:

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

U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(129) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ISNATILIST(x1)) = x1   
POL(U21(x1)) = 0   
POL(U411(x1, x2)) = x2   
POL(U51(x1, x2)) = 0   
POL(U52(x1)) = 0   
POL(U61(x1, x2, x3)) = 1   
POL(U62(x1, x2)) = 1   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = x1 + x2   
POL(isNat(x1)) = 0   
POL(isNatList(x1)) = 0   
POL(length(x1)) = 1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = x1 + x2   
POL(n__length(x1)) = 1   
POL(n__nil) = 0   
POL(n__s(x1)) = 1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = 1   
POL(tt) = 0   
POL(zeros) = 0   

The following usable rules [FROCOS05] were oriented:

U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U51(tt, V2) → U52(isNatList(activate(V2)))
U62(tt, L) → s(length(activate(L)))
0 → n__0
U52(tt) → tt
zeros → n__zeros
zeros → cons(0, n__zeros)
isNat(n__s(V1)) → U21(isNat(activate(V1)))
nil → n__nil
U21(tt) → tt
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
length(X) → n__length(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__nil) → nil
activate(X) → X
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)

(130) Obligation:

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

U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(131) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(U411(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/10\
\00/
·x2

POL(tt) =
/0\
\1/

POL(n__s(x1)) =
/0\
\1/
 +
/00\
\00/
·x1

POL(ISNATILIST(x1)) =
/0\
\0/
 +
/10\
\00/
·x1

POL(s(x1)) =
/0\
\1/
 +
/00\
\00/
·x1

POL(activate(x1)) =
/0\
\0/
 +
/10\
\01/
·x1

POL(n__cons(x1, x2)) =
/0\
\1/
 +
/01\
\00/
·x1 +
/10\
\00/
·x2

POL(cons(x1, x2)) =
/0\
\1/
 +
/01\
\00/
·x1 +
/10\
\00/
·x2

POL(isNat(x1)) =
/0\
\0/
 +
/00\
\01/
·x1

POL(n__zeros) =
/0\
\1/

POL(0) =
/0\
\0/

POL(n__0) =
/0\
\0/

POL(U61(x1, x2, x3)) =
/0\
\0/
 +
/01\
\01/
·x1 +
/00\
\00/
·x2 +
/00\
\00/
·x3

POL(U62(x1, x2)) =
/1\
\1/
 +
/00\
\00/
·x1 +
/00\
\00/
·x2

POL(isNatList(x1)) =
/1\
\0/
 +
/00\
\00/
·x1

POL(U51(x1, x2)) =
/1\
\0/
 +
/00\
\00/
·x1 +
/00\
\00/
·x2

POL(U52(x1)) =
/0\
\0/
 +
/00\
\01/
·x1

POL(length(x1)) =
/0\
\0/
 +
/10\
\00/
·x1

POL(zeros) =
/0\
\1/

POL(U21(x1)) =
/0\
\1/
 +
/00\
\00/
·x1

POL(nil) =
/0\
\0/

POL(n__nil) =
/0\
\0/

POL(n__length(x1)) =
/0\
\0/
 +
/10\
\00/
·x1

The following usable rules [FROCOS05] were oriented:

U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U51(tt, V2) → U52(isNatList(activate(V2)))
U62(tt, L) → s(length(activate(L)))
0 → n__0
U52(tt) → tt
zeros → n__zeros
zeros → cons(0, n__zeros)
isNat(n__s(V1)) → U21(isNat(activate(V1)))
nil → n__nil
U21(tt) → tt
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
length(X) → n__length(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__nil) → nil
activate(X) → X
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)

(132) Obligation:

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

U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(133) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(U411(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/11\
\00/
·x2

POL(tt) =
/0\
\1/

POL(n__s(x1)) =
/0\
\1/
 +
/00\
\00/
·x1

POL(ISNATILIST(x1)) =
/0\
\0/
 +
/10\
\00/
·x1

POL(s(x1)) =
/0\
\1/
 +
/00\
\00/
·x1

POL(activate(x1)) =
/0\
\0/
 +
/10\
\01/
·x1

POL(n__cons(x1, x2)) =
/0\
\0/
 +
/00\
\01/
·x1 +
/11\
\00/
·x2

POL(cons(x1, x2)) =
/0\
\0/
 +
/00\
\01/
·x1 +
/11\
\00/
·x2

POL(isNat(x1)) =
/0\
\0/
 +
/00\
\01/
·x1

POL(n__zeros) =
/0\
\0/

POL(0) =
/0\
\0/

POL(n__0) =
/0\
\0/

POL(U61(x1, x2, x3)) =
/0\
\0/
 +
/00\
\01/
·x1 +
/10\
\00/
·x2 +
/00\
\00/
·x3

POL(U62(x1, x2)) =
/0\
\1/
 +
/00\
\00/
·x1 +
/10\
\00/
·x2

POL(isNatList(x1)) =
/1\
\0/
 +
/10\
\00/
·x1

POL(U51(x1, x2)) =
/1\
\0/
 +
/00\
\00/
·x1 +
/11\
\00/
·x2

POL(U52(x1)) =
/0\
\0/
 +
/00\
\01/
·x1

POL(length(x1)) =
/1\
\0/
 +
/10\
\01/
·x1

POL(zeros) =
/0\
\0/

POL(U21(x1)) =
/0\
\1/
 +
/00\
\00/
·x1

POL(nil) =
/0\
\0/

POL(n__nil) =
/0\
\0/

POL(n__length(x1)) =
/1\
\0/
 +
/10\
\01/
·x1

The following usable rules [FROCOS05] were oriented:

U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U51(tt, V2) → U52(isNatList(activate(V2)))
U62(tt, L) → s(length(activate(L)))
0 → n__0
U52(tt) → tt
zeros → n__zeros
zeros → cons(0, n__zeros)
isNat(n__s(V1)) → U21(isNat(activate(V1)))
nil → n__nil
U21(tt) → tt
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
length(X) → n__length(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__zeros) → zeros
activate(n__nil) → nil
activate(X) → X
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)

(134) Obligation:

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

U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

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

(135) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = U411(isNat(n__0), activate(n__zeros)) evaluates to t =U411(isNat(n__0), activate(n__zeros))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [ ]



Rewriting sequence

U411(isNat(n__0), activate(n__zeros)) → U411(isNat(n__0), n__zeros)
with rule activate(X) → X at position [1] and matcher [X / n__zeros]

U411(isNat(n__0), n__zeros) → U411(tt, n__zeros)
with rule isNat(n__0) → tt at position [0] and matcher [ ]

U411(tt, n__zeros) → ISNATILIST(n__cons(n__0, n__zeros))
with rule U411(tt, n__zeros) → ISNATILIST(n__cons(n__0, n__zeros)) at position [] and matcher [ ]

ISNATILIST(n__cons(n__0, n__zeros)) → U411(isNat(n__0), activate(n__zeros))
with rule ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))

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.



(136) FALSE