(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(nil) → 0
a__length(cons(N, L)) → a__U11(tt, L)
a__take(0, IL) → nil
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
Q is empty.
(1) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(0) = 0
POL(U11(x1, x2)) = x1 + x2
POL(U12(x1, x2)) = x1 + x2
POL(U21(x1, x2, x3, x4)) = x1 + x2 + x3 + x4
POL(U22(x1, x2, x3, x4)) = x1 + x2 + x3 + x4
POL(U23(x1, x2, x3, x4)) = x1 + x2 + x3 + x4
POL(a__U11(x1, x2)) = x1 + x2
POL(a__U12(x1, x2)) = x1 + x2
POL(a__U21(x1, x2, x3, x4)) = x1 + x2 + x3 + x4
POL(a__U22(x1, x2, x3, x4)) = x1 + x2 + x3 + x4
POL(a__U23(x1, x2, x3, x4)) = x1 + x2 + x3 + x4
POL(a__length(x1)) = 1 + x1
POL(a__take(x1, x2)) = 1 + x1 + x2
POL(a__zeros) = 0
POL(cons(x1, x2)) = x1 + x2
POL(length(x1)) = 1 + x1
POL(mark(x1)) = x1
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = 1 + x1 + x2
POL(tt) = 1
POL(zeros) = 0
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
a__length(nil) → 0
a__take(0, IL) → nil
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(cons(N, L)) → a__U11(tt, L)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
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:
A__U11(tt, L) → A__U12(tt, L)
A__U12(tt, L) → A__LENGTH(mark(L))
A__U12(tt, L) → MARK(L)
A__U21(tt, IL, M, N) → A__U22(tt, IL, M, N)
A__U22(tt, IL, M, N) → A__U23(tt, IL, M, N)
A__U23(tt, IL, M, N) → MARK(N)
A__LENGTH(cons(N, L)) → A__U11(tt, L)
A__TAKE(s(M), cons(N, IL)) → A__U21(tt, IL, M, N)
MARK(zeros) → A__ZEROS
MARK(U11(X1, X2)) → A__U11(mark(X1), X2)
MARK(U11(X1, X2)) → MARK(X1)
MARK(U12(X1, X2)) → A__U12(mark(X1), X2)
MARK(U12(X1, X2)) → MARK(X1)
MARK(length(X)) → A__LENGTH(mark(X))
MARK(length(X)) → MARK(X)
MARK(U21(X1, X2, X3, X4)) → A__U21(mark(X1), X2, X3, X4)
MARK(U21(X1, X2, X3, X4)) → MARK(X1)
MARK(U22(X1, X2, X3, X4)) → A__U22(mark(X1), X2, X3, X4)
MARK(U22(X1, X2, X3, X4)) → MARK(X1)
MARK(U23(X1, X2, X3, X4)) → A__U23(mark(X1), X2, X3, X4)
MARK(U23(X1, X2, X3, X4)) → MARK(X1)
MARK(take(X1, X2)) → A__TAKE(mark(X1), mark(X2))
MARK(take(X1, X2)) → MARK(X1)
MARK(take(X1, X2)) → MARK(X2)
MARK(cons(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(cons(N, L)) → a__U11(tt, L)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
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 1 SCC with 1 less node.
(6) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__U12(tt, L) → A__LENGTH(mark(L))
A__LENGTH(cons(N, L)) → A__U11(tt, L)
A__U11(tt, L) → A__U12(tt, L)
A__U12(tt, L) → MARK(L)
MARK(U11(X1, X2)) → A__U11(mark(X1), X2)
MARK(U11(X1, X2)) → MARK(X1)
MARK(U12(X1, X2)) → A__U12(mark(X1), X2)
MARK(U12(X1, X2)) → MARK(X1)
MARK(length(X)) → A__LENGTH(mark(X))
MARK(length(X)) → MARK(X)
MARK(U21(X1, X2, X3, X4)) → A__U21(mark(X1), X2, X3, X4)
A__U21(tt, IL, M, N) → A__U22(tt, IL, M, N)
A__U22(tt, IL, M, N) → A__U23(tt, IL, M, N)
A__U23(tt, IL, M, N) → MARK(N)
MARK(U21(X1, X2, X3, X4)) → MARK(X1)
MARK(U22(X1, X2, X3, X4)) → A__U22(mark(X1), X2, X3, X4)
MARK(U22(X1, X2, X3, X4)) → MARK(X1)
MARK(U23(X1, X2, X3, X4)) → A__U23(mark(X1), X2, X3, X4)
MARK(U23(X1, X2, X3, X4)) → MARK(X1)
MARK(take(X1, X2)) → A__TAKE(mark(X1), mark(X2))
A__TAKE(s(M), cons(N, IL)) → A__U21(tt, IL, M, N)
MARK(take(X1, X2)) → MARK(X1)
MARK(take(X1, X2)) → MARK(X2)
MARK(cons(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(cons(N, L)) → a__U11(tt, L)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(7) 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:
A__U12(tt, L) → MARK(L)
MARK(U11(X1, X2)) → A__U11(mark(X1), X2)
MARK(U11(X1, X2)) → MARK(X1)
MARK(U12(X1, X2)) → A__U12(mark(X1), X2)
MARK(U12(X1, X2)) → MARK(X1)
MARK(length(X)) → A__LENGTH(mark(X))
MARK(length(X)) → MARK(X)
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(A__LENGTH(x1)) = 1 + x1
POL(A__TAKE(x1, x2)) = x1 + x2
POL(A__U11(x1, x2)) = 1 + x1 + x2
POL(A__U12(x1, x2)) = 1 + x1 + x2
POL(A__U21(x1, x2, x3, x4)) = x1 + x2 + x3 + x4
POL(A__U22(x1, x2, x3, x4)) = x1 + x2 + x3 + x4
POL(A__U23(x1, x2, x3, x4)) = x1 + x2 + x3 + x4
POL(MARK(x1)) = x1
POL(U11(x1, x2)) = 2 + x1 + x2
POL(U12(x1, x2)) = 2 + x1 + x2
POL(U21(x1, x2, x3, x4)) = x1 + x2 + x3 + x4
POL(U22(x1, x2, x3, x4)) = x1 + x2 + x3 + x4
POL(U23(x1, x2, x3, x4)) = x1 + x2 + x3 + x4
POL(a__U11(x1, x2)) = 2 + x1 + x2
POL(a__U12(x1, x2)) = 2 + x1 + x2
POL(a__U21(x1, x2, x3, x4)) = x1 + x2 + x3 + x4
POL(a__U22(x1, x2, x3, x4)) = x1 + x2 + x3 + x4
POL(a__U23(x1, x2, x3, x4)) = x1 + x2 + x3 + x4
POL(a__length(x1)) = 2 + x1
POL(a__take(x1, x2)) = x1 + x2
POL(a__zeros) = 0
POL(cons(x1, x2)) = x1 + x2
POL(length(x1)) = 2 + x1
POL(mark(x1)) = x1
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = x1 + x2
POL(tt) = 0
POL(zeros) = 0
(8) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__U12(tt, L) → A__LENGTH(mark(L))
A__LENGTH(cons(N, L)) → A__U11(tt, L)
A__U11(tt, L) → A__U12(tt, L)
MARK(U21(X1, X2, X3, X4)) → A__U21(mark(X1), X2, X3, X4)
A__U21(tt, IL, M, N) → A__U22(tt, IL, M, N)
A__U22(tt, IL, M, N) → A__U23(tt, IL, M, N)
A__U23(tt, IL, M, N) → MARK(N)
MARK(U21(X1, X2, X3, X4)) → MARK(X1)
MARK(U22(X1, X2, X3, X4)) → A__U22(mark(X1), X2, X3, X4)
MARK(U22(X1, X2, X3, X4)) → MARK(X1)
MARK(U23(X1, X2, X3, X4)) → A__U23(mark(X1), X2, X3, X4)
MARK(U23(X1, X2, X3, X4)) → MARK(X1)
MARK(take(X1, X2)) → A__TAKE(mark(X1), mark(X2))
A__TAKE(s(M), cons(N, IL)) → A__U21(tt, IL, M, N)
MARK(take(X1, X2)) → MARK(X1)
MARK(take(X1, X2)) → MARK(X2)
MARK(cons(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(cons(N, L)) → a__U11(tt, L)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(9) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.
(10) Complex Obligation (AND)
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__U21(tt, IL, M, N) → A__U22(tt, IL, M, N)
A__U22(tt, IL, M, N) → A__U23(tt, IL, M, N)
A__U23(tt, IL, M, N) → MARK(N)
MARK(U21(X1, X2, X3, X4)) → A__U21(mark(X1), X2, X3, X4)
MARK(U21(X1, X2, X3, X4)) → MARK(X1)
MARK(U22(X1, X2, X3, X4)) → A__U22(mark(X1), X2, X3, X4)
MARK(U22(X1, X2, X3, X4)) → MARK(X1)
MARK(U23(X1, X2, X3, X4)) → A__U23(mark(X1), X2, X3, X4)
MARK(U23(X1, X2, X3, X4)) → MARK(X1)
MARK(take(X1, X2)) → A__TAKE(mark(X1), mark(X2))
A__TAKE(s(M), cons(N, IL)) → A__U21(tt, IL, M, N)
MARK(take(X1, X2)) → MARK(X1)
MARK(take(X1, X2)) → MARK(X2)
MARK(cons(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(cons(N, L)) → a__U11(tt, L)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(12) 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:
A__U21(tt, IL, M, N) → A__U22(tt, IL, M, N)
A__U22(tt, IL, M, N) → A__U23(tt, IL, M, N)
A__U23(tt, IL, M, N) → MARK(N)
MARK(U21(X1, X2, X3, X4)) → A__U21(mark(X1), X2, X3, X4)
MARK(U21(X1, X2, X3, X4)) → MARK(X1)
MARK(U22(X1, X2, X3, X4)) → A__U22(mark(X1), X2, X3, X4)
MARK(U22(X1, X2, X3, X4)) → MARK(X1)
MARK(U23(X1, X2, X3, X4)) → A__U23(mark(X1), X2, X3, X4)
MARK(U23(X1, X2, X3, X4)) → MARK(X1)
MARK(take(X1, X2)) → A__TAKE(mark(X1), mark(X2))
A__TAKE(s(M), cons(N, IL)) → A__U21(tt, IL, M, N)
MARK(take(X1, X2)) → MARK(X1)
MARK(take(X1, X2)) → MARK(X2)
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(A__TAKE(x1, x2)) = 4 + x1 + x2
POL(A__U21(x1, x2, x3, x4)) = 3 + x1 + x2 + x3 + x4
POL(A__U22(x1, x2, x3, x4)) = 2 + x1 + x2 + x3 + x4
POL(A__U23(x1, x2, x3, x4)) = 1 + x1 + x2 + x3 + x4
POL(MARK(x1)) = x1
POL(U11(x1, x2)) = x1 + x2
POL(U12(x1, x2)) = x1 + x2
POL(U21(x1, x2, x3, x4)) = 5 + x1 + x2 + x3 + x4
POL(U22(x1, x2, x3, x4)) = 5 + x1 + x2 + x3 + x4
POL(U23(x1, x2, x3, x4)) = 5 + x1 + x2 + x3 + x4
POL(a__U11(x1, x2)) = x1 + x2
POL(a__U12(x1, x2)) = x1 + x2
POL(a__U21(x1, x2, x3, x4)) = 5 + x1 + x2 + x3 + x4
POL(a__U22(x1, x2, x3, x4)) = 5 + x1 + x2 + x3 + x4
POL(a__U23(x1, x2, x3, x4)) = 5 + x1 + x2 + x3 + x4
POL(a__length(x1)) = x1
POL(a__take(x1, x2)) = 5 + x1 + x2
POL(a__zeros) = 0
POL(cons(x1, x2)) = x1 + x2
POL(length(x1)) = x1
POL(mark(x1)) = x1
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = 5 + x1 + x2
POL(tt) = 0
POL(zeros) = 0
(13) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MARK(cons(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(cons(N, L)) → a__U11(tt, L)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(14) 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.
(15) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MARK(cons(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(16) 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:
- MARK(cons(X1, X2)) → MARK(X1)
The graph contains the following edges 1 > 1
- MARK(s(X)) → MARK(X)
The graph contains the following edges 1 > 1
(17) TRUE
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__LENGTH(cons(N, L)) → A__U11(tt, L)
A__U11(tt, L) → A__U12(tt, L)
A__U12(tt, L) → A__LENGTH(mark(L))
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(cons(N, L)) → a__U11(tt, L)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(19) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
A__U12(
tt,
L) →
A__LENGTH(
mark(
L)) at position [0] we obtained the following new rules [LPAR04]:
A__U12(tt, zeros) → A__LENGTH(a__zeros)
A__U12(tt, U11(x0, x1)) → A__LENGTH(a__U11(mark(x0), x1))
A__U12(tt, U12(x0, x1)) → A__LENGTH(a__U12(mark(x0), x1))
A__U12(tt, length(x0)) → A__LENGTH(a__length(mark(x0)))
A__U12(tt, U21(x0, x1, x2, x3)) → A__LENGTH(a__U21(mark(x0), x1, x2, x3))
A__U12(tt, U22(x0, x1, x2, x3)) → A__LENGTH(a__U22(mark(x0), x1, x2, x3))
A__U12(tt, U23(x0, x1, x2, x3)) → A__LENGTH(a__U23(mark(x0), x1, x2, x3))
A__U12(tt, take(x0, x1)) → A__LENGTH(a__take(mark(x0), mark(x1)))
A__U12(tt, cons(x0, x1)) → A__LENGTH(cons(mark(x0), x1))
A__U12(tt, 0) → A__LENGTH(0)
A__U12(tt, tt) → A__LENGTH(tt)
A__U12(tt, s(x0)) → A__LENGTH(s(mark(x0)))
A__U12(tt, nil) → A__LENGTH(nil)
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__LENGTH(cons(N, L)) → A__U11(tt, L)
A__U11(tt, L) → A__U12(tt, L)
A__U12(tt, zeros) → A__LENGTH(a__zeros)
A__U12(tt, U11(x0, x1)) → A__LENGTH(a__U11(mark(x0), x1))
A__U12(tt, U12(x0, x1)) → A__LENGTH(a__U12(mark(x0), x1))
A__U12(tt, length(x0)) → A__LENGTH(a__length(mark(x0)))
A__U12(tt, U21(x0, x1, x2, x3)) → A__LENGTH(a__U21(mark(x0), x1, x2, x3))
A__U12(tt, U22(x0, x1, x2, x3)) → A__LENGTH(a__U22(mark(x0), x1, x2, x3))
A__U12(tt, U23(x0, x1, x2, x3)) → A__LENGTH(a__U23(mark(x0), x1, x2, x3))
A__U12(tt, take(x0, x1)) → A__LENGTH(a__take(mark(x0), mark(x1)))
A__U12(tt, cons(x0, x1)) → A__LENGTH(cons(mark(x0), x1))
A__U12(tt, 0) → A__LENGTH(0)
A__U12(tt, tt) → A__LENGTH(tt)
A__U12(tt, s(x0)) → A__LENGTH(s(mark(x0)))
A__U12(tt, nil) → A__LENGTH(nil)
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(cons(N, L)) → a__U11(tt, L)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(21) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 4 less nodes.
(22) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__U11(tt, L) → A__U12(tt, L)
A__U12(tt, zeros) → A__LENGTH(a__zeros)
A__LENGTH(cons(N, L)) → A__U11(tt, L)
A__U12(tt, U11(x0, x1)) → A__LENGTH(a__U11(mark(x0), x1))
A__U12(tt, U12(x0, x1)) → A__LENGTH(a__U12(mark(x0), x1))
A__U12(tt, length(x0)) → A__LENGTH(a__length(mark(x0)))
A__U12(tt, U21(x0, x1, x2, x3)) → A__LENGTH(a__U21(mark(x0), x1, x2, x3))
A__U12(tt, U22(x0, x1, x2, x3)) → A__LENGTH(a__U22(mark(x0), x1, x2, x3))
A__U12(tt, U23(x0, x1, x2, x3)) → A__LENGTH(a__U23(mark(x0), x1, x2, x3))
A__U12(tt, take(x0, x1)) → A__LENGTH(a__take(mark(x0), mark(x1)))
A__U12(tt, cons(x0, x1)) → A__LENGTH(cons(mark(x0), x1))
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(cons(N, L)) → a__U11(tt, L)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(23) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
A__U12(
tt,
zeros) →
A__LENGTH(
a__zeros) at position [0] we obtained the following new rules [LPAR04]:
A__U12(tt, zeros) → A__LENGTH(cons(0, zeros))
A__U12(tt, zeros) → A__LENGTH(zeros)
(24) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__U11(tt, L) → A__U12(tt, L)
A__LENGTH(cons(N, L)) → A__U11(tt, L)
A__U12(tt, U11(x0, x1)) → A__LENGTH(a__U11(mark(x0), x1))
A__U12(tt, U12(x0, x1)) → A__LENGTH(a__U12(mark(x0), x1))
A__U12(tt, length(x0)) → A__LENGTH(a__length(mark(x0)))
A__U12(tt, U21(x0, x1, x2, x3)) → A__LENGTH(a__U21(mark(x0), x1, x2, x3))
A__U12(tt, U22(x0, x1, x2, x3)) → A__LENGTH(a__U22(mark(x0), x1, x2, x3))
A__U12(tt, U23(x0, x1, x2, x3)) → A__LENGTH(a__U23(mark(x0), x1, x2, x3))
A__U12(tt, take(x0, x1)) → A__LENGTH(a__take(mark(x0), mark(x1)))
A__U12(tt, cons(x0, x1)) → A__LENGTH(cons(mark(x0), x1))
A__U12(tt, zeros) → A__LENGTH(cons(0, zeros))
A__U12(tt, zeros) → A__LENGTH(zeros)
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(cons(N, L)) → a__U11(tt, L)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(25) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(26) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__U12(tt, U11(x0, x1)) → A__LENGTH(a__U11(mark(x0), x1))
A__LENGTH(cons(N, L)) → A__U11(tt, L)
A__U11(tt, L) → A__U12(tt, L)
A__U12(tt, U12(x0, x1)) → A__LENGTH(a__U12(mark(x0), x1))
A__U12(tt, length(x0)) → A__LENGTH(a__length(mark(x0)))
A__U12(tt, U21(x0, x1, x2, x3)) → A__LENGTH(a__U21(mark(x0), x1, x2, x3))
A__U12(tt, U22(x0, x1, x2, x3)) → A__LENGTH(a__U22(mark(x0), x1, x2, x3))
A__U12(tt, U23(x0, x1, x2, x3)) → A__LENGTH(a__U23(mark(x0), x1, x2, x3))
A__U12(tt, take(x0, x1)) → A__LENGTH(a__take(mark(x0), mark(x1)))
A__U12(tt, cons(x0, x1)) → A__LENGTH(cons(mark(x0), x1))
A__U12(tt, zeros) → A__LENGTH(cons(0, zeros))
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(cons(N, L)) → a__U11(tt, L)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(27) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
A__U12(tt, length(x0)) → A__LENGTH(a__length(mark(x0)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(A__U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(A__LENGTH(x1)) = | | + | | · | x1 |
POL(a__U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(A__U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__length(x1)) = | | + | | · | x1 |
POL(U21(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U21(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(U22(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U22(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(U23(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U23(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(take(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__take(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U12(tt, L) → s(a__length(mark(L)))
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
a__length(cons(N, L)) → a__U11(tt, L)
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(zeros) → a__zeros
a__U11(tt, L) → a__U12(tt, L)
a__zeros → cons(0, zeros)
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
a__take(X1, X2) → take(X1, X2)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
(28) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__U12(tt, U11(x0, x1)) → A__LENGTH(a__U11(mark(x0), x1))
A__LENGTH(cons(N, L)) → A__U11(tt, L)
A__U11(tt, L) → A__U12(tt, L)
A__U12(tt, U12(x0, x1)) → A__LENGTH(a__U12(mark(x0), x1))
A__U12(tt, U21(x0, x1, x2, x3)) → A__LENGTH(a__U21(mark(x0), x1, x2, x3))
A__U12(tt, U22(x0, x1, x2, x3)) → A__LENGTH(a__U22(mark(x0), x1, x2, x3))
A__U12(tt, U23(x0, x1, x2, x3)) → A__LENGTH(a__U23(mark(x0), x1, x2, x3))
A__U12(tt, take(x0, x1)) → A__LENGTH(a__take(mark(x0), mark(x1)))
A__U12(tt, cons(x0, x1)) → A__LENGTH(cons(mark(x0), x1))
A__U12(tt, zeros) → A__LENGTH(cons(0, zeros))
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(cons(N, L)) → a__U11(tt, L)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(29) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
A__U12(tt, cons(x0, x1)) → A__LENGTH(cons(mark(x0), x1))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(A__U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(A__LENGTH(x1)) = | | + | | · | x1 |
POL(a__U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(A__U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U21(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U21(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(U22(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U22(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(U23(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U23(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(take(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__take(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__length(x1)) = | | + | | · | x1 |
The following usable rules [FROCOS05] were oriented:
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U12(tt, L) → s(a__length(mark(L)))
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
a__length(cons(N, L)) → a__U11(tt, L)
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
a__U11(tt, L) → a__U12(tt, L)
mark(s(X)) → s(mark(X))
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
a__take(X1, X2) → take(X1, X2)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
(30) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__U12(tt, U11(x0, x1)) → A__LENGTH(a__U11(mark(x0), x1))
A__LENGTH(cons(N, L)) → A__U11(tt, L)
A__U11(tt, L) → A__U12(tt, L)
A__U12(tt, U12(x0, x1)) → A__LENGTH(a__U12(mark(x0), x1))
A__U12(tt, U21(x0, x1, x2, x3)) → A__LENGTH(a__U21(mark(x0), x1, x2, x3))
A__U12(tt, U22(x0, x1, x2, x3)) → A__LENGTH(a__U22(mark(x0), x1, x2, x3))
A__U12(tt, U23(x0, x1, x2, x3)) → A__LENGTH(a__U23(mark(x0), x1, x2, x3))
A__U12(tt, take(x0, x1)) → A__LENGTH(a__take(mark(x0), mark(x1)))
A__U12(tt, zeros) → A__LENGTH(cons(0, zeros))
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(cons(N, L)) → a__U11(tt, L)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(31) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
A__U12(tt, U12(x0, x1)) → A__LENGTH(a__U12(mark(x0), x1))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(A__U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(A__LENGTH(x1)) = | | + | | · | x1 |
POL(a__U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(A__U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U21(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U21(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(U22(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U22(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(U23(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U23(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(take(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__take(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__length(x1)) = | | + | | · | x1 |
The following usable rules [FROCOS05] were oriented:
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U12(tt, L) → s(a__length(mark(L)))
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
a__length(cons(N, L)) → a__U11(tt, L)
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
a__U11(tt, L) → a__U12(tt, L)
mark(s(X)) → s(mark(X))
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
a__take(X1, X2) → take(X1, X2)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
(32) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__U12(tt, U11(x0, x1)) → A__LENGTH(a__U11(mark(x0), x1))
A__LENGTH(cons(N, L)) → A__U11(tt, L)
A__U11(tt, L) → A__U12(tt, L)
A__U12(tt, U21(x0, x1, x2, x3)) → A__LENGTH(a__U21(mark(x0), x1, x2, x3))
A__U12(tt, U22(x0, x1, x2, x3)) → A__LENGTH(a__U22(mark(x0), x1, x2, x3))
A__U12(tt, U23(x0, x1, x2, x3)) → A__LENGTH(a__U23(mark(x0), x1, x2, x3))
A__U12(tt, take(x0, x1)) → A__LENGTH(a__take(mark(x0), mark(x1)))
A__U12(tt, zeros) → A__LENGTH(cons(0, zeros))
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(cons(N, L)) → a__U11(tt, L)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(33) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
A__U12(tt, U11(x0, x1)) → A__LENGTH(a__U11(mark(x0), x1))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(A__U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(A__LENGTH(x1)) = | | + | | · | x1 |
POL(a__U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(A__U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U21(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U21(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(U22(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U22(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(U23(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U23(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(take(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__take(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__length(x1)) = | | + | | · | x1 |
POL(U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U12(tt, L) → s(a__length(mark(L)))
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
a__length(cons(N, L)) → a__U11(tt, L)
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
a__U11(tt, L) → a__U12(tt, L)
mark(s(X)) → s(mark(X))
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
a__take(X1, X2) → take(X1, X2)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
(34) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__LENGTH(cons(N, L)) → A__U11(tt, L)
A__U11(tt, L) → A__U12(tt, L)
A__U12(tt, U21(x0, x1, x2, x3)) → A__LENGTH(a__U21(mark(x0), x1, x2, x3))
A__U12(tt, U22(x0, x1, x2, x3)) → A__LENGTH(a__U22(mark(x0), x1, x2, x3))
A__U12(tt, U23(x0, x1, x2, x3)) → A__LENGTH(a__U23(mark(x0), x1, x2, x3))
A__U12(tt, take(x0, x1)) → A__LENGTH(a__take(mark(x0), mark(x1)))
A__U12(tt, zeros) → A__LENGTH(cons(0, zeros))
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(cons(N, L)) → a__U11(tt, L)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(35) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
A__U12(tt, U22(x0, x1, x2, x3)) → A__LENGTH(a__U22(mark(x0), x1, x2, x3))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(A__LENGTH(x1)) = | | + | | · | x1 |
POL(cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(A__U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(A__U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U21(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U21(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(U22(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U22(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(U23(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U23(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(take(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__take(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__length(x1)) = | | + | | · | x1 |
POL(a__U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U12(tt, L) → s(a__length(mark(L)))
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
a__length(cons(N, L)) → a__U11(tt, L)
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
a__U11(tt, L) → a__U12(tt, L)
mark(s(X)) → s(mark(X))
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
a__take(X1, X2) → take(X1, X2)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
(36) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__LENGTH(cons(N, L)) → A__U11(tt, L)
A__U11(tt, L) → A__U12(tt, L)
A__U12(tt, U21(x0, x1, x2, x3)) → A__LENGTH(a__U21(mark(x0), x1, x2, x3))
A__U12(tt, U23(x0, x1, x2, x3)) → A__LENGTH(a__U23(mark(x0), x1, x2, x3))
A__U12(tt, take(x0, x1)) → A__LENGTH(a__take(mark(x0), mark(x1)))
A__U12(tt, zeros) → A__LENGTH(cons(0, zeros))
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(cons(N, L)) → a__U11(tt, L)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(37) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
A__U12(tt, U23(x0, x1, x2, x3)) → A__LENGTH(a__U23(mark(x0), x1, x2, x3))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(A__LENGTH(x1)) = | | + | | · | x1 |
POL(cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(A__U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(A__U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U21(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U21(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(U23(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U23(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(take(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__take(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__U22(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__length(x1)) = | | + | | · | x1 |
POL(a__U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U22(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
The following usable rules [FROCOS05] were oriented:
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U12(tt, L) → s(a__length(mark(L)))
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
a__length(cons(N, L)) → a__U11(tt, L)
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(zeros) → a__zeros
a__U11(tt, L) → a__U12(tt, L)
a__zeros → cons(0, zeros)
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
a__take(X1, X2) → take(X1, X2)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
(38) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__LENGTH(cons(N, L)) → A__U11(tt, L)
A__U11(tt, L) → A__U12(tt, L)
A__U12(tt, U21(x0, x1, x2, x3)) → A__LENGTH(a__U21(mark(x0), x1, x2, x3))
A__U12(tt, take(x0, x1)) → A__LENGTH(a__take(mark(x0), mark(x1)))
A__U12(tt, zeros) → A__LENGTH(cons(0, zeros))
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(cons(N, L)) → a__U11(tt, L)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(39) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
A__U12(tt, U21(x0, x1, x2, x3)) → A__LENGTH(a__U21(mark(x0), x1, x2, x3))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(A__LENGTH(x1)) = | | + | | · | x1 |
POL(cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(A__U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(A__U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U21(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U21(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(take(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__take(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__U22(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(a__length(x1)) = | | + | | · | x1 |
POL(a__U23(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(a__U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U12(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U22(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(U23(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
The following usable rules [FROCOS05] were oriented:
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U12(tt, L) → s(a__length(mark(L)))
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
a__length(cons(N, L)) → a__U11(tt, L)
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
a__U11(tt, L) → a__U12(tt, L)
mark(s(X)) → s(mark(X))
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
a__take(X1, X2) → take(X1, X2)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
(40) Obligation:
Q DP problem:
The TRS P consists of the following rules:
A__LENGTH(cons(N, L)) → A__U11(tt, L)
A__U11(tt, L) → A__U12(tt, L)
A__U12(tt, take(x0, x1)) → A__LENGTH(a__take(mark(x0), mark(x1)))
A__U12(tt, zeros) → A__LENGTH(cons(0, zeros))
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt, L) → a__U12(tt, L)
a__U12(tt, L) → s(a__length(mark(L)))
a__U21(tt, IL, M, N) → a__U22(tt, IL, M, N)
a__U22(tt, IL, M, N) → a__U23(tt, IL, M, N)
a__U23(tt, IL, M, N) → cons(mark(N), take(M, IL))
a__length(cons(N, L)) → a__U11(tt, L)
a__take(s(M), cons(N, IL)) → a__U21(tt, IL, M, N)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X1, X2)) → a__U12(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(U21(X1, X2, X3, X4)) → a__U21(mark(X1), X2, X3, X4)
mark(U22(X1, X2, X3, X4)) → a__U22(mark(X1), X2, X3, X4)
mark(U23(X1, X2, X3, X4)) → a__U23(mark(X1), X2, X3, X4)
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X1, X2) → U12(X1, X2)
a__length(X) → length(X)
a__U21(X1, X2, X3, X4) → U21(X1, X2, X3, X4)
a__U22(X1, X2, X3, X4) → U22(X1, X2, X3, X4)
a__U23(X1, X2, X3, X4) → U23(X1, X2, X3, X4)
a__take(X1, X2) → take(X1, X2)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(41) NonTerminationProof (EQUIVALENT transformation)
We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:
s =
A__U11(
tt,
zeros) evaluates to t =
A__U11(
tt,
zeros)
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Matcher: [ ]
- Semiunifier: [ ]
Rewriting sequenceA__U11(tt, zeros) →
A__U12(
tt,
zeros)
with rule
A__U11(
tt,
L) →
A__U12(
tt,
L) at position [] and matcher [
L /
zeros]
A__U12(tt, zeros) →
A__LENGTH(
cons(
0,
zeros))
with rule
A__U12(
tt,
zeros) →
A__LENGTH(
cons(
0,
zeros)) at position [] and matcher [ ]
A__LENGTH(cons(0, zeros)) →
A__U11(
tt,
zeros)
with rule
A__LENGTH(
cons(
N,
L)) →
A__U11(
tt,
L)
Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence
All these steps are and every following step will be a correct step w.r.t to Q.
(42) FALSE