MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) activate(n__zeros()) -> zeros() and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) length(X) -> n__length(X) length(cons(N,L)) -> uLength(and(isNat(N),isNatList(activate(L))),activate(L)) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) take(0(),IL) -> uTake1(isNatIList(IL)) take(s(M),cons(N,IL)) -> uTake2(and(isNat(M),and(isNat(N),isNatIList(activate(IL)))),M,N,activate(IL)) uLength(tt(),L) -> s(length(activate(L))) uTake1(tt()) -> nil() uTake2(tt(),M,N,IL) -> cons(activate(N),n__take(activate(M),activate(IL))) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,and,cons,isNat,isNatIList,isNatList,length,nil ,s,take,uLength,uTake1,uTake2,zeros} and constructors {n__0,n__cons,n__length,n__nil,n__s,n__take,n__zeros ,tt} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. length(cons(N,L)) -> uLength(and(isNat(N),isNatList(activate(L))),activate(L)) take(0(),IL) -> uTake1(isNatIList(IL)) take(s(M),cons(N,IL)) -> uTake2(and(isNat(M),and(isNat(N),isNatIList(activate(IL)))),M,N,activate(IL)) All above mentioned rules can be savely removed. * Step 2: WeightGap MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) activate(n__zeros()) -> zeros() and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) uLength(tt(),L) -> s(length(activate(L))) uTake1(tt()) -> nil() uTake2(tt(),M,N,IL) -> cons(activate(N),n__take(activate(M),activate(IL))) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,and,cons,isNat,isNatIList,isNatList,length,nil ,s,take,uLength,uTake1,uTake2,zeros} and constructors {n__0,n__cons,n__length,n__nil,n__s,n__take,n__zeros ,tt} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(and) = {1,2}, uargs(cons) = {1,2}, uargs(isNat) = {1}, uargs(isNatIList) = {1}, uargs(isNatList) = {1}, uargs(length) = {1}, uargs(n__take) = {1,2}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(activate) = [1] x1 + [0] p(and) = [1] x1 + [1] x2 + [0] p(cons) = [1] x1 + [1] x2 + [0] p(isNat) = [1] x1 + [0] p(isNatIList) = [1] x1 + [0] p(isNatList) = [1] x1 + [0] p(length) = [1] x1 + [0] p(n__0) = [1] p(n__cons) = [1] x1 + [1] x2 + [0] p(n__length) = [1] x1 + [0] p(n__nil) = [0] p(n__s) = [1] x1 + [0] p(n__take) = [1] x1 + [1] x2 + [0] p(n__zeros) = [0] p(nil) = [0] p(s) = [1] x1 + [0] p(take) = [1] x1 + [1] x2 + [0] p(tt) = [0] p(uLength) = [1] x2 + [0] p(uTake1) = [0] p(uTake2) = [1] x2 + [1] x3 + [1] x4 + [0] p(zeros) = [1] Following rules are strictly oriented: activate(n__0()) = [1] > [0] = 0() isNat(n__0()) = [1] > [0] = tt() zeros() = [1] > [0] = cons(0(),n__zeros()) zeros() = [1] > [0] = n__zeros() Following rules are (at-least) weakly oriented: 0() = [0] >= [1] = n__0() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n__cons(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = cons(X1,X2) activate(n__length(X)) = [1] X + [0] >= [1] X + [0] = length(X) activate(n__nil()) = [0] >= [0] = nil() activate(n__s(X)) = [1] X + [0] >= [1] X + [0] = s(X) activate(n__take(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = take(X1,X2) activate(n__zeros()) = [0] >= [1] = zeros() and(tt(),T) = [1] T + [0] >= [1] T + [0] = T cons(X1,X2) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = n__cons(X1,X2) isNat(n__length(L)) = [1] L + [0] >= [1] L + [0] = isNatList(activate(L)) isNat(n__s(N)) = [1] N + [0] >= [1] N + [0] = isNat(activate(N)) isNatIList(IL) = [1] IL + [0] >= [1] IL + [0] = isNatList(activate(IL)) isNatIList(n__cons(N,IL)) = [1] IL + [1] N + [0] >= [1] IL + [1] N + [0] = and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) = [0] >= [0] = tt() isNatList(n__cons(N,L)) = [1] L + [1] N + [0] >= [1] L + [1] N + [0] = and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) = [0] >= [0] = tt() isNatList(n__take(N,IL)) = [1] IL + [1] N + [0] >= [1] IL + [1] N + [0] = and(isNat(activate(N)),isNatIList(activate(IL))) length(X) = [1] X + [0] >= [1] X + [0] = n__length(X) nil() = [0] >= [0] = n__nil() s(X) = [1] X + [0] >= [1] X + [0] = n__s(X) take(X1,X2) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = n__take(X1,X2) uLength(tt(),L) = [1] L + [0] >= [1] L + [0] = s(length(activate(L))) uTake1(tt()) = [0] >= [0] = nil() uTake2(tt(),M,N,IL) = [1] IL + [1] M + [1] N + [0] >= [1] IL + [1] M + [1] N + [0] = cons(activate(N),n__take(activate(M),activate(IL))) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 3: WeightGap MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) activate(n__zeros()) -> zeros() and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) uLength(tt(),L) -> s(length(activate(L))) uTake1(tt()) -> nil() uTake2(tt(),M,N,IL) -> cons(activate(N),n__take(activate(M),activate(IL))) - Weak TRS: activate(n__0()) -> 0() isNat(n__0()) -> tt() zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,and,cons,isNat,isNatIList,isNatList,length,nil ,s,take,uLength,uTake1,uTake2,zeros} and constructors {n__0,n__cons,n__length,n__nil,n__s,n__take,n__zeros ,tt} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(and) = {1,2}, uargs(cons) = {1,2}, uargs(isNat) = {1}, uargs(isNatIList) = {1}, uargs(isNatList) = {1}, uargs(length) = {1}, uargs(n__take) = {1,2}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [1] p(activate) = [1] x1 + [0] p(and) = [1] x1 + [1] x2 + [0] p(cons) = [1] x1 + [1] x2 + [1] p(isNat) = [1] x1 + [1] p(isNatIList) = [1] x1 + [0] p(isNatList) = [1] x1 + [0] p(length) = [1] x1 + [0] p(n__0) = [1] p(n__cons) = [1] x1 + [1] x2 + [0] p(n__length) = [1] x1 + [0] p(n__nil) = [0] p(n__s) = [1] x1 + [7] p(n__take) = [1] x1 + [1] x2 + [0] p(n__zeros) = [4] p(nil) = [0] p(s) = [1] x1 + [0] p(take) = [1] x1 + [1] x2 + [0] p(tt) = [2] p(uLength) = [1] x2 + [0] p(uTake1) = [0] p(uTake2) = [1] x2 + [1] x3 + [1] x4 + [2] p(zeros) = [7] Following rules are strictly oriented: activate(n__s(X)) = [1] X + [7] > [1] X + [0] = s(X) and(tt(),T) = [1] T + [2] > [1] T + [0] = T cons(X1,X2) = [1] X1 + [1] X2 + [1] > [1] X1 + [1] X2 + [0] = n__cons(X1,X2) isNat(n__length(L)) = [1] L + [1] > [1] L + [0] = isNatList(activate(L)) isNat(n__s(N)) = [1] N + [8] > [1] N + [1] = isNat(activate(N)) isNatIList(n__zeros()) = [4] > [2] = tt() uTake2(tt(),M,N,IL) = [1] IL + [1] M + [1] N + [2] > [1] IL + [1] M + [1] N + [1] = cons(activate(N),n__take(activate(M),activate(IL))) Following rules are (at-least) weakly oriented: 0() = [1] >= [1] = n__0() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n__0()) = [1] >= [1] = 0() activate(n__cons(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [1] = cons(X1,X2) activate(n__length(X)) = [1] X + [0] >= [1] X + [0] = length(X) activate(n__nil()) = [0] >= [0] = nil() activate(n__take(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = take(X1,X2) activate(n__zeros()) = [4] >= [7] = zeros() isNat(n__0()) = [2] >= [2] = tt() isNatIList(IL) = [1] IL + [0] >= [1] IL + [0] = isNatList(activate(IL)) isNatIList(n__cons(N,IL)) = [1] IL + [1] N + [0] >= [1] IL + [1] N + [1] = and(isNat(activate(N)),isNatIList(activate(IL))) isNatList(n__cons(N,L)) = [1] L + [1] N + [0] >= [1] L + [1] N + [1] = and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) = [0] >= [2] = tt() isNatList(n__take(N,IL)) = [1] IL + [1] N + [0] >= [1] IL + [1] N + [1] = and(isNat(activate(N)),isNatIList(activate(IL))) length(X) = [1] X + [0] >= [1] X + [0] = n__length(X) nil() = [0] >= [0] = n__nil() s(X) = [1] X + [0] >= [1] X + [7] = n__s(X) take(X1,X2) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = n__take(X1,X2) uLength(tt(),L) = [1] L + [0] >= [1] L + [0] = s(length(activate(L))) uTake1(tt()) = [0] >= [0] = nil() zeros() = [7] >= [6] = cons(0(),n__zeros()) zeros() = [7] >= [4] = n__zeros() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: WeightGap MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__take(X1,X2)) -> take(X1,X2) activate(n__zeros()) -> zeros() isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) uLength(tt(),L) -> s(length(activate(L))) uTake1(tt()) -> nil() - Weak TRS: activate(n__0()) -> 0() activate(n__s(X)) -> s(X) and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(n__zeros()) -> tt() uTake2(tt(),M,N,IL) -> cons(activate(N),n__take(activate(M),activate(IL))) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,and,cons,isNat,isNatIList,isNatList,length,nil ,s,take,uLength,uTake1,uTake2,zeros} and constructors {n__0,n__cons,n__length,n__nil,n__s,n__take,n__zeros ,tt} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(and) = {1,2}, uargs(cons) = {1,2}, uargs(isNat) = {1}, uargs(isNatIList) = {1}, uargs(isNatList) = {1}, uargs(length) = {1}, uargs(n__take) = {1,2}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(activate) = [1] x1 + [0] p(and) = [1] x1 + [1] x2 + [5] p(cons) = [1] x1 + [1] x2 + [4] p(isNat) = [1] x1 + [4] p(isNatIList) = [1] x1 + [4] p(isNatList) = [1] x1 + [4] p(length) = [1] x1 + [0] p(n__0) = [0] p(n__cons) = [1] x1 + [1] x2 + [4] p(n__length) = [1] x1 + [0] p(n__nil) = [0] p(n__s) = [1] x1 + [0] p(n__take) = [1] x1 + [1] x2 + [0] p(n__zeros) = [0] p(nil) = [0] p(s) = [1] x1 + [0] p(take) = [1] x1 + [1] x2 + [0] p(tt) = [4] p(uLength) = [1] x2 + [0] p(uTake1) = [1] p(uTake2) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0] p(zeros) = [4] Following rules are strictly oriented: uTake1(tt()) = [1] > [0] = nil() Following rules are (at-least) weakly oriented: 0() = [0] >= [0] = n__0() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n__0()) = [0] >= [0] = 0() activate(n__cons(X1,X2)) = [1] X1 + [1] X2 + [4] >= [1] X1 + [1] X2 + [4] = cons(X1,X2) activate(n__length(X)) = [1] X + [0] >= [1] X + [0] = length(X) activate(n__nil()) = [0] >= [0] = nil() activate(n__s(X)) = [1] X + [0] >= [1] X + [0] = s(X) activate(n__take(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = take(X1,X2) activate(n__zeros()) = [0] >= [4] = zeros() and(tt(),T) = [1] T + [9] >= [1] T + [0] = T cons(X1,X2) = [1] X1 + [1] X2 + [4] >= [1] X1 + [1] X2 + [4] = n__cons(X1,X2) isNat(n__0()) = [4] >= [4] = tt() isNat(n__length(L)) = [1] L + [4] >= [1] L + [4] = isNatList(activate(L)) isNat(n__s(N)) = [1] N + [4] >= [1] N + [4] = isNat(activate(N)) isNatIList(IL) = [1] IL + [4] >= [1] IL + [4] = isNatList(activate(IL)) isNatIList(n__cons(N,IL)) = [1] IL + [1] N + [8] >= [1] IL + [1] N + [13] = and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) = [4] >= [4] = tt() isNatList(n__cons(N,L)) = [1] L + [1] N + [8] >= [1] L + [1] N + [13] = and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) = [4] >= [4] = tt() isNatList(n__take(N,IL)) = [1] IL + [1] N + [4] >= [1] IL + [1] N + [13] = and(isNat(activate(N)),isNatIList(activate(IL))) length(X) = [1] X + [0] >= [1] X + [0] = n__length(X) nil() = [0] >= [0] = n__nil() s(X) = [1] X + [0] >= [1] X + [0] = n__s(X) take(X1,X2) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = n__take(X1,X2) uLength(tt(),L) = [1] L + [0] >= [1] L + [0] = s(length(activate(L))) uTake2(tt(),M,N,IL) = [1] IL + [1] M + [1] N + [4] >= [1] IL + [1] M + [1] N + [4] = cons(activate(N),n__take(activate(M),activate(IL))) zeros() = [4] >= [4] = cons(0(),n__zeros()) zeros() = [4] >= [0] = n__zeros() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 5: WeightGap MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__take(X1,X2)) -> take(X1,X2) activate(n__zeros()) -> zeros() isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) uLength(tt(),L) -> s(length(activate(L))) - Weak TRS: activate(n__0()) -> 0() activate(n__s(X)) -> s(X) and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(n__zeros()) -> tt() uTake1(tt()) -> nil() uTake2(tt(),M,N,IL) -> cons(activate(N),n__take(activate(M),activate(IL))) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,and,cons,isNat,isNatIList,isNatList,length,nil ,s,take,uLength,uTake1,uTake2,zeros} and constructors {n__0,n__cons,n__length,n__nil,n__s,n__take,n__zeros ,tt} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(and) = {1,2}, uargs(cons) = {1,2}, uargs(isNat) = {1}, uargs(isNatIList) = {1}, uargs(isNatList) = {1}, uargs(length) = {1}, uargs(n__take) = {1,2}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(activate) = [1] x1 + [0] p(and) = [1] x1 + [1] x2 + [0] p(cons) = [1] x1 + [1] x2 + [0] p(isNat) = [1] x1 + [0] p(isNatIList) = [1] x1 + [0] p(isNatList) = [1] x1 + [0] p(length) = [1] x1 + [0] p(n__0) = [0] p(n__cons) = [1] x1 + [1] x2 + [0] p(n__length) = [1] x1 + [0] p(n__nil) = [0] p(n__s) = [1] x1 + [0] p(n__take) = [1] x1 + [1] x2 + [0] p(n__zeros) = [0] p(nil) = [0] p(s) = [1] x1 + [0] p(take) = [1] x1 + [1] x2 + [0] p(tt) = [0] p(uLength) = [1] x2 + [1] p(uTake1) = [0] p(uTake2) = [1] x2 + [1] x3 + [1] x4 + [0] p(zeros) = [0] Following rules are strictly oriented: uLength(tt(),L) = [1] L + [1] > [1] L + [0] = s(length(activate(L))) Following rules are (at-least) weakly oriented: 0() = [0] >= [0] = n__0() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n__0()) = [0] >= [0] = 0() activate(n__cons(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = cons(X1,X2) activate(n__length(X)) = [1] X + [0] >= [1] X + [0] = length(X) activate(n__nil()) = [0] >= [0] = nil() activate(n__s(X)) = [1] X + [0] >= [1] X + [0] = s(X) activate(n__take(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = take(X1,X2) activate(n__zeros()) = [0] >= [0] = zeros() and(tt(),T) = [1] T + [0] >= [1] T + [0] = T cons(X1,X2) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = n__cons(X1,X2) isNat(n__0()) = [0] >= [0] = tt() isNat(n__length(L)) = [1] L + [0] >= [1] L + [0] = isNatList(activate(L)) isNat(n__s(N)) = [1] N + [0] >= [1] N + [0] = isNat(activate(N)) isNatIList(IL) = [1] IL + [0] >= [1] IL + [0] = isNatList(activate(IL)) isNatIList(n__cons(N,IL)) = [1] IL + [1] N + [0] >= [1] IL + [1] N + [0] = and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) = [0] >= [0] = tt() isNatList(n__cons(N,L)) = [1] L + [1] N + [0] >= [1] L + [1] N + [0] = and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) = [0] >= [0] = tt() isNatList(n__take(N,IL)) = [1] IL + [1] N + [0] >= [1] IL + [1] N + [0] = and(isNat(activate(N)),isNatIList(activate(IL))) length(X) = [1] X + [0] >= [1] X + [0] = n__length(X) nil() = [0] >= [0] = n__nil() s(X) = [1] X + [0] >= [1] X + [0] = n__s(X) take(X1,X2) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = n__take(X1,X2) uTake1(tt()) = [0] >= [0] = nil() uTake2(tt(),M,N,IL) = [1] IL + [1] M + [1] N + [0] >= [1] IL + [1] M + [1] N + [0] = cons(activate(N),n__take(activate(M),activate(IL))) zeros() = [0] >= [0] = cons(0(),n__zeros()) zeros() = [0] >= [0] = n__zeros() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 6: WeightGap MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__take(X1,X2)) -> take(X1,X2) activate(n__zeros()) -> zeros() isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) - Weak TRS: activate(n__0()) -> 0() activate(n__s(X)) -> s(X) and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(n__zeros()) -> tt() uLength(tt(),L) -> s(length(activate(L))) uTake1(tt()) -> nil() uTake2(tt(),M,N,IL) -> cons(activate(N),n__take(activate(M),activate(IL))) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,and,cons,isNat,isNatIList,isNatList,length,nil ,s,take,uLength,uTake1,uTake2,zeros} and constructors {n__0,n__cons,n__length,n__nil,n__s,n__take,n__zeros ,tt} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(and) = {1,2}, uargs(cons) = {1,2}, uargs(isNat) = {1}, uargs(isNatIList) = {1}, uargs(isNatList) = {1}, uargs(length) = {1}, uargs(n__take) = {1,2}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [4] p(activate) = [1] x1 + [0] p(and) = [1] x1 + [1] x2 + [0] p(cons) = [1] x1 + [1] x2 + [0] p(isNat) = [1] x1 + [4] p(isNatIList) = [1] x1 + [0] p(isNatList) = [1] x1 + [4] p(length) = [1] x1 + [0] p(n__0) = [4] p(n__cons) = [1] x1 + [1] x2 + [0] p(n__length) = [1] x1 + [0] p(n__nil) = [0] p(n__s) = [1] x1 + [3] p(n__take) = [1] x1 + [1] x2 + [7] p(n__zeros) = [0] p(nil) = [0] p(s) = [1] x1 + [3] p(take) = [1] x1 + [1] x2 + [0] p(tt) = [0] p(uLength) = [1] x2 + [3] p(uTake1) = [1] x1 + [0] p(uTake2) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [7] p(zeros) = [6] Following rules are strictly oriented: activate(n__take(X1,X2)) = [1] X1 + [1] X2 + [7] > [1] X1 + [1] X2 + [0] = take(X1,X2) isNatList(n__nil()) = [4] > [0] = tt() isNatList(n__take(N,IL)) = [1] IL + [1] N + [11] > [1] IL + [1] N + [4] = and(isNat(activate(N)),isNatIList(activate(IL))) Following rules are (at-least) weakly oriented: 0() = [4] >= [4] = n__0() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n__0()) = [4] >= [4] = 0() activate(n__cons(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = cons(X1,X2) activate(n__length(X)) = [1] X + [0] >= [1] X + [0] = length(X) activate(n__nil()) = [0] >= [0] = nil() activate(n__s(X)) = [1] X + [3] >= [1] X + [3] = s(X) activate(n__zeros()) = [0] >= [6] = zeros() and(tt(),T) = [1] T + [0] >= [1] T + [0] = T cons(X1,X2) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = n__cons(X1,X2) isNat(n__0()) = [8] >= [0] = tt() isNat(n__length(L)) = [1] L + [4] >= [1] L + [4] = isNatList(activate(L)) isNat(n__s(N)) = [1] N + [7] >= [1] N + [4] = isNat(activate(N)) isNatIList(IL) = [1] IL + [0] >= [1] IL + [4] = isNatList(activate(IL)) isNatIList(n__cons(N,IL)) = [1] IL + [1] N + [0] >= [1] IL + [1] N + [4] = and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) = [0] >= [0] = tt() isNatList(n__cons(N,L)) = [1] L + [1] N + [4] >= [1] L + [1] N + [8] = and(isNat(activate(N)),isNatList(activate(L))) length(X) = [1] X + [0] >= [1] X + [0] = n__length(X) nil() = [0] >= [0] = n__nil() s(X) = [1] X + [3] >= [1] X + [3] = n__s(X) take(X1,X2) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [7] = n__take(X1,X2) uLength(tt(),L) = [1] L + [3] >= [1] L + [3] = s(length(activate(L))) uTake1(tt()) = [0] >= [0] = nil() uTake2(tt(),M,N,IL) = [1] IL + [1] M + [1] N + [7] >= [1] IL + [1] M + [1] N + [7] = cons(activate(N),n__take(activate(M),activate(IL))) zeros() = [6] >= [4] = cons(0(),n__zeros()) zeros() = [6] >= [0] = n__zeros() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 7: WeightGap MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__zeros()) -> zeros() isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) - Weak TRS: activate(n__0()) -> 0() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(n__zeros()) -> tt() isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) uLength(tt(),L) -> s(length(activate(L))) uTake1(tt()) -> nil() uTake2(tt(),M,N,IL) -> cons(activate(N),n__take(activate(M),activate(IL))) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,and,cons,isNat,isNatIList,isNatList,length,nil ,s,take,uLength,uTake1,uTake2,zeros} and constructors {n__0,n__cons,n__length,n__nil,n__s,n__take,n__zeros ,tt} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(and) = {1,2}, uargs(cons) = {1,2}, uargs(isNat) = {1}, uargs(isNatIList) = {1}, uargs(isNatList) = {1}, uargs(length) = {1}, uargs(n__take) = {1,2}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(activate) = [1] x1 + [0] p(and) = [1] x1 + [1] x2 + [1] p(cons) = [1] x1 + [1] x2 + [0] p(isNat) = [1] x1 + [0] p(isNatIList) = [1] x1 + [1] p(isNatList) = [1] x1 + [0] p(length) = [1] x1 + [0] p(n__0) = [1] p(n__cons) = [1] x1 + [1] x2 + [0] p(n__length) = [1] x1 + [0] p(n__nil) = [2] p(n__s) = [1] x1 + [0] p(n__take) = [1] x1 + [1] x2 + [2] p(n__zeros) = [0] p(nil) = [0] p(s) = [1] x1 + [0] p(take) = [1] x1 + [1] x2 + [2] p(tt) = [1] p(uLength) = [1] x2 + [2] p(uTake1) = [0] p(uTake2) = [5] x1 + [1] x2 + [1] x3 + [1] x4 + [0] p(zeros) = [0] Following rules are strictly oriented: activate(n__nil()) = [2] > [0] = nil() isNatIList(IL) = [1] IL + [1] > [1] IL + [0] = isNatList(activate(IL)) Following rules are (at-least) weakly oriented: 0() = [0] >= [1] = n__0() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n__0()) = [1] >= [0] = 0() activate(n__cons(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = cons(X1,X2) activate(n__length(X)) = [1] X + [0] >= [1] X + [0] = length(X) activate(n__s(X)) = [1] X + [0] >= [1] X + [0] = s(X) activate(n__take(X1,X2)) = [1] X1 + [1] X2 + [2] >= [1] X1 + [1] X2 + [2] = take(X1,X2) activate(n__zeros()) = [0] >= [0] = zeros() and(tt(),T) = [1] T + [2] >= [1] T + [0] = T cons(X1,X2) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = n__cons(X1,X2) isNat(n__0()) = [1] >= [1] = tt() isNat(n__length(L)) = [1] L + [0] >= [1] L + [0] = isNatList(activate(L)) isNat(n__s(N)) = [1] N + [0] >= [1] N + [0] = isNat(activate(N)) isNatIList(n__cons(N,IL)) = [1] IL + [1] N + [1] >= [1] IL + [1] N + [2] = and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) = [1] >= [1] = tt() isNatList(n__cons(N,L)) = [1] L + [1] N + [0] >= [1] L + [1] N + [1] = and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) = [2] >= [1] = tt() isNatList(n__take(N,IL)) = [1] IL + [1] N + [2] >= [1] IL + [1] N + [2] = and(isNat(activate(N)),isNatIList(activate(IL))) length(X) = [1] X + [0] >= [1] X + [0] = n__length(X) nil() = [0] >= [2] = n__nil() s(X) = [1] X + [0] >= [1] X + [0] = n__s(X) take(X1,X2) = [1] X1 + [1] X2 + [2] >= [1] X1 + [1] X2 + [2] = n__take(X1,X2) uLength(tt(),L) = [1] L + [2] >= [1] L + [0] = s(length(activate(L))) uTake1(tt()) = [0] >= [0] = nil() uTake2(tt(),M,N,IL) = [1] IL + [1] M + [1] N + [5] >= [1] IL + [1] M + [1] N + [2] = cons(activate(N),n__take(activate(M),activate(IL))) zeros() = [0] >= [0] = cons(0(),n__zeros()) zeros() = [0] >= [0] = n__zeros() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 8: WeightGap MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__length(X)) -> length(X) activate(n__zeros()) -> zeros() isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) - Weak TRS: activate(n__0()) -> 0() activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__zeros()) -> tt() isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) uLength(tt(),L) -> s(length(activate(L))) uTake1(tt()) -> nil() uTake2(tt(),M,N,IL) -> cons(activate(N),n__take(activate(M),activate(IL))) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,and,cons,isNat,isNatIList,isNatList,length,nil ,s,take,uLength,uTake1,uTake2,zeros} and constructors {n__0,n__cons,n__length,n__nil,n__s,n__take,n__zeros ,tt} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(and) = {1,2}, uargs(cons) = {1,2}, uargs(isNat) = {1}, uargs(isNatIList) = {1}, uargs(isNatList) = {1}, uargs(length) = {1}, uargs(n__take) = {1,2}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [2] p(activate) = [1] x1 + [0] p(and) = [1] x1 + [1] x2 + [0] p(cons) = [1] x1 + [1] x2 + [0] p(isNat) = [1] x1 + [0] p(isNatIList) = [1] x1 + [0] p(isNatList) = [1] x1 + [0] p(length) = [1] x1 + [2] p(n__0) = [2] p(n__cons) = [1] x1 + [1] x2 + [0] p(n__length) = [1] x1 + [1] p(n__nil) = [1] p(n__s) = [1] x1 + [5] p(n__take) = [1] x1 + [1] x2 + [0] p(n__zeros) = [0] p(nil) = [1] p(s) = [1] x1 + [0] p(take) = [1] x1 + [1] x2 + [0] p(tt) = [0] p(uLength) = [4] x2 + [4] p(uTake1) = [4] p(uTake2) = [4] x1 + [4] x2 + [4] x3 + [5] x4 + [7] p(zeros) = [2] Following rules are strictly oriented: length(X) = [1] X + [2] > [1] X + [1] = n__length(X) Following rules are (at-least) weakly oriented: 0() = [2] >= [2] = n__0() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n__0()) = [2] >= [2] = 0() activate(n__cons(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = cons(X1,X2) activate(n__length(X)) = [1] X + [1] >= [1] X + [2] = length(X) activate(n__nil()) = [1] >= [1] = nil() activate(n__s(X)) = [1] X + [5] >= [1] X + [0] = s(X) activate(n__take(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = take(X1,X2) activate(n__zeros()) = [0] >= [2] = zeros() and(tt(),T) = [1] T + [0] >= [1] T + [0] = T cons(X1,X2) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = n__cons(X1,X2) isNat(n__0()) = [2] >= [0] = tt() isNat(n__length(L)) = [1] L + [1] >= [1] L + [0] = isNatList(activate(L)) isNat(n__s(N)) = [1] N + [5] >= [1] N + [0] = isNat(activate(N)) isNatIList(IL) = [1] IL + [0] >= [1] IL + [0] = isNatList(activate(IL)) isNatIList(n__cons(N,IL)) = [1] IL + [1] N + [0] >= [1] IL + [1] N + [0] = and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) = [0] >= [0] = tt() isNatList(n__cons(N,L)) = [1] L + [1] N + [0] >= [1] L + [1] N + [0] = and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) = [1] >= [0] = tt() isNatList(n__take(N,IL)) = [1] IL + [1] N + [0] >= [1] IL + [1] N + [0] = and(isNat(activate(N)),isNatIList(activate(IL))) nil() = [1] >= [1] = n__nil() s(X) = [1] X + [0] >= [1] X + [5] = n__s(X) take(X1,X2) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = n__take(X1,X2) uLength(tt(),L) = [4] L + [4] >= [1] L + [2] = s(length(activate(L))) uTake1(tt()) = [4] >= [1] = nil() uTake2(tt(),M,N,IL) = [5] IL + [4] M + [4] N + [7] >= [1] IL + [1] M + [1] N + [0] = cons(activate(N),n__take(activate(M),activate(IL))) zeros() = [2] >= [2] = cons(0(),n__zeros()) zeros() = [2] >= [0] = n__zeros() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 9: WeightGap MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__length(X)) -> length(X) activate(n__zeros()) -> zeros() isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) - Weak TRS: activate(n__0()) -> 0() activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__zeros()) -> tt() isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) length(X) -> n__length(X) uLength(tt(),L) -> s(length(activate(L))) uTake1(tt()) -> nil() uTake2(tt(),M,N,IL) -> cons(activate(N),n__take(activate(M),activate(IL))) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,and,cons,isNat,isNatIList,isNatList,length,nil ,s,take,uLength,uTake1,uTake2,zeros} and constructors {n__0,n__cons,n__length,n__nil,n__s,n__take,n__zeros ,tt} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(and) = {1,2}, uargs(cons) = {1,2}, uargs(isNat) = {1}, uargs(isNatIList) = {1}, uargs(isNatList) = {1}, uargs(length) = {1}, uargs(n__take) = {1,2}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(activate) = [1] x1 + [0] p(and) = [1] x1 + [1] x2 + [0] p(cons) = [1] x1 + [1] x2 + [5] p(isNat) = [1] x1 + [0] p(isNatIList) = [1] x1 + [0] p(isNatList) = [1] x1 + [0] p(length) = [1] x1 + [1] p(n__0) = [4] p(n__cons) = [1] x1 + [1] x2 + [5] p(n__length) = [1] x1 + [0] p(n__nil) = [0] p(n__s) = [1] x1 + [1] p(n__take) = [1] x1 + [1] x2 + [0] p(n__zeros) = [2] p(nil) = [0] p(s) = [1] x1 + [0] p(take) = [1] x1 + [1] x2 + [0] p(tt) = [0] p(uLength) = [2] x2 + [4] p(uTake1) = [0] p(uTake2) = [1] x2 + [2] x3 + [1] x4 + [6] p(zeros) = [7] Following rules are strictly oriented: isNatIList(n__cons(N,IL)) = [1] IL + [1] N + [5] > [1] IL + [1] N + [0] = and(isNat(activate(N)),isNatIList(activate(IL))) isNatList(n__cons(N,L)) = [1] L + [1] N + [5] > [1] L + [1] N + [0] = and(isNat(activate(N)),isNatList(activate(L))) Following rules are (at-least) weakly oriented: 0() = [0] >= [4] = n__0() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n__0()) = [4] >= [0] = 0() activate(n__cons(X1,X2)) = [1] X1 + [1] X2 + [5] >= [1] X1 + [1] X2 + [5] = cons(X1,X2) activate(n__length(X)) = [1] X + [0] >= [1] X + [1] = length(X) activate(n__nil()) = [0] >= [0] = nil() activate(n__s(X)) = [1] X + [1] >= [1] X + [0] = s(X) activate(n__take(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = take(X1,X2) activate(n__zeros()) = [2] >= [7] = zeros() and(tt(),T) = [1] T + [0] >= [1] T + [0] = T cons(X1,X2) = [1] X1 + [1] X2 + [5] >= [1] X1 + [1] X2 + [5] = n__cons(X1,X2) isNat(n__0()) = [4] >= [0] = tt() isNat(n__length(L)) = [1] L + [0] >= [1] L + [0] = isNatList(activate(L)) isNat(n__s(N)) = [1] N + [1] >= [1] N + [0] = isNat(activate(N)) isNatIList(IL) = [1] IL + [0] >= [1] IL + [0] = isNatList(activate(IL)) isNatIList(n__zeros()) = [2] >= [0] = tt() isNatList(n__nil()) = [0] >= [0] = tt() isNatList(n__take(N,IL)) = [1] IL + [1] N + [0] >= [1] IL + [1] N + [0] = and(isNat(activate(N)),isNatIList(activate(IL))) length(X) = [1] X + [1] >= [1] X + [0] = n__length(X) nil() = [0] >= [0] = n__nil() s(X) = [1] X + [0] >= [1] X + [1] = n__s(X) take(X1,X2) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = n__take(X1,X2) uLength(tt(),L) = [2] L + [4] >= [1] L + [1] = s(length(activate(L))) uTake1(tt()) = [0] >= [0] = nil() uTake2(tt(),M,N,IL) = [1] IL + [1] M + [2] N + [6] >= [1] IL + [1] M + [1] N + [5] = cons(activate(N),n__take(activate(M),activate(IL))) zeros() = [7] >= [7] = cons(0(),n__zeros()) zeros() = [7] >= [2] = n__zeros() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 10: WeightGap MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__length(X)) -> length(X) activate(n__zeros()) -> zeros() nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) - Weak TRS: activate(n__0()) -> 0() activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) length(X) -> n__length(X) uLength(tt(),L) -> s(length(activate(L))) uTake1(tt()) -> nil() uTake2(tt(),M,N,IL) -> cons(activate(N),n__take(activate(M),activate(IL))) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,and,cons,isNat,isNatIList,isNatList,length,nil ,s,take,uLength,uTake1,uTake2,zeros} and constructors {n__0,n__cons,n__length,n__nil,n__s,n__take,n__zeros ,tt} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(and) = {1,2}, uargs(cons) = {1,2}, uargs(isNat) = {1}, uargs(isNatIList) = {1}, uargs(isNatList) = {1}, uargs(length) = {1}, uargs(n__take) = {1,2}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [2] p(activate) = [1] x1 + [1] p(and) = [1] x1 + [1] x2 + [0] p(cons) = [1] x1 + [1] x2 + [2] p(isNat) = [1] x1 + [0] p(isNatIList) = [1] x1 + [1] p(isNatList) = [1] x1 + [0] p(length) = [1] x1 + [2] p(n__0) = [4] p(n__cons) = [1] x1 + [1] x2 + [2] p(n__length) = [1] x1 + [2] p(n__nil) = [4] p(n__s) = [1] x1 + [4] p(n__take) = [1] x1 + [1] x2 + [4] p(n__zeros) = [3] p(nil) = [5] p(s) = [1] x1 + [0] p(take) = [1] x1 + [1] x2 + [5] p(tt) = [4] p(uLength) = [5] x2 + [3] p(uTake1) = [2] x1 + [0] p(uTake2) = [2] x1 + [4] x2 + [1] x3 + [2] x4 + [1] p(zeros) = [7] Following rules are strictly oriented: activate(X) = [1] X + [1] > [1] X + [0] = X activate(n__cons(X1,X2)) = [1] X1 + [1] X2 + [3] > [1] X1 + [1] X2 + [2] = cons(X1,X2) activate(n__length(X)) = [1] X + [3] > [1] X + [2] = length(X) nil() = [5] > [4] = n__nil() take(X1,X2) = [1] X1 + [1] X2 + [5] > [1] X1 + [1] X2 + [4] = n__take(X1,X2) Following rules are (at-least) weakly oriented: 0() = [2] >= [4] = n__0() activate(n__0()) = [5] >= [2] = 0() activate(n__nil()) = [5] >= [5] = nil() activate(n__s(X)) = [1] X + [5] >= [1] X + [0] = s(X) activate(n__take(X1,X2)) = [1] X1 + [1] X2 + [5] >= [1] X1 + [1] X2 + [5] = take(X1,X2) activate(n__zeros()) = [4] >= [7] = zeros() and(tt(),T) = [1] T + [4] >= [1] T + [0] = T cons(X1,X2) = [1] X1 + [1] X2 + [2] >= [1] X1 + [1] X2 + [2] = n__cons(X1,X2) isNat(n__0()) = [4] >= [4] = tt() isNat(n__length(L)) = [1] L + [2] >= [1] L + [1] = isNatList(activate(L)) isNat(n__s(N)) = [1] N + [4] >= [1] N + [1] = isNat(activate(N)) isNatIList(IL) = [1] IL + [1] >= [1] IL + [1] = isNatList(activate(IL)) isNatIList(n__cons(N,IL)) = [1] IL + [1] N + [3] >= [1] IL + [1] N + [3] = and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) = [4] >= [4] = tt() isNatList(n__cons(N,L)) = [1] L + [1] N + [2] >= [1] L + [1] N + [2] = and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) = [4] >= [4] = tt() isNatList(n__take(N,IL)) = [1] IL + [1] N + [4] >= [1] IL + [1] N + [3] = and(isNat(activate(N)),isNatIList(activate(IL))) length(X) = [1] X + [2] >= [1] X + [2] = n__length(X) s(X) = [1] X + [0] >= [1] X + [4] = n__s(X) uLength(tt(),L) = [5] L + [3] >= [1] L + [3] = s(length(activate(L))) uTake1(tt()) = [8] >= [5] = nil() uTake2(tt(),M,N,IL) = [2] IL + [4] M + [1] N + [9] >= [1] IL + [1] M + [1] N + [9] = cons(activate(N),n__take(activate(M),activate(IL))) zeros() = [7] >= [7] = cons(0(),n__zeros()) zeros() = [7] >= [3] = n__zeros() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 11: WeightGap MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() activate(n__zeros()) -> zeros() s(X) -> n__s(X) - Weak TRS: activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) length(X) -> n__length(X) nil() -> n__nil() take(X1,X2) -> n__take(X1,X2) uLength(tt(),L) -> s(length(activate(L))) uTake1(tt()) -> nil() uTake2(tt(),M,N,IL) -> cons(activate(N),n__take(activate(M),activate(IL))) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,and,cons,isNat,isNatIList,isNatList,length,nil ,s,take,uLength,uTake1,uTake2,zeros} and constructors {n__0,n__cons,n__length,n__nil,n__s,n__take,n__zeros ,tt} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(and) = {1,2}, uargs(cons) = {1,2}, uargs(isNat) = {1}, uargs(isNatIList) = {1}, uargs(isNatList) = {1}, uargs(length) = {1}, uargs(n__take) = {1,2}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [1] p(activate) = [1] x1 + [1] p(and) = [1] x1 + [1] x2 + [0] p(cons) = [1] x1 + [1] x2 + [4] p(isNat) = [1] x1 + [0] p(isNatIList) = [1] x1 + [1] p(isNatList) = [1] x1 + [0] p(length) = [1] x1 + [1] p(n__0) = [3] p(n__cons) = [1] x1 + [1] x2 + [3] p(n__length) = [1] x1 + [1] p(n__nil) = [2] p(n__s) = [1] x1 + [1] p(n__take) = [1] x1 + [1] x2 + [3] p(n__zeros) = [1] p(nil) = [2] p(s) = [1] x1 + [2] p(take) = [1] x1 + [1] x2 + [3] p(tt) = [2] p(uLength) = [1] x2 + [4] p(uTake1) = [2] p(uTake2) = [4] x1 + [1] x2 + [1] x3 + [4] x4 + [4] p(zeros) = [7] Following rules are strictly oriented: s(X) = [1] X + [2] > [1] X + [1] = n__s(X) Following rules are (at-least) weakly oriented: 0() = [1] >= [3] = n__0() activate(X) = [1] X + [1] >= [1] X + [0] = X activate(n__0()) = [4] >= [1] = 0() activate(n__cons(X1,X2)) = [1] X1 + [1] X2 + [4] >= [1] X1 + [1] X2 + [4] = cons(X1,X2) activate(n__length(X)) = [1] X + [2] >= [1] X + [1] = length(X) activate(n__nil()) = [3] >= [2] = nil() activate(n__s(X)) = [1] X + [2] >= [1] X + [2] = s(X) activate(n__take(X1,X2)) = [1] X1 + [1] X2 + [4] >= [1] X1 + [1] X2 + [3] = take(X1,X2) activate(n__zeros()) = [2] >= [7] = zeros() and(tt(),T) = [1] T + [2] >= [1] T + [0] = T cons(X1,X2) = [1] X1 + [1] X2 + [4] >= [1] X1 + [1] X2 + [3] = n__cons(X1,X2) isNat(n__0()) = [3] >= [2] = tt() isNat(n__length(L)) = [1] L + [1] >= [1] L + [1] = isNatList(activate(L)) isNat(n__s(N)) = [1] N + [1] >= [1] N + [1] = isNat(activate(N)) isNatIList(IL) = [1] IL + [1] >= [1] IL + [1] = isNatList(activate(IL)) isNatIList(n__cons(N,IL)) = [1] IL + [1] N + [4] >= [1] IL + [1] N + [3] = and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) = [2] >= [2] = tt() isNatList(n__cons(N,L)) = [1] L + [1] N + [3] >= [1] L + [1] N + [2] = and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) = [2] >= [2] = tt() isNatList(n__take(N,IL)) = [1] IL + [1] N + [3] >= [1] IL + [1] N + [3] = and(isNat(activate(N)),isNatIList(activate(IL))) length(X) = [1] X + [1] >= [1] X + [1] = n__length(X) nil() = [2] >= [2] = n__nil() take(X1,X2) = [1] X1 + [1] X2 + [3] >= [1] X1 + [1] X2 + [3] = n__take(X1,X2) uLength(tt(),L) = [1] L + [4] >= [1] L + [4] = s(length(activate(L))) uTake1(tt()) = [2] >= [2] = nil() uTake2(tt(),M,N,IL) = [4] IL + [1] M + [1] N + [12] >= [1] IL + [1] M + [1] N + [10] = cons(activate(N),n__take(activate(M),activate(IL))) zeros() = [7] >= [6] = cons(0(),n__zeros()) zeros() = [7] >= [1] = n__zeros() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 12: WeightGap MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() activate(n__zeros()) -> zeros() - Weak TRS: activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) uLength(tt(),L) -> s(length(activate(L))) uTake1(tt()) -> nil() uTake2(tt(),M,N,IL) -> cons(activate(N),n__take(activate(M),activate(IL))) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,and,cons,isNat,isNatIList,isNatList,length,nil ,s,take,uLength,uTake1,uTake2,zeros} and constructors {n__0,n__cons,n__length,n__nil,n__s,n__take,n__zeros ,tt} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(and) = {1,2}, uargs(cons) = {1,2}, uargs(isNat) = {1}, uargs(isNatIList) = {1}, uargs(isNatList) = {1}, uargs(length) = {1}, uargs(n__take) = {1,2}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [1] p(activate) = [1] x1 + [1] p(and) = [1] x1 + [1] x2 + [0] p(cons) = [1] x1 + [1] x2 + [4] p(isNat) = [1] x1 + [1] p(isNatIList) = [1] x1 + [2] p(isNatList) = [1] x1 + [1] p(length) = [1] x1 + [7] p(n__0) = [0] p(n__cons) = [1] x1 + [1] x2 + [3] p(n__length) = [1] x1 + [7] p(n__nil) = [2] p(n__s) = [1] x1 + [3] p(n__take) = [1] x1 + [1] x2 + [4] p(n__zeros) = [0] p(nil) = [2] p(s) = [1] x1 + [3] p(take) = [1] x1 + [1] x2 + [4] p(tt) = [1] p(uLength) = [6] x1 + [2] x2 + [5] p(uTake1) = [5] x1 + [5] p(uTake2) = [4] x1 + [1] x2 + [5] x3 + [1] x4 + [7] p(zeros) = [5] Following rules are strictly oriented: 0() = [1] > [0] = n__0() Following rules are (at-least) weakly oriented: activate(X) = [1] X + [1] >= [1] X + [0] = X activate(n__0()) = [1] >= [1] = 0() activate(n__cons(X1,X2)) = [1] X1 + [1] X2 + [4] >= [1] X1 + [1] X2 + [4] = cons(X1,X2) activate(n__length(X)) = [1] X + [8] >= [1] X + [7] = length(X) activate(n__nil()) = [3] >= [2] = nil() activate(n__s(X)) = [1] X + [4] >= [1] X + [3] = s(X) activate(n__take(X1,X2)) = [1] X1 + [1] X2 + [5] >= [1] X1 + [1] X2 + [4] = take(X1,X2) activate(n__zeros()) = [1] >= [5] = zeros() and(tt(),T) = [1] T + [1] >= [1] T + [0] = T cons(X1,X2) = [1] X1 + [1] X2 + [4] >= [1] X1 + [1] X2 + [3] = n__cons(X1,X2) isNat(n__0()) = [1] >= [1] = tt() isNat(n__length(L)) = [1] L + [8] >= [1] L + [2] = isNatList(activate(L)) isNat(n__s(N)) = [1] N + [4] >= [1] N + [2] = isNat(activate(N)) isNatIList(IL) = [1] IL + [2] >= [1] IL + [2] = isNatList(activate(IL)) isNatIList(n__cons(N,IL)) = [1] IL + [1] N + [5] >= [1] IL + [1] N + [5] = and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) = [2] >= [1] = tt() isNatList(n__cons(N,L)) = [1] L + [1] N + [4] >= [1] L + [1] N + [4] = and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) = [3] >= [1] = tt() isNatList(n__take(N,IL)) = [1] IL + [1] N + [5] >= [1] IL + [1] N + [5] = and(isNat(activate(N)),isNatIList(activate(IL))) length(X) = [1] X + [7] >= [1] X + [7] = n__length(X) nil() = [2] >= [2] = n__nil() s(X) = [1] X + [3] >= [1] X + [3] = n__s(X) take(X1,X2) = [1] X1 + [1] X2 + [4] >= [1] X1 + [1] X2 + [4] = n__take(X1,X2) uLength(tt(),L) = [2] L + [11] >= [1] L + [11] = s(length(activate(L))) uTake1(tt()) = [10] >= [2] = nil() uTake2(tt(),M,N,IL) = [1] IL + [1] M + [5] N + [11] >= [1] IL + [1] M + [1] N + [11] = cons(activate(N),n__take(activate(M),activate(IL))) zeros() = [5] >= [5] = cons(0(),n__zeros()) zeros() = [5] >= [0] = n__zeros() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 13: Failure MAYBE + Considered Problem: - Strict TRS: activate(n__zeros()) -> zeros() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) uLength(tt(),L) -> s(length(activate(L))) uTake1(tt()) -> nil() uTake2(tt(),M,N,IL) -> cons(activate(N),n__take(activate(M),activate(IL))) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,and,cons,isNat,isNatIList,isNatList,length,nil ,s,take,uLength,uTake1,uTake2,zeros} and constructors {n__0,n__cons,n__length,n__nil,n__s,n__take,n__zeros ,tt} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE