0 QTRS
↳1 QTRSRRRProof (⇔, 84 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 0 ms)
↳4 QTRS
↳5 QTRSRRRProof (⇔, 0 ms)
↳6 QTRS
↳7 QTRSRRRProof (⇔, 0 ms)
↳8 QTRS
↳9 QTRSRRRProof (⇔, 9 ms)
↳10 QTRS
↳11 DependencyPairsProof (⇔, 25 ms)
↳12 QDP
↳13 DependencyGraphProof (⇔, 0 ms)
↳14 AND
↳15 QDP
↳16 QDPSizeChangeProof (⇔, 0 ms)
↳17 YES
↳18 QDP
↳19 NonLoopProof (⇔, 0 ms)
↳20 NO
zeros → cons(0, n__zeros)
and(tt, X) → activate(X)
length(nil) → 0
length(cons(N, L)) → s(length(activate(L)))
take(0, IL) → nil
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(X) → X
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(activate(x1)) = x1
POL(and(x1, x2)) = 2·x1 + 2·x2
POL(cons(x1, x2)) = 2·x1 + x2
POL(length(x1)) = x1
POL(n__take(x1, x2)) = x1 + 2·x2
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = x1 + 2·x2
POL(tt) = 2
POL(zeros) = 0
and(tt, X) → activate(X)
zeros → cons(0, n__zeros)
length(nil) → 0
length(cons(N, L)) → s(length(activate(L)))
take(0, IL) → nil
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(X) → X
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(activate(x1)) = x1
POL(cons(x1, x2)) = 2·x1 + x2
POL(length(x1)) = 1 + 2·x1
POL(n__take(x1, x2)) = 2·x1 + x2
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = 2·x1 + x2
POL(zeros) = 0
length(nil) → 0
zeros → cons(0, n__zeros)
length(cons(N, L)) → s(length(activate(L)))
take(0, IL) → nil
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(X) → X
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(activate(x1)) = 2·x1
POL(cons(x1, x2)) = 2·x1 + 2·x2
POL(length(x1)) = 2·x1
POL(n__take(x1, x2)) = 1 + x1 + x2
POL(n__zeros) = 0
POL(nil) = 2
POL(s(x1)) = x1
POL(take(x1, x2)) = 2 + 2·x1 + 2·x2
POL(zeros) = 0
take(X1, X2) → n__take(X1, X2)
zeros → cons(0, n__zeros)
length(cons(N, L)) → s(length(activate(L)))
take(0, IL) → nil
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
zeros → n__zeros
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(X) → X
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(activate(x1)) = 2·x1
POL(cons(x1, x2)) = 2·x1 + 2·x2
POL(length(x1)) = x1
POL(n__take(x1, x2)) = 1 + x1 + x2
POL(n__zeros) = 0
POL(nil) = 1
POL(s(x1)) = x1
POL(take(x1, x2)) = 2 + 2·x1 + 2·x2
POL(zeros) = 0
take(0, IL) → nil
zeros → cons(0, n__zeros)
length(cons(N, L)) → s(length(activate(L)))
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
zeros → n__zeros
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(X) → X
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(activate(x1)) = 1 + 2·x1
POL(cons(x1, x2)) = 1 + 2·x1 + 2·x2
POL(length(x1)) = x1
POL(n__take(x1, x2)) = x1 + x2
POL(n__zeros) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = 1 + 2·x1 + 2·x2
POL(zeros) = 1
zeros → n__zeros
activate(X) → X
zeros → cons(0, n__zeros)
length(cons(N, L)) → s(length(activate(L)))
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
LENGTH(cons(N, L)) → LENGTH(activate(L))
LENGTH(cons(N, L)) → ACTIVATE(L)
TAKE(s(M), cons(N, IL)) → ACTIVATE(IL)
ACTIVATE(n__zeros) → ZEROS
ACTIVATE(n__take(X1, X2)) → TAKE(X1, X2)
zeros → cons(0, n__zeros)
length(cons(N, L)) → s(length(activate(L)))
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
ACTIVATE(n__take(X1, X2)) → TAKE(X1, X2)
TAKE(s(M), cons(N, IL)) → ACTIVATE(IL)
zeros → cons(0, n__zeros)
length(cons(N, L)) → s(length(activate(L)))
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
From the DPs we obtained the following set of size-change graphs:
LENGTH(cons(N, L)) → LENGTH(activate(L))
zeros → cons(0, n__zeros)
length(cons(N, L)) → s(length(activate(L)))
take(s(M), cons(N, IL)) → cons(N, n__take(M, activate(IL)))
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)