MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: activate(X) -> X activate(n__add(X1,X2)) -> add(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__s(X)) -> s(X) add(X1,X2) -> n__add(X1,X2) add(0(),X) -> activate(X) add(s(X),Y) -> s(n__add(activate(X),activate(Y))) and(false(),Y) -> false() and(true(),X) -> activate(X) first(X1,X2) -> n__first(X1,X2) first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(activate(Y),n__first(activate(X),activate(Z))) from(X) -> cons(activate(X),n__from(n__s(activate(X)))) from(X) -> n__from(X) if(false(),X,Y) -> activate(Y) if(true(),X,Y) -> activate(X) s(X) -> n__s(X) - Signature: {activate/1,add/2,and/2,first/2,from/1,if/3,s/1} / {0/0,cons/2,false/0,n__add/2,n__first/2,n__from/1,n__s/1 ,nil/0,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate,add,and,first,from,if,s} and constructors {0 ,cons,false,n__add,n__first,n__from,n__s,nil,true} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. add(s(X),Y) -> s(n__add(activate(X),activate(Y))) first(s(X),cons(Y,Z)) -> cons(activate(Y),n__first(activate(X),activate(Z))) All above mentioned rules can be savely removed. * Step 2: DependencyPairs MAYBE + Considered Problem: - Strict TRS: activate(X) -> X activate(n__add(X1,X2)) -> add(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__s(X)) -> s(X) add(X1,X2) -> n__add(X1,X2) add(0(),X) -> activate(X) and(false(),Y) -> false() and(true(),X) -> activate(X) first(X1,X2) -> n__first(X1,X2) first(0(),X) -> nil() from(X) -> cons(activate(X),n__from(n__s(activate(X)))) from(X) -> n__from(X) if(false(),X,Y) -> activate(Y) if(true(),X,Y) -> activate(X) s(X) -> n__s(X) - Signature: {activate/1,add/2,and/2,first/2,from/1,if/3,s/1} / {0/0,cons/2,false/0,n__add/2,n__first/2,n__from/1,n__s/1 ,nil/0,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate,add,and,first,from,if,s} and constructors {0 ,cons,false,n__add,n__first,n__from,n__s,nil,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs activate#(X) -> c_1() activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) activate#(n__first(X1,X2)) -> c_3(first#(X1,X2)) activate#(n__from(X)) -> c_4(from#(X)) activate#(n__s(X)) -> c_5(s#(X)) add#(X1,X2) -> c_6() add#(0(),X) -> c_7(activate#(X)) and#(false(),Y) -> c_8() and#(true(),X) -> c_9(activate#(X)) first#(X1,X2) -> c_10() first#(0(),X) -> c_11() from#(X) -> c_12(activate#(X),activate#(X)) from#(X) -> c_13() if#(false(),X,Y) -> c_14(activate#(Y)) if#(true(),X,Y) -> c_15(activate#(X)) s#(X) -> c_16() Weak DPs and mark the set of starting terms. * Step 3: UsableRules MAYBE + Considered Problem: - Strict DPs: activate#(X) -> c_1() activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) activate#(n__first(X1,X2)) -> c_3(first#(X1,X2)) activate#(n__from(X)) -> c_4(from#(X)) activate#(n__s(X)) -> c_5(s#(X)) add#(X1,X2) -> c_6() add#(0(),X) -> c_7(activate#(X)) and#(false(),Y) -> c_8() and#(true(),X) -> c_9(activate#(X)) first#(X1,X2) -> c_10() first#(0(),X) -> c_11() from#(X) -> c_12(activate#(X),activate#(X)) from#(X) -> c_13() if#(false(),X,Y) -> c_14(activate#(Y)) if#(true(),X,Y) -> c_15(activate#(X)) s#(X) -> c_16() - Weak TRS: activate(X) -> X activate(n__add(X1,X2)) -> add(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__s(X)) -> s(X) add(X1,X2) -> n__add(X1,X2) add(0(),X) -> activate(X) and(false(),Y) -> false() and(true(),X) -> activate(X) first(X1,X2) -> n__first(X1,X2) first(0(),X) -> nil() from(X) -> cons(activate(X),n__from(n__s(activate(X)))) from(X) -> n__from(X) if(false(),X,Y) -> activate(Y) if(true(),X,Y) -> activate(X) s(X) -> n__s(X) - Signature: {activate/1,add/2,and/2,first/2,from/1,if/3,s/1,activate#/1,add#/2,and#/2,first#/2,from#/1,if#/3 ,s#/1} / {0/0,cons/2,false/0,n__add/2,n__first/2,n__from/1,n__s/1,nil/0,true/0,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/1,c_10/0,c_11/0,c_12/2,c_13/0,c_14/1,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,add#,and#,first#,from#,if# ,s#} and constructors {0,cons,false,n__add,n__first,n__from,n__s,nil,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: activate#(X) -> c_1() activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) activate#(n__first(X1,X2)) -> c_3(first#(X1,X2)) activate#(n__from(X)) -> c_4(from#(X)) activate#(n__s(X)) -> c_5(s#(X)) add#(X1,X2) -> c_6() add#(0(),X) -> c_7(activate#(X)) and#(false(),Y) -> c_8() and#(true(),X) -> c_9(activate#(X)) first#(X1,X2) -> c_10() first#(0(),X) -> c_11() from#(X) -> c_12(activate#(X),activate#(X)) from#(X) -> c_13() if#(false(),X,Y) -> c_14(activate#(Y)) if#(true(),X,Y) -> c_15(activate#(X)) s#(X) -> c_16() * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(X) -> c_1() activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) activate#(n__first(X1,X2)) -> c_3(first#(X1,X2)) activate#(n__from(X)) -> c_4(from#(X)) activate#(n__s(X)) -> c_5(s#(X)) add#(X1,X2) -> c_6() add#(0(),X) -> c_7(activate#(X)) and#(false(),Y) -> c_8() and#(true(),X) -> c_9(activate#(X)) first#(X1,X2) -> c_10() first#(0(),X) -> c_11() from#(X) -> c_12(activate#(X),activate#(X)) from#(X) -> c_13() if#(false(),X,Y) -> c_14(activate#(Y)) if#(true(),X,Y) -> c_15(activate#(X)) s#(X) -> c_16() - Signature: {activate/1,add/2,and/2,first/2,from/1,if/3,s/1,activate#/1,add#/2,and#/2,first#/2,from#/1,if#/3 ,s#/1} / {0/0,cons/2,false/0,n__add/2,n__first/2,n__from/1,n__s/1,nil/0,true/0,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/1,c_10/0,c_11/0,c_12/2,c_13/0,c_14/1,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,add#,and#,first#,from#,if# ,s#} and constructors {0,cons,false,n__add,n__first,n__from,n__s,nil,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,6,8,10,11,13,16} by application of Pre({1,6,8,10,11,13,16}) = {2,3,4,5,7,9,12,14,15}. Here rules are labelled as follows: 1: activate#(X) -> c_1() 2: activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) 3: activate#(n__first(X1,X2)) -> c_3(first#(X1,X2)) 4: activate#(n__from(X)) -> c_4(from#(X)) 5: activate#(n__s(X)) -> c_5(s#(X)) 6: add#(X1,X2) -> c_6() 7: add#(0(),X) -> c_7(activate#(X)) 8: and#(false(),Y) -> c_8() 9: and#(true(),X) -> c_9(activate#(X)) 10: first#(X1,X2) -> c_10() 11: first#(0(),X) -> c_11() 12: from#(X) -> c_12(activate#(X),activate#(X)) 13: from#(X) -> c_13() 14: if#(false(),X,Y) -> c_14(activate#(Y)) 15: if#(true(),X,Y) -> c_15(activate#(X)) 16: s#(X) -> c_16() * Step 5: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) activate#(n__first(X1,X2)) -> c_3(first#(X1,X2)) activate#(n__from(X)) -> c_4(from#(X)) activate#(n__s(X)) -> c_5(s#(X)) add#(0(),X) -> c_7(activate#(X)) and#(true(),X) -> c_9(activate#(X)) from#(X) -> c_12(activate#(X),activate#(X)) if#(false(),X,Y) -> c_14(activate#(Y)) if#(true(),X,Y) -> c_15(activate#(X)) - Weak DPs: activate#(X) -> c_1() add#(X1,X2) -> c_6() and#(false(),Y) -> c_8() first#(X1,X2) -> c_10() first#(0(),X) -> c_11() from#(X) -> c_13() s#(X) -> c_16() - Signature: {activate/1,add/2,and/2,first/2,from/1,if/3,s/1,activate#/1,add#/2,and#/2,first#/2,from#/1,if#/3 ,s#/1} / {0/0,cons/2,false/0,n__add/2,n__first/2,n__from/1,n__s/1,nil/0,true/0,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/1,c_10/0,c_11/0,c_12/2,c_13/0,c_14/1,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,add#,and#,first#,from#,if# ,s#} and constructors {0,cons,false,n__add,n__first,n__from,n__s,nil,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,4} by application of Pre({2,4}) = {5,6,7,8,9}. Here rules are labelled as follows: 1: activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) 2: activate#(n__first(X1,X2)) -> c_3(first#(X1,X2)) 3: activate#(n__from(X)) -> c_4(from#(X)) 4: activate#(n__s(X)) -> c_5(s#(X)) 5: add#(0(),X) -> c_7(activate#(X)) 6: and#(true(),X) -> c_9(activate#(X)) 7: from#(X) -> c_12(activate#(X),activate#(X)) 8: if#(false(),X,Y) -> c_14(activate#(Y)) 9: if#(true(),X,Y) -> c_15(activate#(X)) 10: activate#(X) -> c_1() 11: add#(X1,X2) -> c_6() 12: and#(false(),Y) -> c_8() 13: first#(X1,X2) -> c_10() 14: first#(0(),X) -> c_11() 15: from#(X) -> c_13() 16: s#(X) -> c_16() * Step 6: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) activate#(n__from(X)) -> c_4(from#(X)) add#(0(),X) -> c_7(activate#(X)) and#(true(),X) -> c_9(activate#(X)) from#(X) -> c_12(activate#(X),activate#(X)) if#(false(),X,Y) -> c_14(activate#(Y)) if#(true(),X,Y) -> c_15(activate#(X)) - Weak DPs: activate#(X) -> c_1() activate#(n__first(X1,X2)) -> c_3(first#(X1,X2)) activate#(n__s(X)) -> c_5(s#(X)) add#(X1,X2) -> c_6() and#(false(),Y) -> c_8() first#(X1,X2) -> c_10() first#(0(),X) -> c_11() from#(X) -> c_13() s#(X) -> c_16() - Signature: {activate/1,add/2,and/2,first/2,from/1,if/3,s/1,activate#/1,add#/2,and#/2,first#/2,from#/1,if#/3 ,s#/1} / {0/0,cons/2,false/0,n__add/2,n__first/2,n__from/1,n__s/1,nil/0,true/0,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/1,c_10/0,c_11/0,c_12/2,c_13/0,c_14/1,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,add#,and#,first#,from#,if# ,s#} and constructors {0,cons,false,n__add,n__first,n__from,n__s,nil,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) -->_1 add#(0(),X) -> c_7(activate#(X)):3 -->_1 add#(X1,X2) -> c_6():11 2:S:activate#(n__from(X)) -> c_4(from#(X)) -->_1 from#(X) -> c_12(activate#(X),activate#(X)):5 -->_1 from#(X) -> c_13():15 3:S:add#(0(),X) -> c_7(activate#(X)) -->_1 activate#(n__s(X)) -> c_5(s#(X)):10 -->_1 activate#(n__first(X1,X2)) -> c_3(first#(X1,X2)):9 -->_1 activate#(X) -> c_1():8 -->_1 activate#(n__from(X)) -> c_4(from#(X)):2 -->_1 activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)):1 4:S:and#(true(),X) -> c_9(activate#(X)) -->_1 activate#(n__s(X)) -> c_5(s#(X)):10 -->_1 activate#(n__first(X1,X2)) -> c_3(first#(X1,X2)):9 -->_1 activate#(X) -> c_1():8 -->_1 activate#(n__from(X)) -> c_4(from#(X)):2 -->_1 activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)):1 5:S:from#(X) -> c_12(activate#(X),activate#(X)) -->_2 activate#(n__s(X)) -> c_5(s#(X)):10 -->_1 activate#(n__s(X)) -> c_5(s#(X)):10 -->_2 activate#(n__first(X1,X2)) -> c_3(first#(X1,X2)):9 -->_1 activate#(n__first(X1,X2)) -> c_3(first#(X1,X2)):9 -->_2 activate#(X) -> c_1():8 -->_1 activate#(X) -> c_1():8 -->_2 activate#(n__from(X)) -> c_4(from#(X)):2 -->_1 activate#(n__from(X)) -> c_4(from#(X)):2 -->_2 activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)):1 -->_1 activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)):1 6:S:if#(false(),X,Y) -> c_14(activate#(Y)) -->_1 activate#(n__s(X)) -> c_5(s#(X)):10 -->_1 activate#(n__first(X1,X2)) -> c_3(first#(X1,X2)):9 -->_1 activate#(X) -> c_1():8 -->_1 activate#(n__from(X)) -> c_4(from#(X)):2 -->_1 activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)):1 7:S:if#(true(),X,Y) -> c_15(activate#(X)) -->_1 activate#(n__s(X)) -> c_5(s#(X)):10 -->_1 activate#(n__first(X1,X2)) -> c_3(first#(X1,X2)):9 -->_1 activate#(X) -> c_1():8 -->_1 activate#(n__from(X)) -> c_4(from#(X)):2 -->_1 activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)):1 8:W:activate#(X) -> c_1() 9:W:activate#(n__first(X1,X2)) -> c_3(first#(X1,X2)) -->_1 first#(0(),X) -> c_11():14 -->_1 first#(X1,X2) -> c_10():13 10:W:activate#(n__s(X)) -> c_5(s#(X)) -->_1 s#(X) -> c_16():16 11:W:add#(X1,X2) -> c_6() 12:W:and#(false(),Y) -> c_8() 13:W:first#(X1,X2) -> c_10() 14:W:first#(0(),X) -> c_11() 15:W:from#(X) -> c_13() 16:W:s#(X) -> c_16() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 12: and#(false(),Y) -> c_8() 11: add#(X1,X2) -> c_6() 15: from#(X) -> c_13() 8: activate#(X) -> c_1() 9: activate#(n__first(X1,X2)) -> c_3(first#(X1,X2)) 13: first#(X1,X2) -> c_10() 14: first#(0(),X) -> c_11() 10: activate#(n__s(X)) -> c_5(s#(X)) 16: s#(X) -> c_16() * Step 7: RemoveHeads MAYBE + Considered Problem: - Strict DPs: activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) activate#(n__from(X)) -> c_4(from#(X)) add#(0(),X) -> c_7(activate#(X)) and#(true(),X) -> c_9(activate#(X)) from#(X) -> c_12(activate#(X),activate#(X)) if#(false(),X,Y) -> c_14(activate#(Y)) if#(true(),X,Y) -> c_15(activate#(X)) - Signature: {activate/1,add/2,and/2,first/2,from/1,if/3,s/1,activate#/1,add#/2,and#/2,first#/2,from#/1,if#/3 ,s#/1} / {0/0,cons/2,false/0,n__add/2,n__first/2,n__from/1,n__s/1,nil/0,true/0,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/1,c_10/0,c_11/0,c_12/2,c_13/0,c_14/1,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,add#,and#,first#,from#,if# ,s#} and constructors {0,cons,false,n__add,n__first,n__from,n__s,nil,true} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) -->_1 add#(0(),X) -> c_7(activate#(X)):3 2:S:activate#(n__from(X)) -> c_4(from#(X)) -->_1 from#(X) -> c_12(activate#(X),activate#(X)):5 3:S:add#(0(),X) -> c_7(activate#(X)) -->_1 activate#(n__from(X)) -> c_4(from#(X)):2 -->_1 activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)):1 4:S:and#(true(),X) -> c_9(activate#(X)) -->_1 activate#(n__from(X)) -> c_4(from#(X)):2 -->_1 activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)):1 5:S:from#(X) -> c_12(activate#(X),activate#(X)) -->_2 activate#(n__from(X)) -> c_4(from#(X)):2 -->_1 activate#(n__from(X)) -> c_4(from#(X)):2 -->_2 activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)):1 -->_1 activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)):1 6:S:if#(false(),X,Y) -> c_14(activate#(Y)) -->_1 activate#(n__from(X)) -> c_4(from#(X)):2 -->_1 activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)):1 7:S:if#(true(),X,Y) -> c_15(activate#(X)) -->_1 activate#(n__from(X)) -> c_4(from#(X)):2 -->_1 activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)):1 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(4,and#(true(),X) -> c_9(activate#(X))) ,(6,if#(false(),X,Y) -> c_14(activate#(Y))) ,(7,if#(true(),X,Y) -> c_15(activate#(X)))] * Step 8: WeightGap MAYBE + Considered Problem: - Strict DPs: activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) activate#(n__from(X)) -> c_4(from#(X)) add#(0(),X) -> c_7(activate#(X)) from#(X) -> c_12(activate#(X),activate#(X)) - Signature: {activate/1,add/2,and/2,first/2,from/1,if/3,s/1,activate#/1,add#/2,and#/2,first#/2,from#/1,if#/3 ,s#/1} / {0/0,cons/2,false/0,n__add/2,n__first/2,n__from/1,n__s/1,nil/0,true/0,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/1,c_10/0,c_11/0,c_12/2,c_13/0,c_14/1,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,add#,and#,first#,from#,if# ,s#} and constructors {0,cons,false,n__add,n__first,n__from,n__s,nil,true} + 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_4) = {1}, uargs(c_7) = {1}, uargs(c_12) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(activate) = [0] p(add) = [0] p(and) = [0] p(cons) = [0] p(false) = [0] p(first) = [0] p(from) = [0] p(if) = [0] p(n__add) = [0] p(n__first) = [0] p(n__from) = [0] p(n__s) = [0] p(nil) = [0] p(s) = [0] p(true) = [0] p(activate#) = [0] p(add#) = [0] p(and#) = [0] p(first#) = [0] p(from#) = [1] p(if#) = [0] p(s#) = [0] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [0] p(c_4) = [1] x1 + [0] p(c_5) = [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) = [0] p(c_12) = [1] x1 + [1] x2 + [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] Following rules are strictly oriented: from#(X) = [1] > [0] = c_12(activate#(X),activate#(X)) Following rules are (at-least) weakly oriented: activate#(n__add(X1,X2)) = [0] >= [0] = c_2(add#(X1,X2)) activate#(n__from(X)) = [0] >= [1] = c_4(from#(X)) add#(0(),X) = [0] >= [0] = c_7(activate#(X)) 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__add(X1,X2)) -> c_2(add#(X1,X2)) activate#(n__from(X)) -> c_4(from#(X)) add#(0(),X) -> c_7(activate#(X)) - Weak DPs: from#(X) -> c_12(activate#(X),activate#(X)) - Signature: {activate/1,add/2,and/2,first/2,from/1,if/3,s/1,activate#/1,add#/2,and#/2,first#/2,from#/1,if#/3 ,s#/1} / {0/0,cons/2,false/0,n__add/2,n__first/2,n__from/1,n__s/1,nil/0,true/0,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/1,c_10/0,c_11/0,c_12/2,c_13/0,c_14/1,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,add#,and#,first#,from#,if# ,s#} and constructors {0,cons,false,n__add,n__first,n__from,n__s,nil,true} + 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_4) = {1}, uargs(c_7) = {1}, uargs(c_12) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(activate) = [0] p(add) = [0] p(and) = [0] p(cons) = [0] p(false) = [0] p(first) = [0] p(from) = [0] p(if) = [0] p(n__add) = [0] p(n__first) = [0] p(n__from) = [0] p(n__s) = [0] p(nil) = [0] p(s) = [0] p(true) = [0] p(activate#) = [0] p(add#) = [3] p(and#) = [0] p(first#) = [0] p(from#) = [0] p(if#) = [0] p(s#) = [0] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [0] p(c_4) = [1] x1 + [0] p(c_5) = [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) = [0] p(c_12) = [1] x1 + [1] x2 + [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] Following rules are strictly oriented: add#(0(),X) = [3] > [0] = c_7(activate#(X)) Following rules are (at-least) weakly oriented: activate#(n__add(X1,X2)) = [0] >= [3] = c_2(add#(X1,X2)) activate#(n__from(X)) = [0] >= [0] = c_4(from#(X)) from#(X) = [0] >= [0] = c_12(activate#(X),activate#(X)) 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__add(X1,X2)) -> c_2(add#(X1,X2)) activate#(n__from(X)) -> c_4(from#(X)) - Weak DPs: add#(0(),X) -> c_7(activate#(X)) from#(X) -> c_12(activate#(X),activate#(X)) - Signature: {activate/1,add/2,and/2,first/2,from/1,if/3,s/1,activate#/1,add#/2,and#/2,first#/2,from#/1,if#/3 ,s#/1} / {0/0,cons/2,false/0,n__add/2,n__first/2,n__from/1,n__s/1,nil/0,true/0,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/1,c_10/0,c_11/0,c_12/2,c_13/0,c_14/1,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,add#,and#,first#,from#,if# ,s#} and constructors {0,cons,false,n__add,n__first,n__from,n__s,nil,true} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE