Termination w.r.t. Q proof of Transformed_CSR_04_LengthOfFiniteLists_nokinds

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

0 QTRS

↳1 QTRSToCSRProof (⇔, 0 ms)

↳2 CSR

↳3 CSRRRRProof (⇔, 38 ms)

↳4 CSR

↳5 CSRRRRProof (⇔, 0 ms)

↳6 CSR

↳7 CSRRRRProof (⇔, 0 ms)

↳8 CSR

↳9 CSRInnermostProof (⇔, 0 ms)

↳10 CSR

↳11 CSDependencyPairsProof (⇔, 0 ms)

↳12 QCSDP

↳13 QCSDependencyGraphProof (⇔, 0 ms)

↳14 AND

    ↳15 QCSDP

        ↳16 QCSDPSubtermProof (⇔, 0 ms)

        ↳17 QCSDP

        ↳18 PIsEmptyProof (⇔, 0 ms)

        ↳19 YES

    ↳20 QCSDP

        ↳21 QCSUsableRulesProof (⇔, 0 ms)

        ↳22 QCSDP

        ↳23 QCSDPMuMonotonicPoloProof (⇔, 0 ms)

        ↳24 QCSDP

        ↳25 QCSDependencyGraphProof (⇔, 0 ms)

        ↳26 TRUE

    ↳27 QCSDP

        ↳28 QCSDPReductionPairProof (⇔, 8 ms)

        ↳29 QCSDP

        ↳30 QCSDependencyGraphProof (⇔, 0 ms)

        ↳31 TRUE

(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))
active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X1, X2)) → U11(active(X1), X2)
active(s(X)) → s(active(X))
active(length(X)) → length(active(X))
active(and(X1, X2)) → and(active(X1), X2)
cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))
s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))
and(mark(X1), X2) → mark(and(X1, X2))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))
proper(isNatList(X)) → isNatList(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))
proper(nil) → ok(nil)
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))
s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNat(ok(X)) → ok(isNat(X))
isNatList(ok(X)) → ok(isNatList(X))
isNatIList(ok(X)) → ok(isNatIList(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.

(1) QTRSToCSRProof (EQUIVALENT transformation)

The following Q TRS is given: 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))
active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X1, X2)) → U11(active(X1), X2)
active(s(X)) → s(active(X))
active(length(X)) → length(active(X))
active(and(X1, X2)) → and(active(X1), X2)
cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))
s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))
and(mark(X1), X2) → mark(and(X1, X2))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))
proper(isNatList(X)) → isNatList(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))
proper(nil) → ok(nil)
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))
s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNat(ok(X)) → ok(isNat(X))
isNatList(ok(X)) → ok(isNatList(X))
isNatIList(ok(X)) → ok(isNatIList(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
Special symbols used for the transformation (see [GM04]):
top: top, active: active, mark: mark, ok: ok, proper: proper
The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
s: {1}
length: {1}
and: {1}
isNat: empty set
isNatList: empty set
isNatIList: empty set
nil: empty set
The QTRS contained all rules created by the complete Giesl-Middeldorp transformation. Therefore, the inverse transformation is complete (and sound).

(2) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
s: {1}
length: {1}
and: {1}
isNat: empty set
isNatList: empty set
isNatIList: empty set
nil: empty set

(3) CSRRRRProof (EQUIVALENT transformation)

The following CSR is given: Context-sensitive rewrite system:
The TRS R consists of the following rules:

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

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
s: {1}
length: {1}
and: {1}
isNat: empty set
isNatList: empty set
isNatIList: empty set
nil: empty set
Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0
POL(U11(x₁, x₂)) = 2·x₁ + 2·x₂
POL(and(x₁, x₂)) = x₁ + 2·x₂
POL(cons(x₁, x₂)) = x₁ + 2·x₂
POL(isNat(x₁)) = 0
POL(isNatIList(x₁)) = 0
POL(isNatList(x₁)) = 0
POL(length(x₁)) = x₁
POL(nil) = 1
POL(s(x₁)) = x₁
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:

length(nil) → 0

(4) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
s: {1}
length: {1}
and: {1}
isNat: empty set
isNatList: empty set
isNatIList: empty set
nil: empty set

(5) CSRRRRProof (EQUIVALENT transformation)

The following CSR is given: Context-sensitive rewrite system:
The TRS R consists of the following rules:

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

The replacement map contains the following entries:

POL(0) = 0
POL(U11(x₁, x₂)) = x₁ + x₂
POL(and(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₁ + x₂
POL(isNat(x₁)) = 0
POL(isNatIList(x₁)) = 1 + x₁
POL(isNatList(x₁)) = 0
POL(length(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 1

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt

(6) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
s: {1}
length: {1}
and: {1}
isNat: empty set
isNatList: empty set
isNatIList: empty set
nil: empty set

(7) CSRRRRProof (EQUIVALENT transformation)

The following CSR is given: Context-sensitive rewrite system:
The TRS R consists of the following rules:

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

The replacement map contains the following entries:

POL(0) = 0
POL(U11(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(and(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₁ + 2·x₂
POL(isNat(x₁)) = 2·x₁
POL(isNatIList(x₁)) = 2·x₁
POL(isNatList(x₁)) = 2·x₁
POL(length(x₁)) = 1 + 2·x₁
POL(nil) = 2
POL(s(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 0

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

isNat(length(V1)) → isNatList(V1)
isNatList(nil) → tt

(8) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
s: {1}
length: {1}
and: {1}
isNat: empty set
isNatList: empty set
isNatIList: empty set

(9) CSRInnermostProof (EQUIVALENT transformation)

The CSR is orthogonal. By [CS_Inn] we can switch to innermost.

(10) Obligation:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

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

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
s: {1}
length: {1}
and: {1}
isNat: empty set
isNatList: empty set
isNatIList: empty set

Innermost Strategy.

(11) CSDependencyPairsProof (EQUIVALENT transformation)

Using Improved CS-DPs [LPAR08] we result in the following initial Q-CSDP problem.

(12) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, LENGTH} are replacing on all positions.
For all symbols f in {cons, U11, and, U11', AND} we have µ(f) = {1}.
The symbols in {isNat, isNatIList, isNatList, ISNAT, ISNATILIST, ISNATLIST, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DP_o are:

U11'(tt, L) → LENGTH(L)
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
LENGTH(cons(N, L)) → U11'(and(isNatList(L), isNat(N)), L)
LENGTH(cons(N, L)) → AND(isNatList(L), isNat(N))
LENGTH(cons(N, L)) → ISNATLIST(L)

The collapsing dependency pairs are DP_c:

U11'(tt, L) → L
AND(tt, X) → X

The hidden terms of R are:

zeros
isNatIList(x0)
isNatList(x0)
isNat(x0)

Every hiding context is built from:none

Hence, the new unhiding pairs DP_u are :

U11'(tt, L) → U(L)
AND(tt, X) → U(X)
U(zeros) → ZEROS
U(isNatIList(x0)) → ISNATILIST(x0)
U(isNatList(x0)) → ISNATLIST(x0)
U(isNat(x0)) → ISNAT(x0)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

zeros
U11(tt, x0)
and(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))

(13) QCSDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Context-Sensitive Dependency Graph [LPAR08] contains 3 SCCs with 7 less nodes.

(14) Complex Obligation (AND)

(15) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length} are replacing on all positions.
For all symbols f in {cons, U11, and} we have µ(f) = {1}.
The symbols in {isNat, isNatIList, isNatList, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

ISNAT(s(V1)) → ISNAT(V1)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

zeros
U11(tt, x0)
and(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))

(16) QCSDPSubtermProof (EQUIVALENT transformation)

We use the subterm processor [DA_EMMES].

The following pairs can be oriented strictly and are deleted.

ISNAT(s(V1)) → ISNAT(V1)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
ISNAT(x1) = x1

Subterm Order

(17) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length} are replacing on all positions.
For all symbols f in {cons, U11, and} we have µ(f) = {1}.
The symbols in {isNat, isNatIList, isNatList} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

zeros
U11(tt, x0)
and(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))

(18) PIsEmptyProof (EQUIVALENT transformation)

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

(19) YES

(20) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length} are replacing on all positions.
For all symbols f in {cons, U11, and, AND} we have µ(f) = {1}.
The symbols in {isNat, isNatIList, isNatList, ISNATILIST, U, ISNATLIST} are not replacing on any position.

The TRS P consists of the following rules:

ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
AND(tt, X) → U(X)
U(isNatIList(x0)) → ISNATILIST(x0)
U(isNatList(x0)) → ISNATLIST(x0)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

zeros
U11(tt, x0)
and(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))

(21) QCSUsableRulesProof (EQUIVALENT transformation)

The following rules are not useable [DA_EMMES] and can be deleted:

zeros → cons(0, zeros)
U11(tt, x0) → s(length(x0))
and(tt, x0) → x0
isNatIList(cons(x0, x1)) → and(isNat(x0), isNatIList(x1))
isNatList(cons(x0, x1)) → and(isNat(x0), isNatList(x1))
length(cons(x0, x1)) → U11(and(isNatList(x1), isNat(x0)), x1)

(22) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length} are replacing on all positions.
For all symbols f in {cons, AND, U11, and} we have µ(f) = {1}.
The symbols in {isNat, isNatIList, isNatList, ISNATILIST, U, ISNATLIST} are not replacing on any position.

The TRS P consists of the following rules:

ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
AND(tt, X) → U(X)
U(isNatIList(x0)) → ISNATILIST(x0)
U(isNatList(x0)) → ISNATLIST(x0)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))

The TRS R consists of the following rules:

isNat(0) → tt
isNat(s(V1)) → isNat(V1)

The set Q consists of the following terms:

zeros
U11(tt, x0)
and(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))

(23) QCSDPMuMonotonicPoloProof (EQUIVALENT transformation)

By using the following µ-monotonic polynomial ordering [POLO], at least one Dependency Pair or term rewrite system rule of this Q-CSDP problem can be strictly oriented and thus deleted.
Strictly oriented dependency pairs:

ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
U(isNatIList(x0)) → ISNATILIST(x0)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(0) = 1
POL(AND(x₁, x₂)) = x₁ + 2·x₂
POL(ISNATILIST(x₁)) = x₁
POL(ISNATLIST(x₁)) = 2 + x₁
POL(U(x₁)) = 2 + x₁
POL(cons(x₁, x₂)) = 1 + 2·x₁ + 2·x₂
POL(isNat(x₁)) = 2·x₁
POL(isNatIList(x₁)) = x₁
POL(isNatList(x₁)) = x₁
POL(s(x₁)) = 2·x₁
POL(tt) = 2

(24) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length} are replacing on all positions.
For all symbols f in {AND, U11, and, cons} we have µ(f) = {1}.
The symbols in {isNat, isNatList, U, ISNATLIST, isNatIList} are not replacing on any position.

The TRS P consists of the following rules:

AND(tt, X) → U(X)
U(isNatList(x0)) → ISNATLIST(x0)

The TRS R consists of the following rules:

isNat(0) → tt
isNat(s(V1)) → isNat(V1)

The set Q consists of the following terms:

zeros
U11(tt, x0)
and(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))

(25) QCSDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Context-Sensitive Dependency Graph [LPAR08] contains 0 SCCs with 2 less nodes.

(26) TRUE

(27) Obligation:

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, LENGTH} are replacing on all positions.
For all symbols f in {cons, U11, and, U11'} we have µ(f) = {1}.
The symbols in {isNat, isNatIList, isNatList} are not replacing on any position.

The TRS P consists of the following rules:

LENGTH(cons(N, L)) → U11'(and(isNatList(L), isNat(N)), L)
U11'(tt, L) → LENGTH(L)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

zeros
U11(tt, x0)
and(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))

(28) QCSDPReductionPairProof (EQUIVALENT transformation)

Using the order
Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( and(x₁, x₂) ) = max{0, x₁ + x₂ - 1}

POL( tt ) = 1

POL( isNatList(x₁) ) = 0

POL( cons(x₁, x₂) ) = max{0, 2x₂ - 1}

POL( isNat(x₁) ) = 1

POL( 0 ) = 2

POL( s(x₁) ) = x₁

POL( zeros ) = 1

POL( isNatIList(x₁) ) = 2

POL( LENGTH(x₁) ) = 1

POL( U11'(x₁, x₂) ) = 2x₁ + 1

the following usable rules

and(tt, X) → X
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNat(0) → tt
isNat(s(V1)) → isNat(V1)
zeros → cons(0, zeros)
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))

could all be oriented weakly.
Furthermore, the pairs

U11'(tt, L) → LENGTH(L)

could be oriented strictly and thus removed by the CS-Reduction Pair Processor [LPAR08,DA_EMMES].

(29) Obligation:

LENGTH(cons(N, L)) → U11'(and(isNatList(L), isNat(N)), L)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

zeros
U11(tt, x0)
and(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))

(30) QCSDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Context-Sensitive Dependency Graph [LPAR08] contains 0 SCCs with 1 less node.

(0) Obligation:

(1) QTRSToCSRProof (EQUIVALENT transformation)

(2) Obligation:

(3) CSRRRRProof (EQUIVALENT transformation)

(4) Obligation:

(5) CSRRRRProof (EQUIVALENT transformation)

(6) Obligation:

(7) CSRRRRProof (EQUIVALENT transformation)

(8) Obligation:

(9) CSRInnermostProof (EQUIVALENT transformation)

(10) Obligation:

(11) CSDependencyPairsProof (EQUIVALENT transformation)

(12) Obligation:

(13) QCSDependencyGraphProof (EQUIVALENT transformation)

(14) Complex Obligation (AND)

(15) Obligation:

(16) QCSDPSubtermProof (EQUIVALENT transformation)

(17) Obligation:

(18) PIsEmptyProof (EQUIVALENT transformation)

(19) YES

(20) Obligation:

(21) QCSUsableRulesProof (EQUIVALENT transformation)

(22) Obligation:

(23) QCSDPMuMonotonicPoloProof (EQUIVALENT transformation)

(24) Obligation:

(25) QCSDependencyGraphProof (EQUIVALENT transformation)

(26) TRUE

(27) Obligation:

(28) QCSDPReductionPairProof (EQUIVALENT transformation)

(29) Obligation:

(30) QCSDependencyGraphProof (EQUIVALENT transformation)

(31) TRUE