MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: activate(X) -> X activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) s(X) -> n__s(X) sel(0(),cons(X,XS)) -> X sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) zWquot(X1,X2) -> n__zWquot(X1,X2) zWquot(XS,nil()) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) zWquot(nil(),XS) -> nil() - Signature: {activate/1,from/1,minus/2,quot/2,s/1,sel/2,zWquot/2} / {0/0,cons/2,n__from/1,n__s/1,n__zWquot/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate,from,minus,quot,s,sel ,zWquot} and constructors {0,cons,n__from,n__s,n__zWquot,nil} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. minus(s(X),s(Y)) -> minus(X,Y) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) All above mentioned rules can be savely removed. * Step 2: DependencyPairs MAYBE + Considered Problem: - Strict TRS: activate(X) -> X activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) minus(X,0()) -> 0() s(X) -> n__s(X) sel(0(),cons(X,XS)) -> X zWquot(X1,X2) -> n__zWquot(X1,X2) zWquot(XS,nil()) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) zWquot(nil(),XS) -> nil() - Signature: {activate/1,from/1,minus/2,quot/2,s/1,sel/2,zWquot/2} / {0/0,cons/2,n__from/1,n__s/1,n__zWquot/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate,from,minus,quot,s,sel ,zWquot} and constructors {0,cons,n__from,n__s,n__zWquot,nil} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs activate#(X) -> c_1() activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)) activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) from#(X) -> c_5() from#(X) -> c_6() minus#(X,0()) -> c_7() s#(X) -> c_8() sel#(0(),cons(X,XS)) -> c_9() zWquot#(X1,X2) -> c_10() zWquot#(XS,nil()) -> c_11() zWquot#(cons(X,XS),cons(Y,YS)) -> c_12(quot#(X,Y),activate#(XS),activate#(YS)) zWquot#(nil(),XS) -> c_13() Weak DPs and mark the set of starting terms. * Step 3: UsableRules MAYBE + Considered Problem: - Strict DPs: activate#(X) -> c_1() activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)) activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) from#(X) -> c_5() from#(X) -> c_6() minus#(X,0()) -> c_7() s#(X) -> c_8() sel#(0(),cons(X,XS)) -> c_9() zWquot#(X1,X2) -> c_10() zWquot#(XS,nil()) -> c_11() zWquot#(cons(X,XS),cons(Y,YS)) -> c_12(quot#(X,Y),activate#(XS),activate#(YS)) zWquot#(nil(),XS) -> c_13() - Weak TRS: activate(X) -> X activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) minus(X,0()) -> 0() s(X) -> n__s(X) sel(0(),cons(X,XS)) -> X zWquot(X1,X2) -> n__zWquot(X1,X2) zWquot(XS,nil()) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) zWquot(nil(),XS) -> nil() - Signature: {activate/1,from/1,minus/2,quot/2,s/1,sel/2,zWquot/2,activate#/1,from#/1,minus#/2,quot#/2,s#/1,sel#/2 ,zWquot#/2} / {0/0,cons/2,n__from/1,n__s/1,n__zWquot/2,nil/0,c_1/0,c_2/2,c_3/2,c_4/3,c_5/0,c_6/0,c_7/0,c_8/0 ,c_9/0,c_10/0,c_11/0,c_12/3,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,from#,minus#,quot#,s#,sel# ,zWquot#} and constructors {0,cons,n__from,n__s,n__zWquot,nil} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: activate(X) -> X activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) zWquot(X1,X2) -> n__zWquot(X1,X2) zWquot(XS,nil()) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) zWquot(nil(),XS) -> nil() activate#(X) -> c_1() activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)) activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) from#(X) -> c_5() from#(X) -> c_6() minus#(X,0()) -> c_7() s#(X) -> c_8() sel#(0(),cons(X,XS)) -> c_9() zWquot#(X1,X2) -> c_10() zWquot#(XS,nil()) -> c_11() zWquot#(cons(X,XS),cons(Y,YS)) -> c_12(quot#(X,Y),activate#(XS),activate#(YS)) zWquot#(nil(),XS) -> c_13() * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(X) -> c_1() activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)) activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) from#(X) -> c_5() from#(X) -> c_6() minus#(X,0()) -> c_7() s#(X) -> c_8() sel#(0(),cons(X,XS)) -> c_9() zWquot#(X1,X2) -> c_10() zWquot#(XS,nil()) -> c_11() zWquot#(cons(X,XS),cons(Y,YS)) -> c_12(quot#(X,Y),activate#(XS),activate#(YS)) zWquot#(nil(),XS) -> c_13() - Weak TRS: activate(X) -> X activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) zWquot(X1,X2) -> n__zWquot(X1,X2) zWquot(XS,nil()) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) zWquot(nil(),XS) -> nil() - Signature: {activate/1,from/1,minus/2,quot/2,s/1,sel/2,zWquot/2,activate#/1,from#/1,minus#/2,quot#/2,s#/1,sel#/2 ,zWquot#/2} / {0/0,cons/2,n__from/1,n__s/1,n__zWquot/2,nil/0,c_1/0,c_2/2,c_3/2,c_4/3,c_5/0,c_6/0,c_7/0,c_8/0 ,c_9/0,c_10/0,c_11/0,c_12/3,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,from#,minus#,quot#,s#,sel# ,zWquot#} and constructors {0,cons,n__from,n__s,n__zWquot,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,5,6,7,8,9,10,11,13} by application of Pre({1,5,6,7,8,9,10,11,13}) = {2,3,4,12}. Here rules are labelled as follows: 1: activate#(X) -> c_1() 2: activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)) 3: activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)) 4: activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 5: from#(X) -> c_5() 6: from#(X) -> c_6() 7: minus#(X,0()) -> c_7() 8: s#(X) -> c_8() 9: sel#(0(),cons(X,XS)) -> c_9() 10: zWquot#(X1,X2) -> c_10() 11: zWquot#(XS,nil()) -> c_11() 12: zWquot#(cons(X,XS),cons(Y,YS)) -> c_12(quot#(X,Y),activate#(XS),activate#(YS)) 13: zWquot#(nil(),XS) -> c_13() * Step 5: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)) activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) zWquot#(cons(X,XS),cons(Y,YS)) -> c_12(quot#(X,Y),activate#(XS),activate#(YS)) - Weak DPs: activate#(X) -> c_1() from#(X) -> c_5() from#(X) -> c_6() minus#(X,0()) -> c_7() s#(X) -> c_8() sel#(0(),cons(X,XS)) -> c_9() zWquot#(X1,X2) -> c_10() zWquot#(XS,nil()) -> c_11() zWquot#(nil(),XS) -> c_13() - Weak TRS: activate(X) -> X activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) zWquot(X1,X2) -> n__zWquot(X1,X2) zWquot(XS,nil()) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) zWquot(nil(),XS) -> nil() - Signature: {activate/1,from/1,minus/2,quot/2,s/1,sel/2,zWquot/2,activate#/1,from#/1,minus#/2,quot#/2,s#/1,sel#/2 ,zWquot#/2} / {0/0,cons/2,n__from/1,n__s/1,n__zWquot/2,nil/0,c_1/0,c_2/2,c_3/2,c_4/3,c_5/0,c_6/0,c_7/0,c_8/0 ,c_9/0,c_10/0,c_11/0,c_12/3,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,from#,minus#,quot#,s#,sel# ,zWquot#} and constructors {0,cons,n__from,n__s,n__zWquot,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)) -->_2 activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)) ,activate#(X1) ,activate#(X2)):3 -->_2 activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)):2 -->_1 from#(X) -> c_6():7 -->_1 from#(X) -> c_5():6 -->_2 activate#(X) -> c_1():5 -->_2 activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)):1 2:S:activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)) -->_2 activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)) ,activate#(X1) ,activate#(X2)):3 -->_1 s#(X) -> c_8():9 -->_2 activate#(X) -> c_1():5 -->_2 activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)):2 -->_2 activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)):1 3:S:activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_1 zWquot#(cons(X,XS),cons(Y,YS)) -> c_12(quot#(X,Y),activate#(XS),activate#(YS)):4 -->_1 zWquot#(nil(),XS) -> c_13():13 -->_1 zWquot#(XS,nil()) -> c_11():12 -->_1 zWquot#(X1,X2) -> c_10():11 -->_3 activate#(X) -> c_1():5 -->_2 activate#(X) -> c_1():5 -->_3 activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_2 activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_3 activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)):2 -->_2 activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)):2 -->_3 activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)):1 -->_2 activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)):1 4:S:zWquot#(cons(X,XS),cons(Y,YS)) -> c_12(quot#(X,Y),activate#(XS),activate#(YS)) -->_3 activate#(X) -> c_1():5 -->_2 activate#(X) -> c_1():5 -->_3 activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_2 activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_3 activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)):2 -->_2 activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)):2 -->_3 activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)):1 -->_2 activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)):1 5:W:activate#(X) -> c_1() 6:W:from#(X) -> c_5() 7:W:from#(X) -> c_6() 8:W:minus#(X,0()) -> c_7() 9:W:s#(X) -> c_8() 10:W:sel#(0(),cons(X,XS)) -> c_9() 11:W:zWquot#(X1,X2) -> c_10() 12:W:zWquot#(XS,nil()) -> c_11() 13:W:zWquot#(nil(),XS) -> c_13() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 10: sel#(0(),cons(X,XS)) -> c_9() 8: minus#(X,0()) -> c_7() 6: from#(X) -> c_5() 7: from#(X) -> c_6() 11: zWquot#(X1,X2) -> c_10() 12: zWquot#(XS,nil()) -> c_11() 13: zWquot#(nil(),XS) -> c_13() 9: s#(X) -> c_8() 5: activate#(X) -> c_1() * Step 6: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)) activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) zWquot#(cons(X,XS),cons(Y,YS)) -> c_12(quot#(X,Y),activate#(XS),activate#(YS)) - Weak TRS: activate(X) -> X activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) zWquot(X1,X2) -> n__zWquot(X1,X2) zWquot(XS,nil()) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) zWquot(nil(),XS) -> nil() - Signature: {activate/1,from/1,minus/2,quot/2,s/1,sel/2,zWquot/2,activate#/1,from#/1,minus#/2,quot#/2,s#/1,sel#/2 ,zWquot#/2} / {0/0,cons/2,n__from/1,n__s/1,n__zWquot/2,nil/0,c_1/0,c_2/2,c_3/2,c_4/3,c_5/0,c_6/0,c_7/0,c_8/0 ,c_9/0,c_10/0,c_11/0,c_12/3,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,from#,minus#,quot#,s#,sel# ,zWquot#} and constructors {0,cons,n__from,n__s,n__zWquot,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)) -->_2 activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)) ,activate#(X1) ,activate#(X2)):3 -->_2 activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)):2 -->_2 activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)):1 2:S:activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)) -->_2 activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)) ,activate#(X1) ,activate#(X2)):3 -->_2 activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)):2 -->_2 activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)):1 3:S:activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_1 zWquot#(cons(X,XS),cons(Y,YS)) -> c_12(quot#(X,Y),activate#(XS),activate#(YS)):4 -->_3 activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_2 activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_3 activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)):2 -->_2 activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)):2 -->_3 activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)):1 -->_2 activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)):1 4:S:zWquot#(cons(X,XS),cons(Y,YS)) -> c_12(quot#(X,Y),activate#(XS),activate#(YS)) -->_3 activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)) ,activate#(X1) ,activate#(X2)):3 -->_2 activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):3 -->_3 activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)):2 -->_2 activate#(n__s(X)) -> c_3(s#(activate(X)),activate#(X)):2 -->_3 activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)):1 -->_2 activate#(n__from(X)) -> c_2(from#(activate(X)),activate#(X)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: activate#(n__from(X)) -> c_2(activate#(X)) activate#(n__s(X)) -> c_3(activate#(X)) zWquot#(cons(X,XS),cons(Y,YS)) -> c_12(activate#(XS),activate#(YS)) * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: activate#(n__from(X)) -> c_2(activate#(X)) activate#(n__s(X)) -> c_3(activate#(X)) activate#(n__zWquot(X1,X2)) -> c_4(zWquot#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) zWquot#(cons(X,XS),cons(Y,YS)) -> c_12(activate#(XS),activate#(YS)) - Weak TRS: activate(X) -> X activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) zWquot(X1,X2) -> n__zWquot(X1,X2) zWquot(XS,nil()) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) zWquot(nil(),XS) -> nil() - Signature: {activate/1,from/1,minus/2,quot/2,s/1,sel/2,zWquot/2,activate#/1,from#/1,minus#/2,quot#/2,s#/1,sel#/2 ,zWquot#/2} / {0/0,cons/2,n__from/1,n__s/1,n__zWquot/2,nil/0,c_1/0,c_2/1,c_3/1,c_4/3,c_5/0,c_6/0,c_7/0,c_8/0 ,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,from#,minus#,quot#,s#,sel# ,zWquot#} and constructors {0,cons,n__from,n__s,n__zWquot,nil} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE