MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: activate(X) -> X activate(n__app(X1,X2)) -> app(X1,X2) activate(n__from(X)) -> from(X) activate(n__nil()) -> nil() activate(n__zWadr(X1,X2)) -> zWadr(X1,X2) app(X1,X2) -> n__app(X1,X2) app(cons(X,XS),YS) -> cons(X,n__app(activate(XS),YS)) app(nil(),YS) -> YS from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) nil() -> n__nil() prefix(L) -> cons(nil(),n__zWadr(L,prefix(L))) zWadr(X1,X2) -> n__zWadr(X1,X2) zWadr(XS,nil()) -> nil() zWadr(cons(X,XS),cons(Y,YS)) -> cons(app(Y,cons(X,n__nil())),n__zWadr(activate(XS),activate(YS))) zWadr(nil(),YS) -> nil() - Signature: {activate/1,app/2,from/1,nil/0,prefix/1,zWadr/2} / {cons/2,n__app/2,n__from/1,n__nil/0,n__zWadr/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,app,from,nil,prefix ,zWadr} and constructors {cons,n__app,n__from,n__nil,n__zWadr,s} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. app(nil(),YS) -> YS zWadr(XS,nil()) -> nil() zWadr(nil(),YS) -> nil() All above mentioned rules can be savely removed. * Step 2: DependencyPairs MAYBE + Considered Problem: - Strict TRS: activate(X) -> X activate(n__app(X1,X2)) -> app(X1,X2) activate(n__from(X)) -> from(X) activate(n__nil()) -> nil() activate(n__zWadr(X1,X2)) -> zWadr(X1,X2) app(X1,X2) -> n__app(X1,X2) app(cons(X,XS),YS) -> cons(X,n__app(activate(XS),YS)) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) nil() -> n__nil() prefix(L) -> cons(nil(),n__zWadr(L,prefix(L))) zWadr(X1,X2) -> n__zWadr(X1,X2) zWadr(cons(X,XS),cons(Y,YS)) -> cons(app(Y,cons(X,n__nil())),n__zWadr(activate(XS),activate(YS))) - Signature: {activate/1,app/2,from/1,nil/0,prefix/1,zWadr/2} / {cons/2,n__app/2,n__from/1,n__nil/0,n__zWadr/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,app,from,nil,prefix ,zWadr} and constructors {cons,n__app,n__from,n__nil,n__zWadr,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs activate#(X) -> c_1() activate#(n__app(X1,X2)) -> c_2(app#(X1,X2)) activate#(n__from(X)) -> c_3(from#(X)) activate#(n__nil()) -> c_4(nil#()) activate#(n__zWadr(X1,X2)) -> c_5(zWadr#(X1,X2)) app#(X1,X2) -> c_6() app#(cons(X,XS),YS) -> c_7(activate#(XS)) from#(X) -> c_8() from#(X) -> c_9() nil#() -> c_10() prefix#(L) -> c_11(nil#(),prefix#(L)) zWadr#(X1,X2) -> c_12() zWadr#(cons(X,XS),cons(Y,YS)) -> c_13(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) Weak DPs and mark the set of starting terms. * Step 3: UsableRules MAYBE + Considered Problem: - Strict DPs: activate#(X) -> c_1() activate#(n__app(X1,X2)) -> c_2(app#(X1,X2)) activate#(n__from(X)) -> c_3(from#(X)) activate#(n__nil()) -> c_4(nil#()) activate#(n__zWadr(X1,X2)) -> c_5(zWadr#(X1,X2)) app#(X1,X2) -> c_6() app#(cons(X,XS),YS) -> c_7(activate#(XS)) from#(X) -> c_8() from#(X) -> c_9() nil#() -> c_10() prefix#(L) -> c_11(nil#(),prefix#(L)) zWadr#(X1,X2) -> c_12() zWadr#(cons(X,XS),cons(Y,YS)) -> c_13(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) - Weak TRS: activate(X) -> X activate(n__app(X1,X2)) -> app(X1,X2) activate(n__from(X)) -> from(X) activate(n__nil()) -> nil() activate(n__zWadr(X1,X2)) -> zWadr(X1,X2) app(X1,X2) -> n__app(X1,X2) app(cons(X,XS),YS) -> cons(X,n__app(activate(XS),YS)) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) nil() -> n__nil() prefix(L) -> cons(nil(),n__zWadr(L,prefix(L))) zWadr(X1,X2) -> n__zWadr(X1,X2) zWadr(cons(X,XS),cons(Y,YS)) -> cons(app(Y,cons(X,n__nil())),n__zWadr(activate(XS),activate(YS))) - Signature: {activate/1,app/2,from/1,nil/0,prefix/1,zWadr/2,activate#/1,app#/2,from#/1,nil#/0,prefix#/1 ,zWadr#/2} / {cons/2,n__app/2,n__from/1,n__nil/0,n__zWadr/2,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/1 ,c_8/0,c_9/0,c_10/0,c_11/2,c_12/0,c_13/3} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,app#,from#,nil#,prefix# ,zWadr#} and constructors {cons,n__app,n__from,n__nil,n__zWadr,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: activate#(X) -> c_1() activate#(n__app(X1,X2)) -> c_2(app#(X1,X2)) activate#(n__from(X)) -> c_3(from#(X)) activate#(n__nil()) -> c_4(nil#()) activate#(n__zWadr(X1,X2)) -> c_5(zWadr#(X1,X2)) app#(X1,X2) -> c_6() app#(cons(X,XS),YS) -> c_7(activate#(XS)) from#(X) -> c_8() from#(X) -> c_9() nil#() -> c_10() prefix#(L) -> c_11(nil#(),prefix#(L)) zWadr#(X1,X2) -> c_12() zWadr#(cons(X,XS),cons(Y,YS)) -> c_13(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(X) -> c_1() activate#(n__app(X1,X2)) -> c_2(app#(X1,X2)) activate#(n__from(X)) -> c_3(from#(X)) activate#(n__nil()) -> c_4(nil#()) activate#(n__zWadr(X1,X2)) -> c_5(zWadr#(X1,X2)) app#(X1,X2) -> c_6() app#(cons(X,XS),YS) -> c_7(activate#(XS)) from#(X) -> c_8() from#(X) -> c_9() nil#() -> c_10() prefix#(L) -> c_11(nil#(),prefix#(L)) zWadr#(X1,X2) -> c_12() zWadr#(cons(X,XS),cons(Y,YS)) -> c_13(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) - Signature: {activate/1,app/2,from/1,nil/0,prefix/1,zWadr/2,activate#/1,app#/2,from#/1,nil#/0,prefix#/1 ,zWadr#/2} / {cons/2,n__app/2,n__from/1,n__nil/0,n__zWadr/2,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/1 ,c_8/0,c_9/0,c_10/0,c_11/2,c_12/0,c_13/3} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,app#,from#,nil#,prefix# ,zWadr#} and constructors {cons,n__app,n__from,n__nil,n__zWadr,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,6,8,9,10,12} by application of Pre({1,6,8,9,10,12}) = {2,3,4,5,7,11,13}. Here rules are labelled as follows: 1: activate#(X) -> c_1() 2: activate#(n__app(X1,X2)) -> c_2(app#(X1,X2)) 3: activate#(n__from(X)) -> c_3(from#(X)) 4: activate#(n__nil()) -> c_4(nil#()) 5: activate#(n__zWadr(X1,X2)) -> c_5(zWadr#(X1,X2)) 6: app#(X1,X2) -> c_6() 7: app#(cons(X,XS),YS) -> c_7(activate#(XS)) 8: from#(X) -> c_8() 9: from#(X) -> c_9() 10: nil#() -> c_10() 11: prefix#(L) -> c_11(nil#(),prefix#(L)) 12: zWadr#(X1,X2) -> c_12() 13: zWadr#(cons(X,XS),cons(Y,YS)) -> c_13(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) * Step 5: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(n__app(X1,X2)) -> c_2(app#(X1,X2)) activate#(n__from(X)) -> c_3(from#(X)) activate#(n__nil()) -> c_4(nil#()) activate#(n__zWadr(X1,X2)) -> c_5(zWadr#(X1,X2)) app#(cons(X,XS),YS) -> c_7(activate#(XS)) prefix#(L) -> c_11(nil#(),prefix#(L)) zWadr#(cons(X,XS),cons(Y,YS)) -> c_13(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) - Weak DPs: activate#(X) -> c_1() app#(X1,X2) -> c_6() from#(X) -> c_8() from#(X) -> c_9() nil#() -> c_10() zWadr#(X1,X2) -> c_12() - Signature: {activate/1,app/2,from/1,nil/0,prefix/1,zWadr/2,activate#/1,app#/2,from#/1,nil#/0,prefix#/1 ,zWadr#/2} / {cons/2,n__app/2,n__from/1,n__nil/0,n__zWadr/2,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/1 ,c_8/0,c_9/0,c_10/0,c_11/2,c_12/0,c_13/3} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,app#,from#,nil#,prefix# ,zWadr#} and constructors {cons,n__app,n__from,n__nil,n__zWadr,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,3} by application of Pre({2,3}) = {5,7}. Here rules are labelled as follows: 1: activate#(n__app(X1,X2)) -> c_2(app#(X1,X2)) 2: activate#(n__from(X)) -> c_3(from#(X)) 3: activate#(n__nil()) -> c_4(nil#()) 4: activate#(n__zWadr(X1,X2)) -> c_5(zWadr#(X1,X2)) 5: app#(cons(X,XS),YS) -> c_7(activate#(XS)) 6: prefix#(L) -> c_11(nil#(),prefix#(L)) 7: zWadr#(cons(X,XS),cons(Y,YS)) -> c_13(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) 8: activate#(X) -> c_1() 9: app#(X1,X2) -> c_6() 10: from#(X) -> c_8() 11: from#(X) -> c_9() 12: nil#() -> c_10() 13: zWadr#(X1,X2) -> c_12() * Step 6: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: activate#(n__app(X1,X2)) -> c_2(app#(X1,X2)) activate#(n__zWadr(X1,X2)) -> c_5(zWadr#(X1,X2)) app#(cons(X,XS),YS) -> c_7(activate#(XS)) prefix#(L) -> c_11(nil#(),prefix#(L)) zWadr#(cons(X,XS),cons(Y,YS)) -> c_13(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) - Weak DPs: activate#(X) -> c_1() activate#(n__from(X)) -> c_3(from#(X)) activate#(n__nil()) -> c_4(nil#()) app#(X1,X2) -> c_6() from#(X) -> c_8() from#(X) -> c_9() nil#() -> c_10() zWadr#(X1,X2) -> c_12() - Signature: {activate/1,app/2,from/1,nil/0,prefix/1,zWadr/2,activate#/1,app#/2,from#/1,nil#/0,prefix#/1 ,zWadr#/2} / {cons/2,n__app/2,n__from/1,n__nil/0,n__zWadr/2,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/1 ,c_8/0,c_9/0,c_10/0,c_11/2,c_12/0,c_13/3} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,app#,from#,nil#,prefix# ,zWadr#} and constructors {cons,n__app,n__from,n__nil,n__zWadr,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:activate#(n__app(X1,X2)) -> c_2(app#(X1,X2)) -->_1 app#(cons(X,XS),YS) -> c_7(activate#(XS)):3 -->_1 app#(X1,X2) -> c_6():9 2:S:activate#(n__zWadr(X1,X2)) -> c_5(zWadr#(X1,X2)) -->_1 zWadr#(cons(X,XS),cons(Y,YS)) -> c_13(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)):5 -->_1 zWadr#(X1,X2) -> c_12():13 3:S:app#(cons(X,XS),YS) -> c_7(activate#(XS)) -->_1 activate#(n__nil()) -> c_4(nil#()):8 -->_1 activate#(n__from(X)) -> c_3(from#(X)):7 -->_1 activate#(X) -> c_1():6 -->_1 activate#(n__zWadr(X1,X2)) -> c_5(zWadr#(X1,X2)):2 -->_1 activate#(n__app(X1,X2)) -> c_2(app#(X1,X2)):1 4:S:prefix#(L) -> c_11(nil#(),prefix#(L)) -->_1 nil#() -> c_10():12 -->_2 prefix#(L) -> c_11(nil#(),prefix#(L)):4 5:S:zWadr#(cons(X,XS),cons(Y,YS)) -> c_13(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) -->_3 activate#(n__nil()) -> c_4(nil#()):8 -->_2 activate#(n__nil()) -> c_4(nil#()):8 -->_3 activate#(n__from(X)) -> c_3(from#(X)):7 -->_2 activate#(n__from(X)) -> c_3(from#(X)):7 -->_1 app#(X1,X2) -> c_6():9 -->_3 activate#(X) -> c_1():6 -->_2 activate#(X) -> c_1():6 -->_1 app#(cons(X,XS),YS) -> c_7(activate#(XS)):3 -->_3 activate#(n__zWadr(X1,X2)) -> c_5(zWadr#(X1,X2)):2 -->_2 activate#(n__zWadr(X1,X2)) -> c_5(zWadr#(X1,X2)):2 -->_3 activate#(n__app(X1,X2)) -> c_2(app#(X1,X2)):1 -->_2 activate#(n__app(X1,X2)) -> c_2(app#(X1,X2)):1 6:W:activate#(X) -> c_1() 7:W:activate#(n__from(X)) -> c_3(from#(X)) -->_1 from#(X) -> c_9():11 -->_1 from#(X) -> c_8():10 8:W:activate#(n__nil()) -> c_4(nil#()) -->_1 nil#() -> c_10():12 9:W:app#(X1,X2) -> c_6() 10:W:from#(X) -> c_8() 11:W:from#(X) -> c_9() 12:W:nil#() -> c_10() 13:W:zWadr#(X1,X2) -> c_12() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 13: zWadr#(X1,X2) -> c_12() 9: app#(X1,X2) -> c_6() 6: activate#(X) -> c_1() 7: activate#(n__from(X)) -> c_3(from#(X)) 10: from#(X) -> c_8() 11: from#(X) -> c_9() 8: activate#(n__nil()) -> c_4(nil#()) 12: nil#() -> c_10() * Step 7: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: activate#(n__app(X1,X2)) -> c_2(app#(X1,X2)) activate#(n__zWadr(X1,X2)) -> c_5(zWadr#(X1,X2)) app#(cons(X,XS),YS) -> c_7(activate#(XS)) prefix#(L) -> c_11(nil#(),prefix#(L)) zWadr#(cons(X,XS),cons(Y,YS)) -> c_13(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) - Signature: {activate/1,app/2,from/1,nil/0,prefix/1,zWadr/2,activate#/1,app#/2,from#/1,nil#/0,prefix#/1 ,zWadr#/2} / {cons/2,n__app/2,n__from/1,n__nil/0,n__zWadr/2,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/1 ,c_8/0,c_9/0,c_10/0,c_11/2,c_12/0,c_13/3} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,app#,from#,nil#,prefix# ,zWadr#} and constructors {cons,n__app,n__from,n__nil,n__zWadr,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:activate#(n__app(X1,X2)) -> c_2(app#(X1,X2)) -->_1 app#(cons(X,XS),YS) -> c_7(activate#(XS)):3 2:S:activate#(n__zWadr(X1,X2)) -> c_5(zWadr#(X1,X2)) -->_1 zWadr#(cons(X,XS),cons(Y,YS)) -> c_13(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)):5 3:S:app#(cons(X,XS),YS) -> c_7(activate#(XS)) -->_1 activate#(n__zWadr(X1,X2)) -> c_5(zWadr#(X1,X2)):2 -->_1 activate#(n__app(X1,X2)) -> c_2(app#(X1,X2)):1 4:S:prefix#(L) -> c_11(nil#(),prefix#(L)) -->_2 prefix#(L) -> c_11(nil#(),prefix#(L)):4 5:S:zWadr#(cons(X,XS),cons(Y,YS)) -> c_13(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) -->_1 app#(cons(X,XS),YS) -> c_7(activate#(XS)):3 -->_3 activate#(n__zWadr(X1,X2)) -> c_5(zWadr#(X1,X2)):2 -->_2 activate#(n__zWadr(X1,X2)) -> c_5(zWadr#(X1,X2)):2 -->_3 activate#(n__app(X1,X2)) -> c_2(app#(X1,X2)):1 -->_2 activate#(n__app(X1,X2)) -> c_2(app#(X1,X2)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: prefix#(L) -> c_11(prefix#(L)) * Step 8: WeightGap MAYBE + Considered Problem: - Strict DPs: activate#(n__app(X1,X2)) -> c_2(app#(X1,X2)) activate#(n__zWadr(X1,X2)) -> c_5(zWadr#(X1,X2)) app#(cons(X,XS),YS) -> c_7(activate#(XS)) prefix#(L) -> c_11(prefix#(L)) zWadr#(cons(X,XS),cons(Y,YS)) -> c_13(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) - Signature: {activate/1,app/2,from/1,nil/0,prefix/1,zWadr/2,activate#/1,app#/2,from#/1,nil#/0,prefix#/1 ,zWadr#/2} / {cons/2,n__app/2,n__from/1,n__nil/0,n__zWadr/2,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/1 ,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0,c_13/3} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,app#,from#,nil#,prefix# ,zWadr#} and constructors {cons,n__app,n__from,n__nil,n__zWadr,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1}, uargs(c_11) = {1}, uargs(c_13) = {1,2,3} Following symbols are considered usable: all TcT has computed the following interpretation: p(activate) = [0] p(app) = [1] x1 + [0] p(cons) = [0] p(from) = [0] p(n__app) = [0] p(n__from) = [0] p(n__nil) = [0] p(n__zWadr) = [0] p(nil) = [0] p(prefix) = [1] p(s) = [0] p(zWadr) = [0] p(activate#) = [0] p(app#) = [0] p(from#) = [0] p(nil#) = [0] p(prefix#) = [1] x1 + [0] p(zWadr#) = [7] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [1] x1 + [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [1] x1 + [0] p(c_12) = [0] p(c_13) = [1] x1 + [1] x2 + [1] x3 + [0] Following rules are strictly oriented: zWadr#(cons(X,XS),cons(Y,YS)) = [7] > [0] = c_13(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) Following rules are (at-least) weakly oriented: activate#(n__app(X1,X2)) = [0] >= [0] = c_2(app#(X1,X2)) activate#(n__zWadr(X1,X2)) = [0] >= [7] = c_5(zWadr#(X1,X2)) app#(cons(X,XS),YS) = [0] >= [0] = c_7(activate#(XS)) prefix#(L) = [1] L + [0] >= [1] L + [0] = c_11(prefix#(L)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 9: WeightGap MAYBE + Considered Problem: - Strict DPs: activate#(n__app(X1,X2)) -> c_2(app#(X1,X2)) activate#(n__zWadr(X1,X2)) -> c_5(zWadr#(X1,X2)) app#(cons(X,XS),YS) -> c_7(activate#(XS)) prefix#(L) -> c_11(prefix#(L)) - Weak DPs: zWadr#(cons(X,XS),cons(Y,YS)) -> c_13(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) - Signature: {activate/1,app/2,from/1,nil/0,prefix/1,zWadr/2,activate#/1,app#/2,from#/1,nil#/0,prefix#/1 ,zWadr#/2} / {cons/2,n__app/2,n__from/1,n__nil/0,n__zWadr/2,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/1 ,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0,c_13/3} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,app#,from#,nil#,prefix# ,zWadr#} and constructors {cons,n__app,n__from,n__nil,n__zWadr,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1}, uargs(c_11) = {1}, uargs(c_13) = {1,2,3} Following symbols are considered usable: all TcT has computed the following interpretation: p(activate) = [2] p(app) = [2] x1 + [2] p(cons) = [0] p(from) = [2] p(n__app) = [0] p(n__from) = [0] p(n__nil) = [0] p(n__zWadr) = [0] p(nil) = [0] p(prefix) = [0] p(s) = [2] p(zWadr) = [0] p(activate#) = [4] p(app#) = [0] p(from#) = [0] p(nil#) = [0] p(prefix#) = [8] x1 + [11] p(zWadr#) = [12] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [1] x1 + [11] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [1] x1 + [4] p(c_12) = [0] p(c_13) = [1] x1 + [1] x2 + [1] x3 + [4] Following rules are strictly oriented: activate#(n__app(X1,X2)) = [4] > [0] = c_2(app#(X1,X2)) Following rules are (at-least) weakly oriented: activate#(n__zWadr(X1,X2)) = [4] >= [12] = c_5(zWadr#(X1,X2)) app#(cons(X,XS),YS) = [0] >= [15] = c_7(activate#(XS)) prefix#(L) = [8] L + [11] >= [8] L + [15] = c_11(prefix#(L)) zWadr#(cons(X,XS),cons(Y,YS)) = [12] >= [12] = c_13(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 10: Failure MAYBE + Considered Problem: - Strict DPs: activate#(n__zWadr(X1,X2)) -> c_5(zWadr#(X1,X2)) app#(cons(X,XS),YS) -> c_7(activate#(XS)) prefix#(L) -> c_11(prefix#(L)) - Weak DPs: activate#(n__app(X1,X2)) -> c_2(app#(X1,X2)) zWadr#(cons(X,XS),cons(Y,YS)) -> c_13(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) - Signature: {activate/1,app/2,from/1,nil/0,prefix/1,zWadr/2,activate#/1,app#/2,from#/1,nil#/0,prefix#/1 ,zWadr#/2} / {cons/2,n__app/2,n__from/1,n__nil/0,n__zWadr/2,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/1 ,c_8/0,c_9/0,c_10/0,c_11/1,c_12/0,c_13/3} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,app#,from#,nil#,prefix# ,zWadr#} and constructors {cons,n__app,n__from,n__nil,n__zWadr,s} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE