MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , and(tt(), X) -> activate(X) , activate(X) -> X , activate(n__zeros()) -> zeros() , activate(n__take(X1, X2)) -> take(X1, X2) , length(cons(N, L)) -> s(length(activate(L))) , length(nil()) -> 0() , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> nil() , take(s(M), cons(N, IL)) -> cons(N, n__take(M, activate(IL))) } Obligation: innermost runtime complexity Answer: MAYBE We add following weak dependency pairs: Strict DPs: { zeros^#() -> c_1() , zeros^#() -> c_2() , and^#(tt(), X) -> c_3(activate^#(X)) , activate^#(X) -> c_4() , activate^#(n__zeros()) -> c_5(zeros^#()) , activate^#(n__take(X1, X2)) -> c_6(take^#(X1, X2)) , take^#(X1, X2) -> c_9() , take^#(0(), IL) -> c_10() , take^#(s(M), cons(N, IL)) -> c_11(activate^#(IL)) , length^#(cons(N, L)) -> c_7(length^#(activate(L))) , length^#(nil()) -> c_8() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { zeros^#() -> c_1() , zeros^#() -> c_2() , and^#(tt(), X) -> c_3(activate^#(X)) , activate^#(X) -> c_4() , activate^#(n__zeros()) -> c_5(zeros^#()) , activate^#(n__take(X1, X2)) -> c_6(take^#(X1, X2)) , take^#(X1, X2) -> c_9() , take^#(0(), IL) -> c_10() , take^#(s(M), cons(N, IL)) -> c_11(activate^#(IL)) , length^#(cons(N, L)) -> c_7(length^#(activate(L))) , length^#(nil()) -> c_8() } Strict Trs: { zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , and(tt(), X) -> activate(X) , activate(X) -> X , activate(n__zeros()) -> zeros() , activate(n__take(X1, X2)) -> take(X1, X2) , length(cons(N, L)) -> s(length(activate(L))) , length(nil()) -> 0() , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> nil() , take(s(M), cons(N, IL)) -> cons(N, n__take(M, activate(IL))) } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Strict Usable Rules: { zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , activate(X) -> X , activate(n__zeros()) -> zeros() , activate(n__take(X1, X2)) -> take(X1, X2) , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> nil() , take(s(M), cons(N, IL)) -> cons(N, n__take(M, activate(IL))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { zeros^#() -> c_1() , zeros^#() -> c_2() , and^#(tt(), X) -> c_3(activate^#(X)) , activate^#(X) -> c_4() , activate^#(n__zeros()) -> c_5(zeros^#()) , activate^#(n__take(X1, X2)) -> c_6(take^#(X1, X2)) , take^#(X1, X2) -> c_9() , take^#(0(), IL) -> c_10() , take^#(s(M), cons(N, IL)) -> c_11(activate^#(IL)) , length^#(cons(N, L)) -> c_7(length^#(activate(L))) , length^#(nil()) -> c_8() } Strict Trs: { zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , activate(X) -> X , activate(n__zeros()) -> zeros() , activate(n__take(X1, X2)) -> take(X1, X2) , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> nil() , take(s(M), cons(N, IL)) -> cons(N, n__take(M, activate(IL))) } Obligation: innermost runtime complexity Answer: MAYBE The weightgap principle applies (using the following constant growth matrix-interpretation) The following argument positions are usable: Uargs(cons) = {2}, Uargs(n__take) = {2}, Uargs(c_3) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, Uargs(length^#) = {1}, Uargs(c_7) = {1}, Uargs(c_11) = {1} TcT has computed following constructor-restricted matrix interpretation. [zeros] = [2] [cons](x1, x2) = [1] x2 + [0] [0] = [2] [n__zeros] = [1] [tt] = [1] [activate](x1) = [1] x1 + [2] [nil] = [1] [s](x1) = [1] x1 + [2] [take](x1, x2) = [1] x1 + [1] x2 + [2] [n__take](x1, x2) = [1] x1 + [1] x2 + [1] [zeros^#] = [2] [c_1] = [1] [c_2] = [1] [and^#](x1, x2) = [1] x1 + [2] x2 + [2] [c_3](x1) = [1] x1 + [1] [activate^#](x1) = [2] x1 + [2] [c_4] = [1] [c_5](x1) = [1] x1 + [1] [c_6](x1) = [1] x1 + [1] [take^#](x1, x2) = [1] x1 + [2] x2 + [2] [length^#](x1) = [2] x1 + [2] [c_7](x1) = [1] x1 + [1] [c_8] = [2] [c_9] = [1] [c_10] = [1] [c_11](x1) = [1] x1 + [1] This order satisfies following ordering constraints: [zeros()] = [2] > [1] = [cons(0(), n__zeros())] [zeros()] = [2] > [1] = [n__zeros()] [activate(X)] = [1] X + [2] > [1] X + [0] = [X] [activate(n__zeros())] = [3] > [2] = [zeros()] [activate(n__take(X1, X2))] = [1] X1 + [1] X2 + [3] > [1] X1 + [1] X2 + [2] = [take(X1, X2)] [take(X1, X2)] = [1] X1 + [1] X2 + [2] > [1] X1 + [1] X2 + [1] = [n__take(X1, X2)] [take(0(), IL)] = [1] IL + [4] > [1] = [nil()] [take(s(M), cons(N, IL))] = [1] IL + [1] M + [4] > [1] IL + [1] M + [3] = [cons(N, n__take(M, activate(IL)))] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { and^#(tt(), X) -> c_3(activate^#(X)) , length^#(cons(N, L)) -> c_7(length^#(activate(L))) } Weak DPs: { zeros^#() -> c_1() , zeros^#() -> c_2() , activate^#(X) -> c_4() , activate^#(n__zeros()) -> c_5(zeros^#()) , activate^#(n__take(X1, X2)) -> c_6(take^#(X1, X2)) , take^#(X1, X2) -> c_9() , take^#(0(), IL) -> c_10() , take^#(s(M), cons(N, IL)) -> c_11(activate^#(IL)) , length^#(nil()) -> c_8() } Weak Trs: { zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , activate(X) -> X , activate(n__zeros()) -> zeros() , activate(n__take(X1, X2)) -> take(X1, X2) , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> nil() , take(s(M), cons(N, IL)) -> cons(N, n__take(M, activate(IL))) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1} by applications of Pre({1}) = {}. Here rules are labeled as follows: DPs: { 1: and^#(tt(), X) -> c_3(activate^#(X)) , 2: length^#(cons(N, L)) -> c_7(length^#(activate(L))) , 3: zeros^#() -> c_1() , 4: zeros^#() -> c_2() , 5: activate^#(X) -> c_4() , 6: activate^#(n__zeros()) -> c_5(zeros^#()) , 7: activate^#(n__take(X1, X2)) -> c_6(take^#(X1, X2)) , 8: take^#(X1, X2) -> c_9() , 9: take^#(0(), IL) -> c_10() , 10: take^#(s(M), cons(N, IL)) -> c_11(activate^#(IL)) , 11: length^#(nil()) -> c_8() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { length^#(cons(N, L)) -> c_7(length^#(activate(L))) } Weak DPs: { zeros^#() -> c_1() , zeros^#() -> c_2() , and^#(tt(), X) -> c_3(activate^#(X)) , activate^#(X) -> c_4() , activate^#(n__zeros()) -> c_5(zeros^#()) , activate^#(n__take(X1, X2)) -> c_6(take^#(X1, X2)) , take^#(X1, X2) -> c_9() , take^#(0(), IL) -> c_10() , take^#(s(M), cons(N, IL)) -> c_11(activate^#(IL)) , length^#(nil()) -> c_8() } Weak Trs: { zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , activate(X) -> X , activate(n__zeros()) -> zeros() , activate(n__take(X1, X2)) -> take(X1, X2) , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> nil() , take(s(M), cons(N, IL)) -> cons(N, n__take(M, activate(IL))) } Obligation: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { zeros^#() -> c_1() , zeros^#() -> c_2() , and^#(tt(), X) -> c_3(activate^#(X)) , activate^#(X) -> c_4() , activate^#(n__zeros()) -> c_5(zeros^#()) , activate^#(n__take(X1, X2)) -> c_6(take^#(X1, X2)) , take^#(X1, X2) -> c_9() , take^#(0(), IL) -> c_10() , take^#(s(M), cons(N, IL)) -> c_11(activate^#(IL)) , length^#(nil()) -> c_8() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { length^#(cons(N, L)) -> c_7(length^#(activate(L))) } Weak Trs: { zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , activate(X) -> X , activate(n__zeros()) -> zeros() , activate(n__take(X1, X2)) -> take(X1, X2) , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> nil() , take(s(M), cons(N, IL)) -> cons(N, n__take(M, activate(IL))) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..