YES Termination w.r.t. Q proof of Transformed_CSR_04_LengthOfFiniteLists_nokinds_iGM.ari

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

0 QTRS
↳1 QTRSRRRProof (⇔, 77 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 35 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 QDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 QDP
        ↳10 QDPSizeChangeProof (⇔, 0 ms)
        ↳11 YES
    ↳12 QDP
        ↳13 UsableRulesProof (⇔, 0 ms)
        ↳14 QDP
        ↳15 QDPSizeChangeProof (⇔, 0 ms)
        ↳16 YES
    ↳17 QDP
        ↳18 UsableRulesProof (⇔, 0 ms)
        ↳19 QDP
        ↳20 QDPSizeChangeProof (⇔, 0 ms)
        ↳21 YES
    ↳22 QDP
        ↳23 UsableRulesProof (⇔, 0 ms)
        ↳24 QDP
        ↳25 QDPSizeChangeProof (⇔, 0 ms)
        ↳26 YES
    ↳27 QDP
        ↳28 UsableRulesProof (⇔, 0 ms)
        ↳29 QDP
        ↳30 QDPSizeChangeProof (⇔, 0 ms)
        ↳31 YES
    ↳32 QDP
        ↳33 UsableRulesProof (⇔, 0 ms)
        ↳34 QDP
        ↳35 QDPSizeChangeProof (⇔, 0 ms)
        ↳36 YES
    ↳37 QDP
        ↳38 UsableRulesProof (⇔, 0 ms)
        ↳39 QDP
        ↳40 QDPSizeChangeProof (⇔, 0 ms)
        ↳41 YES
    ↳42 QDP
        ↳43 UsableRulesProof (⇔, 0 ms)
        ↳44 QDP
        ↳45 QDPSizeChangeProof (⇔, 0 ms)
        ↳46 YES
    ↳47 QDP
        ↳48 MRRProof (⇔, 49 ms)
        ↳49 QDP
        ↳50 QDPOrderProof (⇔, 146 ms)
        ↳51 QDP
        ↳52 QDPOrderProof (⇔, 110 ms)
        ↳53 QDP
        ↳54 QDPOrderProof (⇔, 174 ms)
        ↳55 QDP
        ↳56 QDPOrderProof (⇔, 279 ms)
        ↳57 QDP
        ↳58 QDPOrderProof (⇔, 36 ms)
        ↳59 QDP
        ↳60 QDPOrderProof (⇔, 40 ms)
        ↳61 QDP
        ↳62 QDPOrderProof (⇔, 152 ms)
        ↳63 QDP
        ↳64 QDPOrderProof (⇔, 26 ms)
        ↳65 QDP
        ↳66 QDPOrderProof (⇔, 79 ms)
        ↳67 QDP
        ↳68 QDPOrderProof (⇔, 0 ms)
        ↳69 QDP
        ↳70 QDPOrderProof (⇔, 71 ms)
        ↳71 QDP
        ↳72 QDPOrderProof (⇔, 62 ms)
        ↳73 QDP
        ↳74 TransformationProof (⇔, 0 ms)
        ↳75 QDP
        ↳76 TransformationProof (⇔, 0 ms)
        ↳77 QDP
        ↳78 TransformationProof (⇔, 0 ms)
        ↳79 QDP
        ↳80 DependencyGraphProof (⇔, 0 ms)
        ↳81 QDP
        ↳82 TransformationProof (⇔, 7 ms)
        ↳83 QDP
        ↳84 DependencyGraphProof (⇔, 0 ms)
        ↳85 QDP
        ↳86 TransformationProof (⇔, 0 ms)
        ↳87 QDP
        ↳88 DependencyGraphProof (⇔, 0 ms)
        ↳89 QDP
        ↳90 QDPOrderProof (⇔, 252 ms)
        ↳91 QDP
        ↳92 QDPOrderProof (⇔, 153 ms)
        ↳93 QDP
        ↳94 QDPOrderProof (⇔, 97 ms)
        ↳95 QDP
        ↳96 QDPOrderProof (⇔, 227 ms)
        ↳97 QDP
        ↳98 QDPOrderProof (⇔, 76 ms)
        ↳99 QDP
        ↳100 QDPOrderProof (⇔, 87 ms)
        ↳101 QDP
        ↳102 QDPOrderProof (⇔, 147 ms)
        ↳103 QDP
        ↳104 QDPOrderProof (⇔, 425 ms)
        ↳105 QDP
        ↳106 QDPOrderProof (⇔, 207 ms)
        ↳107 QDP
        ↳108 QDPOrderProof (⇔, 232 ms)
        ↳109 QDP
        ↳110 QDPOrderProof (⇔, 167 ms)
        ↳111 QDP
        ↳112 QDPOrderProof (⇔, 73 ms)
        ↳113 QDP
        ↳114 NonMonReductionPairProof (⇔, 3542 ms)
        ↳115 QDP
        ↳116 QDPOrderProof (⇔, 20 ms)
        ↳117 QDP
        ↳118 QDPOrderProof (⇔, 0 ms)
        ↳119 QDP
        ↳120 PisEmptyProof (⇔, 0 ms)
        ↳121 YES

(0) Obligation:

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

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(isNatList(V1))
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(V)) → mark(isNatList(V))
active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

Q is empty.

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(U11(x1, x2)) = 1 + x1 + 2·x2   
POL(active(x1)) = x1   
POL(and(x1, x2)) = 2·x1 + x2   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatIList(x1)) = 1 + 2·x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 1 + 2·x1   
POL(mark(x1)) = x1   
POL(nil) = 2   
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:

active(isNat(length(V1))) → mark(isNatList(V1))
active(isNatIList(V)) → mark(isNatList(V))
active(isNatIList(zeros)) → mark(tt)
active(isNatList(nil)) → mark(tt)
active(length(nil)) → mark(0)


(2) Obligation:

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

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

Q is empty.

(3) DependencyPairsProof (EQUIVALENT transformation)

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

(4) Obligation:

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

ACTIVE(zeros) → MARK(cons(0, zeros))
ACTIVE(zeros) → CONS(0, zeros)
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
ACTIVE(U11(tt, L)) → S(length(L))
ACTIVE(U11(tt, L)) → LENGTH(L)
ACTIVE(and(tt, X)) → MARK(X)
ACTIVE(isNat(0)) → MARK(tt)
ACTIVE(isNat(s(V1))) → MARK(isNat(V1))
ACTIVE(isNat(s(V1))) → ISNAT(V1)
ACTIVE(isNatIList(cons(V1, V2))) → MARK(and(isNat(V1), isNatIList(V2)))
ACTIVE(isNatIList(cons(V1, V2))) → AND(isNat(V1), isNatIList(V2))
ACTIVE(isNatIList(cons(V1, V2))) → ISNAT(V1)
ACTIVE(isNatIList(cons(V1, V2))) → ISNATILIST(V2)
ACTIVE(isNatList(cons(V1, V2))) → MARK(and(isNat(V1), isNatList(V2)))
ACTIVE(isNatList(cons(V1, V2))) → AND(isNat(V1), isNatList(V2))
ACTIVE(isNatList(cons(V1, V2))) → ISNAT(V1)
ACTIVE(isNatList(cons(V1, V2))) → ISNATLIST(V2)
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
ACTIVE(length(cons(N, L))) → U111(and(isNatList(L), isNat(N)), L)
ACTIVE(length(cons(N, L))) → AND(isNatList(L), isNat(N))
ACTIVE(length(cons(N, L))) → ISNATLIST(L)
ACTIVE(length(cons(N, L))) → ISNAT(N)
MARK(zeros) → ACTIVE(zeros)
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(cons(X1, X2)) → CONS(mark(X1), X2)
MARK(cons(X1, X2)) → MARK(X1)
MARK(0) → ACTIVE(0)
MARK(U11(X1, X2)) → ACTIVE(U11(mark(X1), X2))
MARK(U11(X1, X2)) → U111(mark(X1), X2)
MARK(U11(X1, X2)) → MARK(X1)
MARK(tt) → ACTIVE(tt)
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → S(mark(X))
MARK(s(X)) → MARK(X)
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(length(X)) → LENGTH(mark(X))
MARK(length(X)) → MARK(X)
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
MARK(and(X1, X2)) → AND(mark(X1), X2)
MARK(and(X1, X2)) → MARK(X1)
MARK(isNat(X)) → ACTIVE(isNat(X))
MARK(isNatList(X)) → ACTIVE(isNatList(X))
MARK(isNatIList(X)) → ACTIVE(isNatIList(X))
MARK(nil) → ACTIVE(nil)
CONS(mark(X1), X2) → CONS(X1, X2)
CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)
U111(mark(X1), X2) → U111(X1, X2)
U111(X1, mark(X2)) → U111(X1, X2)
U111(active(X1), X2) → U111(X1, X2)
U111(X1, active(X2)) → U111(X1, X2)
S(mark(X)) → S(X)
S(active(X)) → S(X)
LENGTH(mark(X)) → LENGTH(X)
LENGTH(active(X)) → LENGTH(X)
AND(mark(X1), X2) → AND(X1, X2)
AND(X1, mark(X2)) → AND(X1, X2)
AND(active(X1), X2) → AND(X1, X2)
AND(X1, active(X2)) → AND(X1, X2)
ISNAT(mark(X)) → ISNAT(X)
ISNAT(active(X)) → ISNAT(X)
ISNATLIST(mark(X)) → ISNATLIST(X)
ISNATLIST(active(X)) → ISNATLIST(X)
ISNATILIST(mark(X)) → ISNATILIST(X)
ISNATILIST(active(X)) → ISNATILIST(X)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

ISNATILIST(active(X)) → ISNATILIST(X)
ISNATILIST(mark(X)) → ISNATILIST(X)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(8) 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.

(9) Obligation:

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

ISNATILIST(active(X)) → ISNATILIST(X)
ISNATILIST(mark(X)) → ISNATILIST(X)

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

(10) 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:

  • ISNATILIST(active(X)) → ISNATILIST(X)
    The graph contains the following edges 1 > 1

  • ISNATILIST(mark(X)) → ISNATILIST(X)
    The graph contains the following edges 1 > 1

(11) YES

(12) Obligation:

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

ISNATLIST(active(X)) → ISNATLIST(X)
ISNATLIST(mark(X)) → ISNATLIST(X)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(13) 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.

(14) Obligation:

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

ISNATLIST(active(X)) → ISNATLIST(X)
ISNATLIST(mark(X)) → ISNATLIST(X)

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

(15) 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:

  • ISNATLIST(active(X)) → ISNATLIST(X)
    The graph contains the following edges 1 > 1

  • ISNATLIST(mark(X)) → ISNATLIST(X)
    The graph contains the following edges 1 > 1

(16) YES

(17) Obligation:

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

ISNAT(active(X)) → ISNAT(X)
ISNAT(mark(X)) → ISNAT(X)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(18) 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.

(19) Obligation:

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

ISNAT(active(X)) → ISNAT(X)
ISNAT(mark(X)) → ISNAT(X)

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

(20) 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:

  • ISNAT(active(X)) → ISNAT(X)
    The graph contains the following edges 1 > 1

  • ISNAT(mark(X)) → ISNAT(X)
    The graph contains the following edges 1 > 1

(21) YES

(22) Obligation:

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

AND(X1, mark(X2)) → AND(X1, X2)
AND(mark(X1), X2) → AND(X1, X2)
AND(active(X1), X2) → AND(X1, X2)
AND(X1, active(X2)) → AND(X1, X2)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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:

AND(X1, mark(X2)) → AND(X1, X2)
AND(mark(X1), X2) → AND(X1, X2)
AND(active(X1), X2) → AND(X1, X2)
AND(X1, active(X2)) → AND(X1, X2)

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:

  • AND(X1, mark(X2)) → AND(X1, X2)
    The graph contains the following edges 1 >= 1, 2 > 2

  • AND(mark(X1), X2) → AND(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

  • AND(active(X1), X2) → AND(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

  • AND(X1, active(X2)) → AND(X1, X2)
    The graph contains the following edges 1 >= 1, 2 > 2

(26) YES

(27) Obligation:

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

LENGTH(active(X)) → LENGTH(X)
LENGTH(mark(X)) → LENGTH(X)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(28) 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.

(29) Obligation:

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

LENGTH(active(X)) → LENGTH(X)
LENGTH(mark(X)) → LENGTH(X)

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

(30) 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:

  • LENGTH(active(X)) → LENGTH(X)
    The graph contains the following edges 1 > 1

  • LENGTH(mark(X)) → LENGTH(X)
    The graph contains the following edges 1 > 1

(31) YES

(32) Obligation:

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

S(active(X)) → S(X)
S(mark(X)) → S(X)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(33) 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.

(34) Obligation:

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

S(active(X)) → S(X)
S(mark(X)) → S(X)

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

(35) 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:

  • S(active(X)) → S(X)
    The graph contains the following edges 1 > 1

  • S(mark(X)) → S(X)
    The graph contains the following edges 1 > 1

(36) YES

(37) Obligation:

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

U111(X1, mark(X2)) → U111(X1, X2)
U111(mark(X1), X2) → U111(X1, X2)
U111(active(X1), X2) → U111(X1, X2)
U111(X1, active(X2)) → U111(X1, X2)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(38) 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.

(39) Obligation:

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

U111(X1, mark(X2)) → U111(X1, X2)
U111(mark(X1), X2) → U111(X1, X2)
U111(active(X1), X2) → U111(X1, X2)
U111(X1, active(X2)) → U111(X1, X2)

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

(40) 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:

  • U111(X1, mark(X2)) → U111(X1, X2)
    The graph contains the following edges 1 >= 1, 2 > 2

  • U111(mark(X1), X2) → U111(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

  • U111(active(X1), X2) → U111(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

  • U111(X1, active(X2)) → U111(X1, X2)
    The graph contains the following edges 1 >= 1, 2 > 2

(41) YES

(42) Obligation:

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

CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(mark(X1), X2) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(43) 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.

(44) Obligation:

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

CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(mark(X1), X2) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)

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

(45) 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:

  • CONS(X1, mark(X2)) → CONS(X1, X2)
    The graph contains the following edges 1 >= 1, 2 > 2

  • CONS(mark(X1), X2) → CONS(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

  • CONS(active(X1), X2) → CONS(X1, X2)
    The graph contains the following edges 1 > 1, 2 >= 2

  • CONS(X1, active(X2)) → CONS(X1, X2)
    The graph contains the following edges 1 >= 1, 2 > 2

(46) YES

(47) Obligation:

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

MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(zeros) → ACTIVE(zeros)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(U11(X1, X2)) → ACTIVE(U11(mark(X1), X2))
ACTIVE(and(tt, X)) → MARK(X)
MARK(U11(X1, X2)) → MARK(X1)
MARK(s(X)) → ACTIVE(s(mark(X)))
ACTIVE(isNat(s(V1))) → MARK(isNat(V1))
MARK(s(X)) → MARK(X)
MARK(length(X)) → ACTIVE(length(mark(X)))
ACTIVE(isNatIList(cons(V1, V2))) → MARK(and(isNat(V1), isNatIList(V2)))
MARK(length(X)) → MARK(X)
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
ACTIVE(isNatList(cons(V1, V2))) → MARK(and(isNat(V1), isNatList(V2)))
MARK(and(X1, X2)) → MARK(X1)
MARK(isNat(X)) → ACTIVE(isNat(X))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(isNatList(X)) → ACTIVE(isNatList(X))
MARK(isNatIList(X)) → ACTIVE(isNatIList(X))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(48) 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:

MARK(U11(X1, X2)) → MARK(X1)
MARK(length(X)) → MARK(X)


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVE(x1)) = x1   
POL(MARK(x1)) = x1   
POL(U11(x1, x2)) = 1 + x1 + 2·x2   
POL(active(x1)) = x1   
POL(and(x1, x2)) = 2·x1 + x2   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatIList(x1)) = 1 + x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 1 + 2·x1   
POL(mark(x1)) = x1   
POL(nil) = 2   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   

(49) Obligation:

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

MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(zeros) → ACTIVE(zeros)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(U11(X1, X2)) → ACTIVE(U11(mark(X1), X2))
ACTIVE(and(tt, X)) → MARK(X)
MARK(s(X)) → ACTIVE(s(mark(X)))
ACTIVE(isNat(s(V1))) → MARK(isNat(V1))
MARK(s(X)) → MARK(X)
MARK(length(X)) → ACTIVE(length(mark(X)))
ACTIVE(isNatIList(cons(V1, V2))) → MARK(and(isNat(V1), isNatIList(V2)))
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
ACTIVE(isNatList(cons(V1, V2))) → MARK(and(isNat(V1), isNatList(V2)))
MARK(and(X1, X2)) → MARK(X1)
MARK(isNat(X)) → ACTIVE(isNat(X))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(isNatList(X)) → ACTIVE(isNatList(X))
MARK(isNatIList(X)) → ACTIVE(isNatIList(X))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(50) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(cons(X1, X2)) → MARK(X1)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( ACTIVE(x1) ) = 2x1 + 2

POL( U11(x1, x2) ) = x1 + 2

POL( and(x1, x2) ) = 2x1 + x2

POL( cons(x1, x2) ) = 2x1 + 1

POL( length(x1) ) = 2

POL( s(x1) ) = x1

POL( mark(x1) ) = x1

POL( active(x1) ) = x1

POL( zeros ) = 1

POL( 0 ) = 0

POL( tt ) = 0

POL( isNat(x1) ) = 0

POL( isNatIList(x1) ) = 2

POL( isNatList(x1) ) = 0

POL( nil ) = 0

POL( MARK(x1) ) = 2x1 + 2


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
active(and(tt, X)) → mark(X)
mark(s(X)) → active(s(mark(X)))
active(isNat(s(V1))) → mark(isNat(V1))
mark(length(X)) → active(length(mark(X)))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
mark(isNat(X)) → active(isNat(X))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(0) → active(0)
mark(tt) → active(tt)
mark(nil) → active(nil)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)
isNatIList(active(X)) → isNatIList(X)
isNatIList(mark(X)) → isNatIList(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNatList(active(X)) → isNatList(X)
isNatList(mark(X)) → isNatList(X)
active(isNat(0)) → mark(tt)

(51) Obligation:

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

MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(zeros) → ACTIVE(zeros)
ACTIVE(zeros) → MARK(cons(0, zeros))
MARK(U11(X1, X2)) → ACTIVE(U11(mark(X1), X2))
ACTIVE(and(tt, X)) → MARK(X)
MARK(s(X)) → ACTIVE(s(mark(X)))
ACTIVE(isNat(s(V1))) → MARK(isNat(V1))
MARK(s(X)) → MARK(X)
MARK(length(X)) → ACTIVE(length(mark(X)))
ACTIVE(isNatIList(cons(V1, V2))) → MARK(and(isNat(V1), isNatIList(V2)))
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
ACTIVE(isNatList(cons(V1, V2))) → MARK(and(isNat(V1), isNatList(V2)))
MARK(and(X1, X2)) → MARK(X1)
MARK(isNat(X)) → ACTIVE(isNat(X))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(isNatList(X)) → ACTIVE(isNatList(X))
MARK(isNatIList(X)) → ACTIVE(isNatIList(X))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(52) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(zeros) → ACTIVE(zeros)
ACTIVE(zeros) → MARK(cons(0, zeros))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( ACTIVE(x1) ) = x1

POL( U11(x1, x2) ) = 0

POL( and(x1, x2) ) = x1 + 2x2

POL( cons(x1, x2) ) = 0

POL( length(x1) ) = 0

POL( s(x1) ) = 2x1

POL( mark(x1) ) = 2x1

POL( active(x1) ) = x1

POL( zeros ) = 1

POL( 0 ) = 0

POL( tt ) = 0

POL( isNat(x1) ) = 0

POL( isNatIList(x1) ) = 0

POL( isNatList(x1) ) = 0

POL( nil ) = 0

POL( MARK(x1) ) = 2x1


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
active(and(tt, X)) → mark(X)
mark(s(X)) → active(s(mark(X)))
active(isNat(s(V1))) → mark(isNat(V1))
mark(length(X)) → active(length(mark(X)))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
mark(isNat(X)) → active(isNat(X))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(0) → active(0)
mark(tt) → active(tt)
mark(nil) → active(nil)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)
isNatIList(active(X)) → isNatIList(X)
isNatIList(mark(X)) → isNatIList(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNatList(active(X)) → isNatList(X)
isNatList(mark(X)) → isNatList(X)
active(isNat(0)) → mark(tt)

(53) Obligation:

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

MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(X1, X2)) → ACTIVE(U11(mark(X1), X2))
ACTIVE(and(tt, X)) → MARK(X)
MARK(s(X)) → ACTIVE(s(mark(X)))
ACTIVE(isNat(s(V1))) → MARK(isNat(V1))
MARK(s(X)) → MARK(X)
MARK(length(X)) → ACTIVE(length(mark(X)))
ACTIVE(isNatIList(cons(V1, V2))) → MARK(and(isNat(V1), isNatIList(V2)))
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
ACTIVE(isNatList(cons(V1, V2))) → MARK(and(isNat(V1), isNatList(V2)))
MARK(and(X1, X2)) → MARK(X1)
MARK(isNat(X)) → ACTIVE(isNat(X))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(isNatList(X)) → ACTIVE(isNatList(X))
MARK(isNatIList(X)) → ACTIVE(isNatIList(X))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(54) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(s(X)) → ACTIVE(s(mark(X)))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
MARK(x1)  =  MARK
cons(x1, x2)  =  cons
ACTIVE(x1)  =  x1
mark(x1)  =  mark(x1)
U11(x1, x2)  =  U11
tt  =  tt
s(x1)  =  s
length(x1)  =  length
and(x1, x2)  =  and
isNat(x1)  =  isNat
isNatIList(x1)  =  isNatIList
isNatList(x1)  =  isNatList
active(x1)  =  active(x1)
zeros  =  zeros
0  =  0
nil  =  nil

Recursive path order with status [RPO].
Quasi-Precedence:
active1 > [MARK, U11, length, and, isNat, isNatIList, isNatList] > mark1 > [cons, zeros] > 0 > s
active1 > [MARK, U11, length, and, isNat, isNatIList, isNatList] > mark1 > tt > s
active1 > [MARK, U11, length, and, isNat, isNatIList, isNatList] > mark1 > nil > s

Status:
MARK: multiset
cons: multiset
mark1: multiset
U11: multiset
tt: multiset
s: multiset
length: multiset
and: multiset
isNat: multiset
isNatIList: multiset
isNatList: multiset
active1: [1]
zeros: multiset
0: multiset
nil: multiset


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)
isNatIList(active(X)) → isNatIList(X)
isNatIList(mark(X)) → isNatIList(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNatList(active(X)) → isNatList(X)
isNatList(mark(X)) → isNatList(X)

(55) Obligation:

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

ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(X1, X2)) → ACTIVE(U11(mark(X1), X2))
ACTIVE(and(tt, X)) → MARK(X)
ACTIVE(isNat(s(V1))) → MARK(isNat(V1))
MARK(s(X)) → MARK(X)
MARK(length(X)) → ACTIVE(length(mark(X)))
ACTIVE(isNatIList(cons(V1, V2))) → MARK(and(isNat(V1), isNatIList(V2)))
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
ACTIVE(isNatList(cons(V1, V2))) → MARK(and(isNat(V1), isNatList(V2)))
MARK(and(X1, X2)) → MARK(X1)
MARK(isNat(X)) → ACTIVE(isNat(X))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(isNatList(X)) → ACTIVE(isNatList(X))
MARK(isNatIList(X)) → ACTIVE(isNatIList(X))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(56) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


ACTIVE(and(tt, X)) → MARK(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(ACTIVE(x1)) = 5A + 0A·x1

POL(U11(x1, x2)) = 3A + -I·x1 + 2A·x2

POL(tt) = 5A

POL(MARK(x1)) = 4A + 2A·x1

POL(s(x1)) = 3A + 0A·x1

POL(length(x1)) = 3A + 0A·x1

POL(mark(x1)) = 5A + 0A·x1

POL(and(x1, x2)) = 3A + 0A·x1 + 3A·x2

POL(isNat(x1)) = 3A + -I·x1

POL(isNatIList(x1)) = 3A + 5A·x1

POL(cons(x1, x2)) = 3A + 0A·x1 + 5A·x2

POL(isNatList(x1)) = 3A + 5A·x1

POL(active(x1)) = 5A + 0A·x1

POL(zeros) = 0A

POL(0) = 3A

POL(nil) = 1A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
active(and(tt, X)) → mark(X)
mark(s(X)) → active(s(mark(X)))
active(isNat(s(V1))) → mark(isNat(V1))
mark(length(X)) → active(length(mark(X)))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
mark(isNat(X)) → active(isNat(X))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(0) → active(0)
mark(tt) → active(tt)
mark(nil) → active(nil)
U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)
isNatIList(active(X)) → isNatIList(X)
isNatIList(mark(X)) → isNatIList(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNatList(active(X)) → isNatList(X)
isNatList(mark(X)) → isNatList(X)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
active(isNat(0)) → mark(tt)

(57) Obligation:

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

ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(X1, X2)) → ACTIVE(U11(mark(X1), X2))
ACTIVE(isNat(s(V1))) → MARK(isNat(V1))
MARK(s(X)) → MARK(X)
MARK(length(X)) → ACTIVE(length(mark(X)))
ACTIVE(isNatIList(cons(V1, V2))) → MARK(and(isNat(V1), isNatIList(V2)))
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
ACTIVE(isNatList(cons(V1, V2))) → MARK(and(isNat(V1), isNatList(V2)))
MARK(and(X1, X2)) → MARK(X1)
MARK(isNat(X)) → ACTIVE(isNat(X))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(isNatList(X)) → ACTIVE(isNatList(X))
MARK(isNatIList(X)) → ACTIVE(isNatIList(X))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(58) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(isNatIList(X)) → ACTIVE(isNatIList(X))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( ACTIVE(x1) ) = 0

POL( MARK(x1) ) = 2x1

POL( s(x1) ) = 2x1

POL( length(x1) ) = max{0, -2}

POL( active(x1) ) = x1 + 1

POL( mark(x1) ) = 2x1 + 2

POL( U11(x1, x2) ) = max{0, -1}

POL( and(x1, x2) ) = 2x1

POL( cons(x1, x2) ) = max{0, x1 - 1}

POL( zeros ) = 0

POL( 0 ) = 0

POL( tt ) = 0

POL( isNat(x1) ) = 0

POL( isNatIList(x1) ) = 2

POL( isNatList(x1) ) = 0

POL( nil ) = 1


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)

(59) Obligation:

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

ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(X1, X2)) → ACTIVE(U11(mark(X1), X2))
ACTIVE(isNat(s(V1))) → MARK(isNat(V1))
MARK(s(X)) → MARK(X)
MARK(length(X)) → ACTIVE(length(mark(X)))
ACTIVE(isNatIList(cons(V1, V2))) → MARK(and(isNat(V1), isNatIList(V2)))
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
ACTIVE(isNatList(cons(V1, V2))) → MARK(and(isNat(V1), isNatList(V2)))
MARK(and(X1, X2)) → MARK(X1)
MARK(isNat(X)) → ACTIVE(isNat(X))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(isNatList(X)) → ACTIVE(isNatList(X))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(60) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


ACTIVE(isNatIList(cons(V1, V2))) → MARK(and(isNat(V1), isNatIList(V2)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( ACTIVE(x1) ) = max{0, x1 - 2}

POL( MARK(x1) ) = max{0, -1}

POL( s(x1) ) = x1

POL( length(x1) ) = 0

POL( active(x1) ) = 2

POL( mark(x1) ) = x1

POL( U11(x1, x2) ) = 0

POL( and(x1, x2) ) = 1

POL( cons(x1, x2) ) = x1 + 2

POL( zeros ) = 2

POL( 0 ) = 2

POL( tt ) = 0

POL( isNat(x1) ) = 2

POL( isNatIList(x1) ) = x1 + 1

POL( isNatList(x1) ) = 2

POL( nil ) = 2


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

length(active(X)) → length(X)
length(mark(X)) → length(X)
U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNatList(active(X)) → isNatList(X)
isNatList(mark(X)) → isNatList(X)

(61) Obligation:

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

ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(X1, X2)) → ACTIVE(U11(mark(X1), X2))
ACTIVE(isNat(s(V1))) → MARK(isNat(V1))
MARK(s(X)) → MARK(X)
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
ACTIVE(isNatList(cons(V1, V2))) → MARK(and(isNat(V1), isNatList(V2)))
MARK(and(X1, X2)) → MARK(X1)
MARK(isNat(X)) → ACTIVE(isNat(X))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(isNatList(X)) → ACTIVE(isNatList(X))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(62) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ACTIVE(x1)  =  x1
U11(x1, x2)  =  U11
tt  =  tt
MARK(x1)  =  MARK
s(x1)  =  s
length(x1)  =  length
mark(x1)  =  mark
isNat(x1)  =  isNat
and(x1, x2)  =  and
isNatList(x1)  =  isNatList
cons(x1, x2)  =  cons(x1, x2)
active(x1)  =  active
zeros  =  zeros
0  =  0
isNatIList(x1)  =  x1
nil  =  nil

Recursive path order with status [RPO].
Quasi-Precedence:
mark > tt > [U11, MARK, length, isNat, isNatList] > [s, and, active, zeros, 0, nil]
mark > cons2 > [U11, MARK, length, isNat, isNatList] > [s, and, active, zeros, 0, nil]

Status:
U11: multiset
tt: multiset
MARK: multiset
s: multiset
length: multiset
mark: multiset
isNat: multiset
and: []
isNatList: multiset
cons2: multiset
active: multiset
zeros: multiset
0: multiset
nil: multiset


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

length(active(X)) → length(X)
length(mark(X)) → length(X)
U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNatList(active(X)) → isNatList(X)
isNatList(mark(X)) → isNatList(X)

(63) Obligation:

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

ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(X1, X2)) → ACTIVE(U11(mark(X1), X2))
ACTIVE(isNat(s(V1))) → MARK(isNat(V1))
MARK(s(X)) → MARK(X)
MARK(length(X)) → ACTIVE(length(mark(X)))
ACTIVE(isNatList(cons(V1, V2))) → MARK(and(isNat(V1), isNatList(V2)))
MARK(and(X1, X2)) → MARK(X1)
MARK(isNat(X)) → ACTIVE(isNat(X))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(isNatList(X)) → ACTIVE(isNatList(X))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(64) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


ACTIVE(isNatList(cons(V1, V2))) → MARK(and(isNat(V1), isNatList(V2)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( ACTIVE(x1) ) = 2x1 + 1

POL( MARK(x1) ) = 2x1 + 1

POL( s(x1) ) = x1

POL( length(x1) ) = 2

POL( active(x1) ) = x1 + 1

POL( mark(x1) ) = 2x1

POL( U11(x1, x2) ) = 2

POL( cons(x1, x2) ) = max{0, 2x1 + x2 - 1}

POL( zeros ) = 2

POL( 0 ) = 2

POL( tt ) = 0

POL( and(x1, x2) ) = 2x1

POL( isNat(x1) ) = 0

POL( isNatIList(x1) ) = 2x1 + 2

POL( isNatList(x1) ) = 2

POL( nil ) = 1


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)
isNatList(active(X)) → isNatList(X)
isNatList(mark(X)) → isNatList(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)

(65) Obligation:

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

ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(X1, X2)) → ACTIVE(U11(mark(X1), X2))
ACTIVE(isNat(s(V1))) → MARK(isNat(V1))
MARK(s(X)) → MARK(X)
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(and(X1, X2)) → MARK(X1)
MARK(isNat(X)) → ACTIVE(isNat(X))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(isNatList(X)) → ACTIVE(isNatList(X))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(66) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(isNatList(X)) → ACTIVE(isNatList(X))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ACTIVE(x1)  =  x1
U11(x1, x2)  =  U11
tt  =  tt
MARK(x1)  =  MARK
s(x1)  =  s(x1)
length(x1)  =  length
mark(x1)  =  mark
isNat(x1)  =  isNat
and(x1, x2)  =  and(x2)
cons(x1, x2)  =  cons(x1, x2)
isNatList(x1)  =  isNatList
active(x1)  =  active
zeros  =  zeros
0  =  0
isNatIList(x1)  =  x1
nil  =  nil

Recursive path order with status [RPO].
Quasi-Precedence:
[tt, s1, mark, and1, active] > cons2 > [U11, MARK, length, isNat] > isNatList
[tt, s1, mark, and1, active] > zeros > isNatList
[tt, s1, mark, and1, active] > 0 > isNatList
[tt, s1, mark, and1, active] > nil > isNatList

Status:
U11: []
tt: multiset
MARK: []
s1: multiset
length: []
mark: multiset
isNat: []
and1: multiset
cons2: multiset
isNatList: multiset
active: multiset
zeros: multiset
0: multiset
nil: multiset


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

length(active(X)) → length(X)
length(mark(X)) → length(X)
U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)
isNatList(active(X)) → isNatList(X)
isNatList(mark(X)) → isNatList(X)

(67) Obligation:

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

ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(X1, X2)) → ACTIVE(U11(mark(X1), X2))
ACTIVE(isNat(s(V1))) → MARK(isNat(V1))
MARK(s(X)) → MARK(X)
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(and(X1, X2)) → MARK(X1)
MARK(isNat(X)) → ACTIVE(isNat(X))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(68) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(and(X1, X2)) → MARK(X1)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( ACTIVE(x1) ) = 0

POL( MARK(x1) ) = 2x1

POL( s(x1) ) = x1

POL( length(x1) ) = 0

POL( active(x1) ) = x1

POL( mark(x1) ) = x1

POL( U11(x1, x2) ) = 0

POL( cons(x1, x2) ) = x1 + x2 + 2

POL( zeros ) = 2

POL( 0 ) = 2

POL( tt ) = 0

POL( and(x1, x2) ) = 2x1 + 2x2 + 2

POL( isNat(x1) ) = 0

POL( isNatIList(x1) ) = 2x1 + 2

POL( isNatList(x1) ) = 2

POL( nil ) = 0


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)

(69) Obligation:

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

ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(X1, X2)) → ACTIVE(U11(mark(X1), X2))
ACTIVE(isNat(s(V1))) → MARK(isNat(V1))
MARK(s(X)) → MARK(X)
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(isNat(X)) → ACTIVE(isNat(X))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(70) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


ACTIVE(isNat(s(V1))) → MARK(isNat(V1))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( ACTIVE(x1) ) = max{0, 2x1 - 2}

POL( MARK(x1) ) = max{0, 2x1 - 2}

POL( s(x1) ) = x1 + 1

POL( length(x1) ) = 0

POL( active(x1) ) = x1

POL( mark(x1) ) = x1

POL( U11(x1, x2) ) = 1

POL( cons(x1, x2) ) = 1

POL( zeros ) = 1

POL( 0 ) = 1

POL( tt ) = 1

POL( and(x1, x2) ) = max{0, x1 - 2}

POL( isNat(x1) ) = x1 + 2

POL( isNatIList(x1) ) = 2x1 + 2

POL( isNatList(x1) ) = 1

POL( nil ) = 0


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)

(71) Obligation:

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

ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(X1, X2)) → ACTIVE(U11(mark(X1), X2))
MARK(s(X)) → MARK(X)
MARK(length(X)) → ACTIVE(length(mark(X)))
MARK(isNat(X)) → ACTIVE(isNat(X))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(72) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(isNat(X)) → ACTIVE(isNat(X))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ACTIVE(x1)  =  x1
U11(x1, x2)  =  U11
tt  =  tt
MARK(x1)  =  MARK
s(x1)  =  x1
length(x1)  =  length
mark(x1)  =  mark
isNat(x1)  =  isNat
cons(x1, x2)  =  cons(x2)
and(x1, x2)  =  and(x2)
isNatList(x1)  =  isNatList(x1)
active(x1)  =  active
zeros  =  zeros
0  =  0
isNatIList(x1)  =  x1
nil  =  nil

Recursive path order with status [RPO].
Quasi-Precedence:
[U11, MARK, length] > [mark, isNat, cons1, isNatList1, active, zeros, 0, nil]
tt > [mark, isNat, cons1, isNatList1, active, zeros, 0, nil]
and1 > [mark, isNat, cons1, isNatList1, active, zeros, 0, nil]

Status:
U11: multiset
tt: multiset
MARK: multiset
length: multiset
mark: multiset
isNat: multiset
cons1: multiset
and1: multiset
isNatList1: [1]
active: []
zeros: multiset
0: multiset
nil: multiset


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

length(active(X)) → length(X)
length(mark(X)) → length(X)
U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)

(73) Obligation:

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

ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(X1, X2)) → ACTIVE(U11(mark(X1), X2))
MARK(s(X)) → MARK(X)
MARK(length(X)) → ACTIVE(length(mark(X)))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(74) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule MARK(U11(X1, X2)) → ACTIVE(U11(mark(X1), X2)) at position [0] we obtained the following new rules [LPAR04]:

MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1)) → MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1))
MARK(U11(y0, mark(x1))) → ACTIVE(U11(mark(y0), x1)) → MARK(U11(y0, mark(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(y0, active(x1))) → ACTIVE(U11(mark(y0), x1)) → MARK(U11(y0, active(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(zeros, y1)) → ACTIVE(U11(active(zeros), y1)) → MARK(U11(zeros, y1)) → ACTIVE(U11(active(zeros), y1))
MARK(U11(cons(x0, x1), y1)) → ACTIVE(U11(active(cons(mark(x0), x1)), y1)) → MARK(U11(cons(x0, x1), y1)) → ACTIVE(U11(active(cons(mark(x0), x1)), y1))
MARK(U11(0, y1)) → ACTIVE(U11(active(0), y1)) → MARK(U11(0, y1)) → ACTIVE(U11(active(0), y1))
MARK(U11(U11(x0, x1), y1)) → ACTIVE(U11(active(U11(mark(x0), x1)), y1)) → MARK(U11(U11(x0, x1), y1)) → ACTIVE(U11(active(U11(mark(x0), x1)), y1))
MARK(U11(tt, y1)) → ACTIVE(U11(active(tt), y1)) → MARK(U11(tt, y1)) → ACTIVE(U11(active(tt), y1))
MARK(U11(s(x0), y1)) → ACTIVE(U11(active(s(mark(x0))), y1)) → MARK(U11(s(x0), y1)) → ACTIVE(U11(active(s(mark(x0))), y1))
MARK(U11(length(x0), y1)) → ACTIVE(U11(active(length(mark(x0))), y1)) → MARK(U11(length(x0), y1)) → ACTIVE(U11(active(length(mark(x0))), y1))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1)) → MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(U11(isNat(x0), y1)) → ACTIVE(U11(active(isNat(x0)), y1)) → MARK(U11(isNat(x0), y1)) → ACTIVE(U11(active(isNat(x0)), y1))
MARK(U11(isNatList(x0), y1)) → ACTIVE(U11(active(isNatList(x0)), y1)) → MARK(U11(isNatList(x0), y1)) → ACTIVE(U11(active(isNatList(x0)), y1))
MARK(U11(isNatIList(x0), y1)) → ACTIVE(U11(active(isNatIList(x0)), y1)) → MARK(U11(isNatIList(x0), y1)) → ACTIVE(U11(active(isNatIList(x0)), y1))
MARK(U11(nil, y1)) → ACTIVE(U11(active(nil), y1)) → MARK(U11(nil, y1)) → ACTIVE(U11(active(nil), y1))

(75) Obligation:

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

ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(s(X)) → MARK(X)
MARK(length(X)) → ACTIVE(length(mark(X)))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1))
MARK(U11(y0, mark(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(y0, active(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(zeros, y1)) → ACTIVE(U11(active(zeros), y1))
MARK(U11(cons(x0, x1), y1)) → ACTIVE(U11(active(cons(mark(x0), x1)), y1))
MARK(U11(0, y1)) → ACTIVE(U11(active(0), y1))
MARK(U11(U11(x0, x1), y1)) → ACTIVE(U11(active(U11(mark(x0), x1)), y1))
MARK(U11(tt, y1)) → ACTIVE(U11(active(tt), y1))
MARK(U11(s(x0), y1)) → ACTIVE(U11(active(s(mark(x0))), y1))
MARK(U11(length(x0), y1)) → ACTIVE(U11(active(length(mark(x0))), y1))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(U11(isNat(x0), y1)) → ACTIVE(U11(active(isNat(x0)), y1))
MARK(U11(isNatList(x0), y1)) → ACTIVE(U11(active(isNatList(x0)), y1))
MARK(U11(isNatIList(x0), y1)) → ACTIVE(U11(active(isNatIList(x0)), y1))
MARK(U11(nil, y1)) → ACTIVE(U11(active(nil), y1))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(76) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule MARK(length(X)) → ACTIVE(length(mark(X))) at position [0] we obtained the following new rules [LPAR04]:

MARK(length(x0)) → ACTIVE(length(x0)) → MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros))) → MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1)))) → MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(0)) → ACTIVE(length(active(0))) → MARK(length(0)) → ACTIVE(length(active(0)))
MARK(length(U11(x0, x1))) → ACTIVE(length(active(U11(mark(x0), x1)))) → MARK(length(U11(x0, x1))) → ACTIVE(length(active(U11(mark(x0), x1))))
MARK(length(tt)) → ACTIVE(length(active(tt))) → MARK(length(tt)) → ACTIVE(length(active(tt)))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0))))) → MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0))))) → MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1)))) → MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(isNat(x0))) → ACTIVE(length(active(isNat(x0)))) → MARK(length(isNat(x0))) → ACTIVE(length(active(isNat(x0))))
MARK(length(isNatList(x0))) → ACTIVE(length(active(isNatList(x0)))) → MARK(length(isNatList(x0))) → ACTIVE(length(active(isNatList(x0))))
MARK(length(isNatIList(x0))) → ACTIVE(length(active(isNatIList(x0)))) → MARK(length(isNatIList(x0))) → ACTIVE(length(active(isNatIList(x0))))
MARK(length(nil)) → ACTIVE(length(active(nil))) → MARK(length(nil)) → ACTIVE(length(active(nil)))

(77) Obligation:

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

ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(s(X)) → MARK(X)
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1))
MARK(U11(y0, mark(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(y0, active(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(zeros, y1)) → ACTIVE(U11(active(zeros), y1))
MARK(U11(cons(x0, x1), y1)) → ACTIVE(U11(active(cons(mark(x0), x1)), y1))
MARK(U11(0, y1)) → ACTIVE(U11(active(0), y1))
MARK(U11(U11(x0, x1), y1)) → ACTIVE(U11(active(U11(mark(x0), x1)), y1))
MARK(U11(tt, y1)) → ACTIVE(U11(active(tt), y1))
MARK(U11(s(x0), y1)) → ACTIVE(U11(active(s(mark(x0))), y1))
MARK(U11(length(x0), y1)) → ACTIVE(U11(active(length(mark(x0))), y1))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(U11(isNat(x0), y1)) → ACTIVE(U11(active(isNat(x0)), y1))
MARK(U11(isNatList(x0), y1)) → ACTIVE(U11(active(isNatList(x0)), y1))
MARK(U11(isNatIList(x0), y1)) → ACTIVE(U11(active(isNatIList(x0)), y1))
MARK(U11(nil, y1)) → ACTIVE(U11(active(nil), y1))
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(0)) → ACTIVE(length(active(0)))
MARK(length(U11(x0, x1))) → ACTIVE(length(active(U11(mark(x0), x1))))
MARK(length(tt)) → ACTIVE(length(active(tt)))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(isNat(x0))) → ACTIVE(length(active(isNat(x0))))
MARK(length(isNatList(x0))) → ACTIVE(length(active(isNatList(x0))))
MARK(length(isNatIList(x0))) → ACTIVE(length(active(isNatIList(x0))))
MARK(length(nil)) → ACTIVE(length(active(nil)))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(78) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule MARK(length(0)) → ACTIVE(length(active(0))) at position [0] we obtained the following new rules [LPAR04]:

MARK(length(0)) → ACTIVE(length(0)) → MARK(length(0)) → ACTIVE(length(0))

(79) Obligation:

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

ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(s(X)) → MARK(X)
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1))
MARK(U11(y0, mark(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(y0, active(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(zeros, y1)) → ACTIVE(U11(active(zeros), y1))
MARK(U11(cons(x0, x1), y1)) → ACTIVE(U11(active(cons(mark(x0), x1)), y1))
MARK(U11(0, y1)) → ACTIVE(U11(active(0), y1))
MARK(U11(U11(x0, x1), y1)) → ACTIVE(U11(active(U11(mark(x0), x1)), y1))
MARK(U11(tt, y1)) → ACTIVE(U11(active(tt), y1))
MARK(U11(s(x0), y1)) → ACTIVE(U11(active(s(mark(x0))), y1))
MARK(U11(length(x0), y1)) → ACTIVE(U11(active(length(mark(x0))), y1))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(U11(isNat(x0), y1)) → ACTIVE(U11(active(isNat(x0)), y1))
MARK(U11(isNatList(x0), y1)) → ACTIVE(U11(active(isNatList(x0)), y1))
MARK(U11(isNatIList(x0), y1)) → ACTIVE(U11(active(isNatIList(x0)), y1))
MARK(U11(nil, y1)) → ACTIVE(U11(active(nil), y1))
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(U11(x0, x1))) → ACTIVE(length(active(U11(mark(x0), x1))))
MARK(length(tt)) → ACTIVE(length(active(tt)))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(isNat(x0))) → ACTIVE(length(active(isNat(x0))))
MARK(length(isNatList(x0))) → ACTIVE(length(active(isNatList(x0))))
MARK(length(isNatIList(x0))) → ACTIVE(length(active(isNatIList(x0))))
MARK(length(nil)) → ACTIVE(length(active(nil)))
MARK(length(0)) → ACTIVE(length(0))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(80) DependencyGraphProof (EQUIVALENT transformation)

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

(81) Obligation:

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

MARK(s(X)) → MARK(X)
MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1))
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(y0, mark(x1))) → ACTIVE(U11(mark(y0), x1))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(y0, active(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(zeros, y1)) → ACTIVE(U11(active(zeros), y1))
MARK(U11(cons(x0, x1), y1)) → ACTIVE(U11(active(cons(mark(x0), x1)), y1))
MARK(U11(0, y1)) → ACTIVE(U11(active(0), y1))
MARK(U11(U11(x0, x1), y1)) → ACTIVE(U11(active(U11(mark(x0), x1)), y1))
MARK(U11(tt, y1)) → ACTIVE(U11(active(tt), y1))
MARK(U11(s(x0), y1)) → ACTIVE(U11(active(s(mark(x0))), y1))
MARK(U11(length(x0), y1)) → ACTIVE(U11(active(length(mark(x0))), y1))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(U11(isNat(x0), y1)) → ACTIVE(U11(active(isNat(x0)), y1))
MARK(U11(isNatList(x0), y1)) → ACTIVE(U11(active(isNatList(x0)), y1))
MARK(U11(isNatIList(x0), y1)) → ACTIVE(U11(active(isNatIList(x0)), y1))
MARK(U11(nil, y1)) → ACTIVE(U11(active(nil), y1))
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(U11(x0, x1))) → ACTIVE(length(active(U11(mark(x0), x1))))
MARK(length(tt)) → ACTIVE(length(active(tt)))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(isNat(x0))) → ACTIVE(length(active(isNat(x0))))
MARK(length(isNatList(x0))) → ACTIVE(length(active(isNatList(x0))))
MARK(length(isNatIList(x0))) → ACTIVE(length(active(isNatIList(x0))))
MARK(length(nil)) → ACTIVE(length(active(nil)))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(82) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule MARK(length(tt)) → ACTIVE(length(active(tt))) at position [0] we obtained the following new rules [LPAR04]:

MARK(length(tt)) → ACTIVE(length(tt)) → MARK(length(tt)) → ACTIVE(length(tt))

(83) Obligation:

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

MARK(s(X)) → MARK(X)
MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1))
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(y0, mark(x1))) → ACTIVE(U11(mark(y0), x1))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(y0, active(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(zeros, y1)) → ACTIVE(U11(active(zeros), y1))
MARK(U11(cons(x0, x1), y1)) → ACTIVE(U11(active(cons(mark(x0), x1)), y1))
MARK(U11(0, y1)) → ACTIVE(U11(active(0), y1))
MARK(U11(U11(x0, x1), y1)) → ACTIVE(U11(active(U11(mark(x0), x1)), y1))
MARK(U11(tt, y1)) → ACTIVE(U11(active(tt), y1))
MARK(U11(s(x0), y1)) → ACTIVE(U11(active(s(mark(x0))), y1))
MARK(U11(length(x0), y1)) → ACTIVE(U11(active(length(mark(x0))), y1))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(U11(isNat(x0), y1)) → ACTIVE(U11(active(isNat(x0)), y1))
MARK(U11(isNatList(x0), y1)) → ACTIVE(U11(active(isNatList(x0)), y1))
MARK(U11(isNatIList(x0), y1)) → ACTIVE(U11(active(isNatIList(x0)), y1))
MARK(U11(nil, y1)) → ACTIVE(U11(active(nil), y1))
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(U11(x0, x1))) → ACTIVE(length(active(U11(mark(x0), x1))))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(isNat(x0))) → ACTIVE(length(active(isNat(x0))))
MARK(length(isNatList(x0))) → ACTIVE(length(active(isNatList(x0))))
MARK(length(isNatIList(x0))) → ACTIVE(length(active(isNatIList(x0))))
MARK(length(nil)) → ACTIVE(length(active(nil)))
MARK(length(tt)) → ACTIVE(length(tt))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(84) DependencyGraphProof (EQUIVALENT transformation)

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

(85) Obligation:

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

MARK(s(X)) → MARK(X)
MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1))
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(y0, mark(x1))) → ACTIVE(U11(mark(y0), x1))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(y0, active(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(zeros, y1)) → ACTIVE(U11(active(zeros), y1))
MARK(U11(cons(x0, x1), y1)) → ACTIVE(U11(active(cons(mark(x0), x1)), y1))
MARK(U11(0, y1)) → ACTIVE(U11(active(0), y1))
MARK(U11(U11(x0, x1), y1)) → ACTIVE(U11(active(U11(mark(x0), x1)), y1))
MARK(U11(tt, y1)) → ACTIVE(U11(active(tt), y1))
MARK(U11(s(x0), y1)) → ACTIVE(U11(active(s(mark(x0))), y1))
MARK(U11(length(x0), y1)) → ACTIVE(U11(active(length(mark(x0))), y1))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(U11(isNat(x0), y1)) → ACTIVE(U11(active(isNat(x0)), y1))
MARK(U11(isNatList(x0), y1)) → ACTIVE(U11(active(isNatList(x0)), y1))
MARK(U11(isNatIList(x0), y1)) → ACTIVE(U11(active(isNatIList(x0)), y1))
MARK(U11(nil, y1)) → ACTIVE(U11(active(nil), y1))
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(U11(x0, x1))) → ACTIVE(length(active(U11(mark(x0), x1))))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(isNat(x0))) → ACTIVE(length(active(isNat(x0))))
MARK(length(isNatList(x0))) → ACTIVE(length(active(isNatList(x0))))
MARK(length(isNatIList(x0))) → ACTIVE(length(active(isNatIList(x0))))
MARK(length(nil)) → ACTIVE(length(active(nil)))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(86) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule MARK(length(nil)) → ACTIVE(length(active(nil))) at position [0] we obtained the following new rules [LPAR04]:

MARK(length(nil)) → ACTIVE(length(nil)) → MARK(length(nil)) → ACTIVE(length(nil))

(87) Obligation:

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

MARK(s(X)) → MARK(X)
MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1))
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(y0, mark(x1))) → ACTIVE(U11(mark(y0), x1))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(y0, active(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(zeros, y1)) → ACTIVE(U11(active(zeros), y1))
MARK(U11(cons(x0, x1), y1)) → ACTIVE(U11(active(cons(mark(x0), x1)), y1))
MARK(U11(0, y1)) → ACTIVE(U11(active(0), y1))
MARK(U11(U11(x0, x1), y1)) → ACTIVE(U11(active(U11(mark(x0), x1)), y1))
MARK(U11(tt, y1)) → ACTIVE(U11(active(tt), y1))
MARK(U11(s(x0), y1)) → ACTIVE(U11(active(s(mark(x0))), y1))
MARK(U11(length(x0), y1)) → ACTIVE(U11(active(length(mark(x0))), y1))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(U11(isNat(x0), y1)) → ACTIVE(U11(active(isNat(x0)), y1))
MARK(U11(isNatList(x0), y1)) → ACTIVE(U11(active(isNatList(x0)), y1))
MARK(U11(isNatIList(x0), y1)) → ACTIVE(U11(active(isNatIList(x0)), y1))
MARK(U11(nil, y1)) → ACTIVE(U11(active(nil), y1))
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(U11(x0, x1))) → ACTIVE(length(active(U11(mark(x0), x1))))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(isNat(x0))) → ACTIVE(length(active(isNat(x0))))
MARK(length(isNatList(x0))) → ACTIVE(length(active(isNatList(x0))))
MARK(length(isNatIList(x0))) → ACTIVE(length(active(isNatIList(x0))))
MARK(length(nil)) → ACTIVE(length(nil))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(88) DependencyGraphProof (EQUIVALENT transformation)

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

(89) Obligation:

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

MARK(s(X)) → MARK(X)
MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1))
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(y0, mark(x1))) → ACTIVE(U11(mark(y0), x1))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(y0, active(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(zeros, y1)) → ACTIVE(U11(active(zeros), y1))
MARK(U11(cons(x0, x1), y1)) → ACTIVE(U11(active(cons(mark(x0), x1)), y1))
MARK(U11(0, y1)) → ACTIVE(U11(active(0), y1))
MARK(U11(U11(x0, x1), y1)) → ACTIVE(U11(active(U11(mark(x0), x1)), y1))
MARK(U11(tt, y1)) → ACTIVE(U11(active(tt), y1))
MARK(U11(s(x0), y1)) → ACTIVE(U11(active(s(mark(x0))), y1))
MARK(U11(length(x0), y1)) → ACTIVE(U11(active(length(mark(x0))), y1))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(U11(isNat(x0), y1)) → ACTIVE(U11(active(isNat(x0)), y1))
MARK(U11(isNatList(x0), y1)) → ACTIVE(U11(active(isNatList(x0)), y1))
MARK(U11(isNatIList(x0), y1)) → ACTIVE(U11(active(isNatIList(x0)), y1))
MARK(U11(nil, y1)) → ACTIVE(U11(active(nil), y1))
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(U11(x0, x1))) → ACTIVE(length(active(U11(mark(x0), x1))))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(isNat(x0))) → ACTIVE(length(active(isNat(x0))))
MARK(length(isNatList(x0))) → ACTIVE(length(active(isNatList(x0))))
MARK(length(isNatIList(x0))) → ACTIVE(length(active(isNatIList(x0))))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(90) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(U11(U11(x0, x1), y1)) → ACTIVE(U11(active(U11(mark(x0), x1)), y1))
MARK(U11(length(x0), y1)) → ACTIVE(U11(active(length(mark(x0))), y1))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( ACTIVE(x1) ) = x1 + 1

POL( MARK(x1) ) = 2x1

POL( U11(x1, x2) ) = x1 + 1

POL( mark(x1) ) = x1

POL( active(x1) ) = x1

POL( s(x1) ) = x1

POL( length(x1) ) = 1

POL( cons(x1, x2) ) = 0

POL( zeros ) = 0

POL( 0 ) = 0

POL( tt ) = 0

POL( and(x1, x2) ) = x2

POL( isNat(x1) ) = 0

POL( isNatIList(x1) ) = 0

POL( isNatList(x1) ) = 0

POL( nil ) = 0


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
active(and(tt, X)) → mark(X)
mark(s(X)) → active(s(mark(X)))
active(isNat(s(V1))) → mark(isNat(V1))
mark(length(X)) → active(length(mark(X)))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
mark(isNat(X)) → active(isNat(X))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(0) → active(0)
mark(tt) → active(tt)
mark(nil) → active(nil)
isNatList(active(X)) → isNatList(X)
isNatList(mark(X)) → isNatList(X)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
active(isNat(0)) → mark(tt)
isNatIList(active(X)) → isNatIList(X)
isNatIList(mark(X)) → isNatIList(X)

(91) Obligation:

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

MARK(s(X)) → MARK(X)
MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1))
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(y0, mark(x1))) → ACTIVE(U11(mark(y0), x1))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(y0, active(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(zeros, y1)) → ACTIVE(U11(active(zeros), y1))
MARK(U11(cons(x0, x1), y1)) → ACTIVE(U11(active(cons(mark(x0), x1)), y1))
MARK(U11(0, y1)) → ACTIVE(U11(active(0), y1))
MARK(U11(tt, y1)) → ACTIVE(U11(active(tt), y1))
MARK(U11(s(x0), y1)) → ACTIVE(U11(active(s(mark(x0))), y1))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(U11(isNat(x0), y1)) → ACTIVE(U11(active(isNat(x0)), y1))
MARK(U11(isNatList(x0), y1)) → ACTIVE(U11(active(isNatList(x0)), y1))
MARK(U11(isNatIList(x0), y1)) → ACTIVE(U11(active(isNatIList(x0)), y1))
MARK(U11(nil, y1)) → ACTIVE(U11(active(nil), y1))
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(U11(x0, x1))) → ACTIVE(length(active(U11(mark(x0), x1))))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(isNat(x0))) → ACTIVE(length(active(isNat(x0))))
MARK(length(isNatList(x0))) → ACTIVE(length(active(isNatList(x0))))
MARK(length(isNatIList(x0))) → ACTIVE(length(active(isNatIList(x0))))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(92) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(U11(s(x0), y1)) → ACTIVE(U11(active(s(mark(x0))), y1))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( ACTIVE(x1) ) = 0

POL( MARK(x1) ) = max{0, 2x1 - 2}

POL( U11(x1, x2) ) = 2x1 + 1

POL( mark(x1) ) = x1

POL( active(x1) ) = 2x1 + 1

POL( s(x1) ) = 2x1 + 1

POL( length(x1) ) = 0

POL( cons(x1, x2) ) = 0

POL( zeros ) = 0

POL( 0 ) = 0

POL( tt ) = 0

POL( and(x1, x2) ) = 0

POL( isNat(x1) ) = 0

POL( isNatIList(x1) ) = 0

POL( isNatList(x1) ) = 0

POL( nil ) = 0


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)

(93) Obligation:

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

MARK(s(X)) → MARK(X)
MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1))
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(y0, mark(x1))) → ACTIVE(U11(mark(y0), x1))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(y0, active(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(zeros, y1)) → ACTIVE(U11(active(zeros), y1))
MARK(U11(cons(x0, x1), y1)) → ACTIVE(U11(active(cons(mark(x0), x1)), y1))
MARK(U11(0, y1)) → ACTIVE(U11(active(0), y1))
MARK(U11(tt, y1)) → ACTIVE(U11(active(tt), y1))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(U11(isNat(x0), y1)) → ACTIVE(U11(active(isNat(x0)), y1))
MARK(U11(isNatList(x0), y1)) → ACTIVE(U11(active(isNatList(x0)), y1))
MARK(U11(isNatIList(x0), y1)) → ACTIVE(U11(active(isNatIList(x0)), y1))
MARK(U11(nil, y1)) → ACTIVE(U11(active(nil), y1))
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(U11(x0, x1))) → ACTIVE(length(active(U11(mark(x0), x1))))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(isNat(x0))) → ACTIVE(length(active(isNat(x0))))
MARK(length(isNatList(x0))) → ACTIVE(length(active(isNatList(x0))))
MARK(length(isNatIList(x0))) → ACTIVE(length(active(isNatIList(x0))))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(94) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(U11(zeros, y1)) → ACTIVE(U11(active(zeros), y1))
MARK(U11(cons(x0, x1), y1)) → ACTIVE(U11(active(cons(mark(x0), x1)), y1))
MARK(U11(0, y1)) → ACTIVE(U11(active(0), y1))
MARK(U11(tt, y1)) → ACTIVE(U11(active(tt), y1))
MARK(U11(isNatList(x0), y1)) → ACTIVE(U11(active(isNatList(x0)), y1))
MARK(U11(isNatIList(x0), y1)) → ACTIVE(U11(active(isNatIList(x0)), y1))
MARK(U11(nil, y1)) → ACTIVE(U11(active(nil), y1))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( ACTIVE(x1) ) = 2

POL( MARK(x1) ) = x1 + 2

POL( U11(x1, x2) ) = x1

POL( mark(x1) ) = 2x1 + 2

POL( active(x1) ) = x1

POL( s(x1) ) = x1

POL( length(x1) ) = 0

POL( cons(x1, x2) ) = x2 + 1

POL( zeros ) = 1

POL( 0 ) = 1

POL( tt ) = 2

POL( and(x1, x2) ) = x2

POL( isNat(x1) ) = 0

POL( isNatIList(x1) ) = 1

POL( isNatList(x1) ) = x1 + 2

POL( nil ) = 1


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)

(95) Obligation:

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

MARK(s(X)) → MARK(X)
MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1))
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(y0, mark(x1))) → ACTIVE(U11(mark(y0), x1))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(y0, active(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(U11(isNat(x0), y1)) → ACTIVE(U11(active(isNat(x0)), y1))
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(U11(x0, x1))) → ACTIVE(length(active(U11(mark(x0), x1))))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(isNat(x0))) → ACTIVE(length(active(isNat(x0))))
MARK(length(isNatList(x0))) → ACTIVE(length(active(isNatList(x0))))
MARK(length(isNatIList(x0))) → ACTIVE(length(active(isNatIList(x0))))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(96) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(U11(isNat(x0), y1)) → ACTIVE(U11(active(isNat(x0)), y1))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( ACTIVE(x1) ) = 1

POL( MARK(x1) ) = x1 + 1

POL( U11(x1, x2) ) = 2x1

POL( mark(x1) ) = 2x1 + 1

POL( active(x1) ) = 2x1

POL( s(x1) ) = 2x1

POL( length(x1) ) = 0

POL( cons(x1, x2) ) = x2

POL( zeros ) = 1

POL( 0 ) = 1

POL( tt ) = 1

POL( and(x1, x2) ) = 0

POL( isNat(x1) ) = 1

POL( isNatIList(x1) ) = 0

POL( isNatList(x1) ) = 2

POL( nil ) = 0


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)

(97) Obligation:

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

MARK(s(X)) → MARK(X)
MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1))
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(y0, mark(x1))) → ACTIVE(U11(mark(y0), x1))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(y0, active(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(U11(x0, x1))) → ACTIVE(length(active(U11(mark(x0), x1))))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(isNat(x0))) → ACTIVE(length(active(isNat(x0))))
MARK(length(isNatList(x0))) → ACTIVE(length(active(isNatList(x0))))
MARK(length(isNatIList(x0))) → ACTIVE(length(active(isNatIList(x0))))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(98) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(length(isNat(x0))) → ACTIVE(length(active(isNat(x0))))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(MARK(x1)) = 3A + 0A·x1

POL(s(x1)) = 3A + 0A·x1

POL(U11(x1, x2)) = 5A + 3A·x1 + 2A·x2

POL(ACTIVE(x1)) = 2A + 0A·x1

POL(tt) = 0A

POL(length(x1)) = 0A + 2A·x1

POL(mark(x1)) = -I + 0A·x1

POL(cons(x1, x2)) = 5A + -I·x1 + 0A·x2

POL(and(x1, x2)) = 4A + -I·x1 + 0A·x2

POL(isNatList(x1)) = 3A + 0A·x1

POL(isNat(x1)) = 0A + -I·x1

POL(active(x1)) = -I + 0A·x1

POL(zeros) = 5A

POL(isNatIList(x1)) = 5A + -I·x1

POL(0) = 3A

POL(nil) = 1A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
active(and(tt, X)) → mark(X)
mark(s(X)) → active(s(mark(X)))
active(isNat(s(V1))) → mark(isNat(V1))
mark(length(X)) → active(length(mark(X)))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
mark(isNat(X)) → active(isNat(X))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(0) → active(0)
mark(tt) → active(tt)
mark(nil) → active(nil)
isNatList(active(X)) → isNatList(X)
isNatList(mark(X)) → isNatList(X)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
active(isNat(0)) → mark(tt)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
isNatIList(active(X)) → isNatIList(X)
isNatIList(mark(X)) → isNatIList(X)

(99) Obligation:

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

MARK(s(X)) → MARK(X)
MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1))
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(y0, mark(x1))) → ACTIVE(U11(mark(y0), x1))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(y0, active(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(U11(x0, x1))) → ACTIVE(length(active(U11(mark(x0), x1))))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(isNatList(x0))) → ACTIVE(length(active(isNatList(x0))))
MARK(length(isNatIList(x0))) → ACTIVE(length(active(isNatIList(x0))))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(100) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(length(isNatIList(x0))) → ACTIVE(length(active(isNatIList(x0))))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(MARK(x1)) = 1A + 0A·x1

POL(s(x1)) = -I + 0A·x1

POL(U11(x1, x2)) = -I + 1A·x1 + 0A·x2

POL(ACTIVE(x1)) = 0A + 0A·x1

POL(tt) = 0A

POL(length(x1)) = -I + 0A·x1

POL(mark(x1)) = -I + 0A·x1

POL(cons(x1, x2)) = 1A + -I·x1 + 0A·x2

POL(and(x1, x2)) = 0A + -I·x1 + 0A·x2

POL(isNatList(x1)) = 3A + 4A·x1

POL(isNat(x1)) = 0A + -I·x1

POL(active(x1)) = -I + 0A·x1

POL(zeros) = 1A

POL(isNatIList(x1)) = 0A + -I·x1

POL(0) = 2A

POL(nil) = 2A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
active(and(tt, X)) → mark(X)
mark(s(X)) → active(s(mark(X)))
active(isNat(s(V1))) → mark(isNat(V1))
mark(length(X)) → active(length(mark(X)))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
mark(isNat(X)) → active(isNat(X))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(0) → active(0)
mark(tt) → active(tt)
mark(nil) → active(nil)
isNatList(active(X)) → isNatList(X)
isNatList(mark(X)) → isNatList(X)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
active(isNat(0)) → mark(tt)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
isNatIList(active(X)) → isNatIList(X)
isNatIList(mark(X)) → isNatIList(X)

(101) Obligation:

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

MARK(s(X)) → MARK(X)
MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1))
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(y0, mark(x1))) → ACTIVE(U11(mark(y0), x1))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(y0, active(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(U11(x0, x1))) → ACTIVE(length(active(U11(mark(x0), x1))))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
MARK(length(isNatList(x0))) → ACTIVE(length(active(isNatList(x0))))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(102) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(length(isNatList(x0))) → ACTIVE(length(active(isNatList(x0))))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(MARK(x1)) = 4A + 1A·x1

POL(s(x1)) = 3A + 0A·x1

POL(U11(x1, x2)) = 3A + 1A·x1 + 0A·x2

POL(ACTIVE(x1)) = 1A + 1A·x1

POL(tt) = 1A

POL(length(x1)) = 2A + 0A·x1

POL(mark(x1)) = 1A + 0A·x1

POL(cons(x1, x2)) = 3A + 2A·x1 + 0A·x2

POL(and(x1, x2)) = -I + -I·x1 + 0A·x2

POL(isNatList(x1)) = 2A + -I·x1

POL(isNat(x1)) = -I + 0A·x1

POL(active(x1)) = 1A + 0A·x1

POL(zeros) = 3A

POL(0) = 0A

POL(isNatIList(x1)) = 0A + 0A·x1

POL(nil) = 0A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
active(and(tt, X)) → mark(X)
mark(s(X)) → active(s(mark(X)))
active(isNat(s(V1))) → mark(isNat(V1))
mark(length(X)) → active(length(mark(X)))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
mark(isNat(X)) → active(isNat(X))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(0) → active(0)
mark(tt) → active(tt)
mark(nil) → active(nil)
isNatList(active(X)) → isNatList(X)
isNatList(mark(X)) → isNatList(X)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
active(isNat(0)) → mark(tt)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
isNatIList(active(X)) → isNatIList(X)
isNatIList(mark(X)) → isNatIList(X)

(103) Obligation:

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

MARK(s(X)) → MARK(X)
MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1))
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(y0, mark(x1))) → ACTIVE(U11(mark(y0), x1))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(y0, active(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(U11(x0, x1))) → ACTIVE(length(active(U11(mark(x0), x1))))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(104) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(U11(y0, mark(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(U11(y0, active(x1))) → ACTIVE(U11(mark(y0), x1))
MARK(length(U11(x0, x1))) → ACTIVE(length(active(U11(mark(x0), x1))))
MARK(length(length(x0))) → ACTIVE(length(active(length(mark(x0)))))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(MARK(x1)) = 5A + 1A·x1

POL(s(x1)) = -I + 0A·x1

POL(U11(x1, x2)) = 3A + 1A·x1 + 3A·x2

POL(ACTIVE(x1)) = 5A + 0A·x1

POL(tt) = 3A

POL(length(x1)) = 4A + 2A·x1

POL(mark(x1)) = 2A + 0A·x1

POL(cons(x1, x2)) = 2A + 0A·x1 + 2A·x2

POL(and(x1, x2)) = 2A + 0A·x1 + 0A·x2

POL(isNatList(x1)) = 3A + 2A·x1

POL(isNat(x1)) = 3A + 0A·x1

POL(active(x1)) = 2A + 0A·x1

POL(zeros) = 0A

POL(0) = 1A

POL(isNatIList(x1)) = 5A + 3A·x1

POL(nil) = 5A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
active(and(tt, X)) → mark(X)
mark(s(X)) → active(s(mark(X)))
active(isNat(s(V1))) → mark(isNat(V1))
mark(length(X)) → active(length(mark(X)))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
mark(isNat(X)) → active(isNat(X))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(0) → active(0)
mark(tt) → active(tt)
mark(nil) → active(nil)
isNatList(active(X)) → isNatList(X)
isNatList(mark(X)) → isNatList(X)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
active(isNat(0)) → mark(tt)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
isNatIList(active(X)) → isNatIList(X)
isNatIList(mark(X)) → isNatIList(X)

(105) Obligation:

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

MARK(s(X)) → MARK(X)
MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1))
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(106) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(length(cons(x0, x1))) → ACTIVE(length(active(cons(mark(x0), x1))))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(MARK(x1)) = 4A + 1A·x1

POL(s(x1)) = 4A + 0A·x1

POL(U11(x1, x2)) = 4A + 0A·x1 + 1A·x2

POL(ACTIVE(x1)) = 5A + 0A·x1

POL(tt) = 3A

POL(length(x1)) = 4A + 0A·x1

POL(cons(x1, x2)) = 5A + 0A·x1 + 5A·x2

POL(and(x1, x2)) = -I + 0A·x1 + 4A·x2

POL(isNatList(x1)) = 1A + -I·x1

POL(isNat(x1)) = 0A + -I·x1

POL(active(x1)) = 5A + 0A·x1

POL(mark(x1)) = 5A + 0A·x1

POL(zeros) = 0A

POL(0) = 0A

POL(isNatIList(x1)) = 2A + 1A·x1

POL(nil) = 5A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
isNatList(active(X)) → isNatList(X)
isNatList(mark(X)) → isNatList(X)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
active(and(tt, X)) → mark(X)
mark(s(X)) → active(s(mark(X)))
active(isNat(s(V1))) → mark(isNat(V1))
mark(length(X)) → active(length(mark(X)))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
mark(isNat(X)) → active(isNat(X))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(0) → active(0)
mark(tt) → active(tt)
mark(nil) → active(nil)
active(isNat(0)) → mark(tt)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
isNatIList(active(X)) → isNatIList(X)
isNatIList(mark(X)) → isNatIList(X)

(107) Obligation:

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

MARK(s(X)) → MARK(X)
MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1))
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(108) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(length(and(x0, x1))) → ACTIVE(length(active(and(mark(x0), x1))))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(MARK(x1)) = 3A + 1A·x1

POL(s(x1)) = 2A + 0A·x1

POL(U11(x1, x2)) = 0A + -I·x1 + 1A·x2

POL(ACTIVE(x1)) = 3A + 0A·x1

POL(tt) = 1A

POL(length(x1)) = 1A + 0A·x1

POL(cons(x1, x2)) = 0A + 0A·x1 + 2A·x2

POL(and(x1, x2)) = 3A + -I·x1 + 1A·x2

POL(isNatList(x1)) = 2A + 5A·x1

POL(isNat(x1)) = 0A + -I·x1

POL(active(x1)) = 3A + 0A·x1

POL(mark(x1)) = 3A + 1A·x1

POL(zeros) = 0A

POL(0) = 0A

POL(isNatIList(x1)) = 1A + 4A·x1

POL(nil) = 5A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
isNatList(active(X)) → isNatList(X)
isNatList(mark(X)) → isNatList(X)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
active(and(tt, X)) → mark(X)
mark(s(X)) → active(s(mark(X)))
active(isNat(s(V1))) → mark(isNat(V1))
mark(length(X)) → active(length(mark(X)))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
mark(isNat(X)) → active(isNat(X))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(0) → active(0)
mark(tt) → active(tt)
mark(nil) → active(nil)
active(isNat(0)) → mark(tt)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
isNatIList(active(X)) → isNatIList(X)
isNatIList(mark(X)) → isNatIList(X)

(109) Obligation:

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

MARK(s(X)) → MARK(X)
MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1))
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(length(x0)) → ACTIVE(length(x0))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(110) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(U11(x0, x1)) → ACTIVE(U11(x0, x1))
MARK(length(x0)) → ACTIVE(length(x0))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(MARK(x1)) = 5A + 2A·x1

POL(s(x1)) = 0A + 0A·x1

POL(U11(x1, x2)) = -I + 0A·x1 + 2A·x2

POL(ACTIVE(x1)) = 4A + 0A·x1

POL(tt) = 5A

POL(length(x1)) = 3A + 0A·x1

POL(cons(x1, x2)) = 5A + 0A·x1 + 4A·x2

POL(and(x1, x2)) = 3A + 0A·x1 + 0A·x2

POL(isNatList(x1)) = 0A + -I·x1

POL(isNat(x1)) = 0A + -I·x1

POL(active(x1)) = 5A + 0A·x1

POL(mark(x1)) = 5A + 0A·x1

POL(zeros) = 0A

POL(0) = 3A

POL(isNatIList(x1)) = 0A + 5A·x1

POL(nil) = 0A

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
isNatList(active(X)) → isNatList(X)
isNatList(mark(X)) → isNatList(X)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
active(and(tt, X)) → mark(X)
mark(s(X)) → active(s(mark(X)))
active(isNat(s(V1))) → mark(isNat(V1))
mark(length(X)) → active(length(mark(X)))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
mark(isNat(X)) → active(isNat(X))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(0) → active(0)
mark(tt) → active(tt)
mark(nil) → active(nil)
active(isNat(0)) → mark(tt)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
isNatIList(active(X)) → isNatIList(X)
isNatIList(mark(X)) → isNatIList(X)

(111) Obligation:

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

MARK(s(X)) → MARK(X)
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(112) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MARK(length(s(x0))) → ACTIVE(length(active(s(mark(x0)))))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( ACTIVE(x1) ) = max{0, x1 - 1}

POL( MARK(x1) ) = 1

POL( s(x1) ) = 0

POL( length(x1) ) = x1 + 1

POL( active(x1) ) = x1

POL( mark(x1) ) = x1

POL( U11(x1, x2) ) = 2

POL( and(x1, x2) ) = 2x1 + x2

POL( isNatList(x1) ) = 0

POL( isNat(x1) ) = 0

POL( cons(x1, x2) ) = 1

POL( zeros ) = 1

POL( 0 ) = 1

POL( tt ) = 0

POL( isNatIList(x1) ) = 1

POL( nil ) = 0


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
isNatList(active(X)) → isNatList(X)
isNatList(mark(X)) → isNatList(X)
isNat(active(X)) → isNat(X)
isNat(mark(X)) → isNat(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
mark(zeros) → active(zeros)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
active(and(tt, X)) → mark(X)
mark(s(X)) → active(s(mark(X)))
active(isNat(s(V1))) → mark(isNat(V1))
mark(length(X)) → active(length(mark(X)))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
mark(isNat(X)) → active(isNat(X))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(0) → active(0)
mark(tt) → active(tt)
mark(nil) → active(nil)
active(isNat(0)) → mark(tt)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
isNatIList(active(X)) → isNatIList(X)
isNatIList(mark(X)) → isNatIList(X)

(113) Obligation:

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

MARK(s(X)) → MARK(X)
ACTIVE(U11(tt, L)) → MARK(s(length(L)))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(114) NonMonReductionPairProof (EQUIVALENT transformation)

Using the following max-polynomial ordering, we can orient the general usable rules and all rules from P weakly and some rules from P strictly:
Polynomial interpretation with max [POLO,NEGPOLO,MAXPOLO]:

POL(0) = 1   
POL(ACTIVE(x1)) = 1 + x1   
POL(MARK(x1)) = 1 + x1   
POL(U11(x1, x2)) = max(0, 1 - x1)   
POL(active(x1)) = x1   
POL(and(x1, x2)) = max(0, x1 + x2)   
POL(cons(x1, x2)) = max(0, 0)   
POL(isNat(x1)) = 0   
POL(isNatIList(x1)) = 0   
POL(isNatList(x1)) = 1   
POL(length(x1)) = 0   
POL(mark(x1)) = x1   
POL(nil) = 1   
POL(s(x1)) = 1 + x1   
POL(tt) = 0   
POL(zeros) = 0   

The following pairs can be oriented strictly and are deleted.

MARK(s(X)) → MARK(X)
The remaining pairs can at least be oriented weakly.

ACTIVE(U11(tt, L)) → MARK(s(length(L)))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
The following rules are usable:

active(zeros) ↔ mark(cons(0, zeros))
active(U11(tt, L)) ↔ mark(s(length(L)))
active(and(tt, X)) ↔ mark(X)
active(isNat(0)) ↔ mark(tt)
active(isNat(s(V1))) ↔ mark(isNat(V1))
active(isNatIList(cons(V1, V2))) ↔ mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) ↔ mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) ↔ mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) ↔ active(zeros)
mark(cons(X1, X2)) ↔ active(cons(mark(X1), X2))
mark(0) ↔ active(0)
mark(U11(X1, X2)) ↔ active(U11(mark(X1), X2))
mark(tt) ↔ active(tt)
mark(s(X)) ↔ active(s(mark(X)))
mark(length(X)) ↔ active(length(mark(X)))
mark(and(X1, X2)) ↔ active(and(mark(X1), X2))
mark(isNat(X)) ↔ active(isNat(X))
mark(isNatList(X)) ↔ active(isNatList(X))
mark(isNatIList(X)) ↔ active(isNatIList(X))
mark(nil) ↔ active(nil)
cons(mark(X1), X2) ↔ cons(X1, X2)
cons(X1, mark(X2)) ↔ cons(X1, X2)
cons(active(X1), X2) ↔ cons(X1, X2)
cons(X1, active(X2)) ↔ cons(X1, X2)
U11(mark(X1), X2) ↔ U11(X1, X2)
U11(X1, mark(X2)) ↔ U11(X1, X2)
U11(active(X1), X2) ↔ U11(X1, X2)
U11(X1, active(X2)) ↔ U11(X1, X2)
s(mark(X)) ↔ s(X)
s(active(X)) ↔ s(X)
length(mark(X)) ↔ length(X)
length(active(X)) ↔ length(X)
and(mark(X1), X2) ↔ and(X1, X2)
and(X1, mark(X2)) ↔ and(X1, X2)
and(active(X1), X2) ↔ and(X1, X2)
and(X1, active(X2)) ↔ and(X1, X2)
isNat(mark(X)) ↔ isNat(X)
isNat(active(X)) ↔ isNat(X)
isNatList(mark(X)) ↔ isNatList(X)
isNatList(active(X)) ↔ isNatList(X)
isNatIList(mark(X)) ↔ isNatIList(X)
isNatIList(active(X)) ↔ isNatIList(X)

(115) Obligation:

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

ACTIVE(U11(tt, L)) → MARK(s(length(L)))
ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(116) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


ACTIVE(length(cons(N, L))) → MARK(U11(and(isNatList(L), isNat(N)), L))
MARK(length(zeros)) → ACTIVE(length(active(zeros)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( ACTIVE(x1) ) = x1 + 2

POL( MARK(x1) ) = 2x1 + 2

POL( s(x1) ) = max{0, -2}

POL( length(x1) ) = 1

POL( active(x1) ) = 2x1 + 1

POL( mark(x1) ) = 2x1 + 1

POL( U11(x1, x2) ) = 0

POL( and(x1, x2) ) = max{0, x1 + x2 - 1}

POL( isNatList(x1) ) = 0

POL( isNat(x1) ) = 1

POL( cons(x1, x2) ) = 2x2 + 1

POL( zeros ) = 2

POL( 0 ) = 0

POL( tt ) = 1

POL( isNatIList(x1) ) = x1 + 2

POL( nil ) = 0


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

length(active(X)) → length(X)
length(mark(X)) → length(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
U11(X1, mark(X2)) → U11(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)

(117) Obligation:

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

ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))

The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(118) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


ACTIVE(U11(tt, L)) → MARK(s(length(L)))
MARK(U11(and(x0, x1), y1)) → ACTIVE(U11(active(and(mark(x0), x1)), y1))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ACTIVE(x1)  =  ACTIVE
MARK(x1)  =  x1
s(x1)  =  s
U11(x1, x2)  =  U11

Knuth-Bendix order [KBO] with precedence:
trivial

and weight map:

s=1
ACTIVE=2
U11=3

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

s(active(X)) → s(X)
s(mark(X)) → s(X)

(119) Obligation:

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

active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(U11(X1, X2)) → active(U11(mark(X1), X2))
mark(tt) → active(tt)
mark(s(X)) → active(s(mark(X)))
mark(length(X)) → active(length(mark(X)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(isNat(X)) → active(isNat(X))
mark(isNatList(X)) → active(isNatList(X))
mark(isNatIList(X)) → active(isNatIList(X))
mark(nil) → active(nil)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
U11(mark(X1), X2) → U11(X1, X2)
U11(X1, mark(X2)) → U11(X1, X2)
U11(active(X1), X2) → U11(X1, X2)
U11(X1, active(X2)) → U11(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
length(mark(X)) → length(X)
length(active(X)) → length(X)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isNat(mark(X)) → isNat(X)
isNat(active(X)) → isNat(X)
isNatList(mark(X)) → isNatList(X)
isNatList(active(X)) → isNatList(X)
isNatIList(mark(X)) → isNatIList(X)
isNatIList(active(X)) → isNatIList(X)

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

(120) PisEmptyProof (EQUIVALENT transformation)

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

(121) YES