MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: activate(X) -> X activate(n__app(X1,X2)) -> app(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__nil()) -> nil() activate(n__prefix(X)) -> prefix(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWadr(X1,X2)) -> zWadr(activate(X1),activate(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(n__s(X))) from(X) -> n__from(X) nil() -> n__nil() prefix(L) -> cons(nil(),n__zWadr(L,n__prefix(L))) prefix(X) -> n__prefix(X) s(X) -> n__s(X) 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,s/1,zWadr/2} / {cons/2,n__app/2,n__from/1,n__nil/0,n__prefix/1 ,n__s/1,n__zWadr/2} - Obligation: innermost runtime complexity wrt. defined symbols {activate,app,from,nil,prefix,s ,zWadr} and constructors {cons,n__app,n__from,n__nil,n__prefix,n__s,n__zWadr} + 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(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__nil()) -> nil() activate(n__prefix(X)) -> prefix(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWadr(X1,X2)) -> zWadr(activate(X1),activate(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(n__s(X))) from(X) -> n__from(X) nil() -> n__nil() prefix(L) -> cons(nil(),n__zWadr(L,n__prefix(L))) prefix(X) -> n__prefix(X) s(X) -> n__s(X) 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,s/1,zWadr/2} / {cons/2,n__app/2,n__from/1,n__nil/0,n__prefix/1 ,n__s/1,n__zWadr/2} - Obligation: innermost runtime complexity wrt. defined symbols {activate,app,from,nil,prefix,s ,zWadr} and constructors {cons,n__app,n__from,n__nil,n__prefix,n__s,n__zWadr} + 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#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)) activate#(n__nil()) -> c_4(nil#()) activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)) activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) app#(X1,X2) -> c_8() app#(cons(X,XS),YS) -> c_9(activate#(XS)) from#(X) -> c_10() from#(X) -> c_11() nil#() -> c_12() prefix#(L) -> c_13(nil#()) prefix#(X) -> c_14() s#(X) -> c_15() zWadr#(X1,X2) -> c_16() zWadr#(cons(X,XS),cons(Y,YS)) -> c_17(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) Weak DPs and mark the set of starting terms. * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(X) -> c_1() activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)) activate#(n__nil()) -> c_4(nil#()) activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)) activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) app#(X1,X2) -> c_8() app#(cons(X,XS),YS) -> c_9(activate#(XS)) from#(X) -> c_10() from#(X) -> c_11() nil#() -> c_12() prefix#(L) -> c_13(nil#()) prefix#(X) -> c_14() s#(X) -> c_15() zWadr#(X1,X2) -> c_16() zWadr#(cons(X,XS),cons(Y,YS)) -> c_17(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) - Weak TRS: activate(X) -> X activate(n__app(X1,X2)) -> app(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__nil()) -> nil() activate(n__prefix(X)) -> prefix(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWadr(X1,X2)) -> zWadr(activate(X1),activate(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(n__s(X))) from(X) -> n__from(X) nil() -> n__nil() prefix(L) -> cons(nil(),n__zWadr(L,n__prefix(L))) prefix(X) -> n__prefix(X) s(X) -> n__s(X) 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,s/1,zWadr/2,activate#/1,app#/2,from#/1,nil#/0,prefix#/1,s#/1 ,zWadr#/2} / {cons/2,n__app/2,n__from/1,n__nil/0,n__prefix/1,n__s/1,n__zWadr/2,c_1/0,c_2/3,c_3/2,c_4/1,c_5/2 ,c_6/2,c_7/3,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/0,c_17/3} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,app#,from#,nil#,prefix#,s# ,zWadr#} and constructors {cons,n__app,n__from,n__nil,n__prefix,n__s,n__zWadr} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,8,10,11,12,14,15,16} by application of Pre({1,8,10,11,12,14,15,16}) = {2,3,4,5,6,7,9,13,17}. Here rules are labelled as follows: 1: activate#(X) -> c_1() 2: activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 3: activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)) 4: activate#(n__nil()) -> c_4(nil#()) 5: activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)) 6: activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)) 7: activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 8: app#(X1,X2) -> c_8() 9: app#(cons(X,XS),YS) -> c_9(activate#(XS)) 10: from#(X) -> c_10() 11: from#(X) -> c_11() 12: nil#() -> c_12() 13: prefix#(L) -> c_13(nil#()) 14: prefix#(X) -> c_14() 15: s#(X) -> c_15() 16: zWadr#(X1,X2) -> c_16() 17: zWadr#(cons(X,XS),cons(Y,YS)) -> c_17(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)) activate#(n__nil()) -> c_4(nil#()) activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)) activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) app#(cons(X,XS),YS) -> c_9(activate#(XS)) prefix#(L) -> c_13(nil#()) zWadr#(cons(X,XS),cons(Y,YS)) -> c_17(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) - Weak DPs: activate#(X) -> c_1() app#(X1,X2) -> c_8() from#(X) -> c_10() from#(X) -> c_11() nil#() -> c_12() prefix#(X) -> c_14() s#(X) -> c_15() zWadr#(X1,X2) -> c_16() - Weak TRS: activate(X) -> X activate(n__app(X1,X2)) -> app(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__nil()) -> nil() activate(n__prefix(X)) -> prefix(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWadr(X1,X2)) -> zWadr(activate(X1),activate(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(n__s(X))) from(X) -> n__from(X) nil() -> n__nil() prefix(L) -> cons(nil(),n__zWadr(L,n__prefix(L))) prefix(X) -> n__prefix(X) s(X) -> n__s(X) 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,s/1,zWadr/2,activate#/1,app#/2,from#/1,nil#/0,prefix#/1,s#/1 ,zWadr#/2} / {cons/2,n__app/2,n__from/1,n__nil/0,n__prefix/1,n__s/1,n__zWadr/2,c_1/0,c_2/3,c_3/2,c_4/1,c_5/2 ,c_6/2,c_7/3,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/0,c_17/3} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,app#,from#,nil#,prefix#,s# ,zWadr#} and constructors {cons,n__app,n__from,n__nil,n__prefix,n__s,n__zWadr} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {3,8} by application of Pre({3,8}) = {1,2,4,5,6,7,9}. Here rules are labelled as follows: 1: activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 2: activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)) 3: activate#(n__nil()) -> c_4(nil#()) 4: activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)) 5: activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)) 6: activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 7: app#(cons(X,XS),YS) -> c_9(activate#(XS)) 8: prefix#(L) -> c_13(nil#()) 9: zWadr#(cons(X,XS),cons(Y,YS)) -> c_17(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) 10: activate#(X) -> c_1() 11: app#(X1,X2) -> c_8() 12: from#(X) -> c_10() 13: from#(X) -> c_11() 14: nil#() -> c_12() 15: prefix#(X) -> c_14() 16: s#(X) -> c_15() 17: zWadr#(X1,X2) -> c_16() * Step 5: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)) activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)) activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) app#(cons(X,XS),YS) -> c_9(activate#(XS)) zWadr#(cons(X,XS),cons(Y,YS)) -> c_17(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) - Weak DPs: activate#(X) -> c_1() activate#(n__nil()) -> c_4(nil#()) app#(X1,X2) -> c_8() from#(X) -> c_10() from#(X) -> c_11() nil#() -> c_12() prefix#(L) -> c_13(nil#()) prefix#(X) -> c_14() s#(X) -> c_15() zWadr#(X1,X2) -> c_16() - Weak TRS: activate(X) -> X activate(n__app(X1,X2)) -> app(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__nil()) -> nil() activate(n__prefix(X)) -> prefix(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWadr(X1,X2)) -> zWadr(activate(X1),activate(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(n__s(X))) from(X) -> n__from(X) nil() -> n__nil() prefix(L) -> cons(nil(),n__zWadr(L,n__prefix(L))) prefix(X) -> n__prefix(X) s(X) -> n__s(X) 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,s/1,zWadr/2,activate#/1,app#/2,from#/1,nil#/0,prefix#/1,s#/1 ,zWadr#/2} / {cons/2,n__app/2,n__from/1,n__nil/0,n__prefix/1,n__s/1,n__zWadr/2,c_1/0,c_2/3,c_3/2,c_4/1,c_5/2 ,c_6/2,c_7/3,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/0,c_17/3} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,app#,from#,nil#,prefix#,s# ,zWadr#} and constructors {cons,n__app,n__from,n__nil,n__prefix,n__s,n__zWadr} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__nil()) -> c_4(nil#()):9 -->_2 activate#(n__nil()) -> c_4(nil#()):9 -->_1 app#(cons(X,XS),YS) -> c_9(activate#(XS)):6 -->_3 activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)):4 -->_3 activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)):3 -->_2 activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)):3 -->_3 activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)):2 -->_2 activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)):2 -->_1 app#(X1,X2) -> c_8():10 -->_3 activate#(X) -> c_1():8 -->_2 activate#(X) -> c_1():8 -->_3 activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):1 -->_2 activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):1 2:S:activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)) -->_2 activate#(n__nil()) -> c_4(nil#()):9 -->_2 activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)):3 -->_1 from#(X) -> c_11():12 -->_1 from#(X) -> c_10():11 -->_2 activate#(X) -> c_1():8 -->_2 activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)):2 -->_2 activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):1 3:S:activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)) -->_1 prefix#(L) -> c_13(nil#()):14 -->_2 activate#(n__nil()) -> c_4(nil#()):9 -->_2 activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)):4 -->_1 prefix#(X) -> c_14():15 -->_2 activate#(X) -> c_1():8 -->_2 activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)):3 -->_2 activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)):2 -->_2 activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):1 4:S:activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)) -->_2 activate#(n__nil()) -> c_4(nil#()):9 -->_2 activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 s#(X) -> c_15():16 -->_2 activate#(X) -> c_1():8 -->_2 activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)):3 -->_2 activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)):2 -->_2 activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):1 5:S:activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__nil()) -> c_4(nil#()):9 -->_2 activate#(n__nil()) -> c_4(nil#()):9 -->_1 zWadr#(cons(X,XS),cons(Y,YS)) -> c_17(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)):7 -->_1 zWadr#(X1,X2) -> c_16():17 -->_3 activate#(X) -> c_1():8 -->_2 activate#(X) -> c_1():8 -->_3 activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)):4 -->_3 activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)):3 -->_2 activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)):3 -->_3 activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)):2 -->_2 activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)):2 -->_3 activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):1 -->_2 activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):1 6:S:app#(cons(X,XS),YS) -> c_9(activate#(XS)) -->_1 activate#(n__nil()) -> c_4(nil#()):9 -->_1 activate#(X) -> c_1():8 -->_1 activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)):4 -->_1 activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)):3 -->_1 activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)):2 -->_1 activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):1 7:S:zWadr#(cons(X,XS),cons(Y,YS)) -> c_17(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) -->_3 activate#(n__nil()) -> c_4(nil#()):9 -->_2 activate#(n__nil()) -> c_4(nil#()):9 -->_1 app#(X1,X2) -> c_8():10 -->_3 activate#(X) -> c_1():8 -->_2 activate#(X) -> c_1():8 -->_1 app#(cons(X,XS),YS) -> c_9(activate#(XS)):6 -->_3 activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)):4 -->_3 activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)):3 -->_2 activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)):3 -->_3 activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)):2 -->_2 activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)):2 -->_3 activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):1 -->_2 activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):1 8:W:activate#(X) -> c_1() 9:W:activate#(n__nil()) -> c_4(nil#()) -->_1 nil#() -> c_12():13 10:W:app#(X1,X2) -> c_8() 11:W:from#(X) -> c_10() 12:W:from#(X) -> c_11() 13:W:nil#() -> c_12() 14:W:prefix#(L) -> c_13(nil#()) -->_1 nil#() -> c_12():13 15:W:prefix#(X) -> c_14() 16:W:s#(X) -> c_15() 17:W:zWadr#(X1,X2) -> c_16() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 17: zWadr#(X1,X2) -> c_16() 11: from#(X) -> c_10() 12: from#(X) -> c_11() 15: prefix#(X) -> c_14() 14: prefix#(L) -> c_13(nil#()) 16: s#(X) -> c_15() 10: app#(X1,X2) -> c_8() 8: activate#(X) -> c_1() 9: activate#(n__nil()) -> c_4(nil#()) 13: nil#() -> c_12() * Step 6: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)) activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)) activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) app#(cons(X,XS),YS) -> c_9(activate#(XS)) zWadr#(cons(X,XS),cons(Y,YS)) -> c_17(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) - Weak TRS: activate(X) -> X activate(n__app(X1,X2)) -> app(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__nil()) -> nil() activate(n__prefix(X)) -> prefix(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWadr(X1,X2)) -> zWadr(activate(X1),activate(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(n__s(X))) from(X) -> n__from(X) nil() -> n__nil() prefix(L) -> cons(nil(),n__zWadr(L,n__prefix(L))) prefix(X) -> n__prefix(X) s(X) -> n__s(X) 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,s/1,zWadr/2,activate#/1,app#/2,from#/1,nil#/0,prefix#/1,s#/1 ,zWadr#/2} / {cons/2,n__app/2,n__from/1,n__nil/0,n__prefix/1,n__s/1,n__zWadr/2,c_1/0,c_2/3,c_3/2,c_4/1,c_5/2 ,c_6/2,c_7/3,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/0,c_17/3} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,app#,from#,nil#,prefix#,s# ,zWadr#} and constructors {cons,n__app,n__from,n__nil,n__prefix,n__s,n__zWadr} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_1 app#(cons(X,XS),YS) -> c_9(activate#(XS)):6 -->_3 activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)):4 -->_3 activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)):3 -->_2 activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)):3 -->_3 activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)):2 -->_2 activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)):2 -->_3 activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):1 -->_2 activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):1 2:S:activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)) -->_2 activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)):3 -->_2 activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)):2 -->_2 activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):1 3:S:activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)) -->_2 activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)):3 -->_2 activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)):2 -->_2 activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):1 4:S:activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)) -->_2 activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)):3 -->_2 activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)):2 -->_2 activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):1 5:S:activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_1 zWadr#(cons(X,XS),cons(Y,YS)) -> c_17(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)):7 -->_3 activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)):4 -->_3 activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)):3 -->_2 activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)):3 -->_3 activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)):2 -->_2 activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)):2 -->_3 activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):1 -->_2 activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):1 6:S:app#(cons(X,XS),YS) -> c_9(activate#(XS)) -->_1 activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)):4 -->_1 activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)):3 -->_1 activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)):2 -->_1 activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):1 7:S:zWadr#(cons(X,XS),cons(Y,YS)) -> c_17(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) -->_1 app#(cons(X,XS),YS) -> c_9(activate#(XS)):6 -->_3 activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__s(X)) -> c_6(s#(activate(X)),activate#(X)):4 -->_3 activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)):3 -->_2 activate#(n__prefix(X)) -> c_5(prefix#(activate(X)),activate#(X)):3 -->_3 activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)):2 -->_2 activate#(n__from(X)) -> c_3(from#(activate(X)),activate#(X)):2 -->_3 activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):1 -->_2 activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: activate#(n__from(X)) -> c_3(activate#(X)) activate#(n__prefix(X)) -> c_5(activate#(X)) activate#(n__s(X)) -> c_6(activate#(X)) * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: activate#(n__app(X1,X2)) -> c_2(app#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__from(X)) -> c_3(activate#(X)) activate#(n__prefix(X)) -> c_5(activate#(X)) activate#(n__s(X)) -> c_6(activate#(X)) activate#(n__zWadr(X1,X2)) -> c_7(zWadr#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) app#(cons(X,XS),YS) -> c_9(activate#(XS)) zWadr#(cons(X,XS),cons(Y,YS)) -> c_17(app#(Y,cons(X,n__nil())),activate#(XS),activate#(YS)) - Weak TRS: activate(X) -> X activate(n__app(X1,X2)) -> app(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__nil()) -> nil() activate(n__prefix(X)) -> prefix(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWadr(X1,X2)) -> zWadr(activate(X1),activate(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(n__s(X))) from(X) -> n__from(X) nil() -> n__nil() prefix(L) -> cons(nil(),n__zWadr(L,n__prefix(L))) prefix(X) -> n__prefix(X) s(X) -> n__s(X) 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,s/1,zWadr/2,activate#/1,app#/2,from#/1,nil#/0,prefix#/1,s#/1 ,zWadr#/2} / {cons/2,n__app/2,n__from/1,n__nil/0,n__prefix/1,n__s/1,n__zWadr/2,c_1/0,c_2/3,c_3/1,c_4/1,c_5/1 ,c_6/1,c_7/3,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/0,c_16/0,c_17/3} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,app#,from#,nil#,prefix#,s# ,zWadr#} and constructors {cons,n__app,n__from,n__nil,n__prefix,n__s,n__zWadr} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE