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__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) cons(X1,X2) -> n__cons(X1,X2) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) first1(0(),Z) -> nil1() first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,activate(Z))) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) nil() -> n__nil() quote(n__0()) -> 01() quote(n__s(X)) -> s1(quote(activate(X))) quote(n__sel(X,Z)) -> sel1(activate(X),activate(Z)) quote1(n__cons(X,Z)) -> cons1(quote(activate(X)),quote1(activate(Z))) quote1(n__first(X,Z)) -> first1(activate(X),activate(Z)) quote1(n__nil()) -> nil1() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) sel(0(),cons(X,Z)) -> X sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) sel1(0(),cons(X,Z)) -> quote(X) sel1(s(X),cons(Y,Z)) -> sel1(X,activate(Z)) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() - Signature: {0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1 ,unquote1/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0,n__s/1,n__sel/2,nil1/0,s1/1} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,cons,fcons,first,first1,from,nil,quote,quote1 ,s,sel,sel1,unquote,unquote1} and constructors {01,cons1,n__0,n__cons,n__first,n__from,n__nil,n__s,n__sel ,nil1,s1} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. first(0(),Z) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) first1(0(),Z) -> nil1() first1(s(X),cons(Y,Z)) -> cons1(quote(Y),first1(X,activate(Z))) sel(0(),cons(X,Z)) -> X sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) sel1(0(),cons(X,Z)) -> quote(X) sel1(s(X),cons(Y,Z)) -> sel1(X,activate(Z)) All above mentioned rules can be savely removed. * Step 2: DependencyPairs 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__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) cons(X1,X2) -> n__cons(X1,X2) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) nil() -> n__nil() quote(n__0()) -> 01() quote(n__s(X)) -> s1(quote(activate(X))) quote(n__sel(X,Z)) -> sel1(activate(X),activate(Z)) quote1(n__cons(X,Z)) -> cons1(quote(activate(X)),quote1(activate(Z))) quote1(n__first(X,Z)) -> first1(activate(X),activate(Z)) quote1(n__nil()) -> nil1() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() - Signature: {0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1 ,unquote1/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0,n__s/1,n__sel/2,nil1/0,s1/1} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,cons,fcons,first,first1,from,nil,quote,quote1 ,s,sel,sel1,unquote,unquote1} and constructors {01,cons1,n__0,n__cons,n__first,n__from,n__nil,n__s,n__sel ,nil1,s1} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs 0#() -> c_1() activate#(X) -> c_2() activate#(n__0()) -> c_3(0#()) activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)) activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)) activate#(n__from(X)) -> c_6(from#(X)) activate#(n__nil()) -> c_7(nil#()) activate#(n__s(X)) -> c_8(s#(X)) activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)) cons#(X1,X2) -> c_10() fcons#(X,Z) -> c_11(cons#(X,Z)) first#(X1,X2) -> c_12() from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X)) from#(X) -> c_14() nil#() -> c_15() quote#(n__0()) -> c_16() quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)) quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)) quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)) quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z)) quote1#(n__nil()) -> c_21() s#(X) -> c_22() sel#(X1,X2) -> c_23() unquote#(01()) -> c_24(0#()) unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) unquote1#(nil1()) -> c_27(nil#()) Weak DPs and mark the set of starting terms. * Step 3: UsableRules MAYBE + Considered Problem: - Strict DPs: 0#() -> c_1() activate#(X) -> c_2() activate#(n__0()) -> c_3(0#()) activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)) activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)) activate#(n__from(X)) -> c_6(from#(X)) activate#(n__nil()) -> c_7(nil#()) activate#(n__s(X)) -> c_8(s#(X)) activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)) cons#(X1,X2) -> c_10() fcons#(X,Z) -> c_11(cons#(X,Z)) first#(X1,X2) -> c_12() from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X)) from#(X) -> c_14() nil#() -> c_15() quote#(n__0()) -> c_16() quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)) quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)) quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)) quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z)) quote1#(n__nil()) -> c_21() s#(X) -> c_22() sel#(X1,X2) -> c_23() unquote#(01()) -> c_24(0#()) unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) unquote1#(nil1()) -> c_27(nil#()) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) cons(X1,X2) -> n__cons(X1,X2) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) nil() -> n__nil() quote(n__0()) -> 01() quote(n__s(X)) -> s1(quote(activate(X))) quote(n__sel(X,Z)) -> sel1(activate(X),activate(Z)) quote1(n__cons(X,Z)) -> cons1(quote(activate(X)),quote1(activate(Z))) quote1(n__first(X,Z)) -> first1(activate(X),activate(Z)) quote1(n__nil()) -> nil1() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() - Signature: {0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1 ,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1 ,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0 ,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0 ,c_13/2,c_14/0,c_15/0,c_16/0,c_17/2,c_18/3,c_19/4,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/2,c_26/3,c_27/1} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil# ,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from ,n__nil,n__s,n__sel,nil1,s1} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) cons(X1,X2) -> n__cons(X1,X2) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) nil() -> n__nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() 0#() -> c_1() activate#(X) -> c_2() activate#(n__0()) -> c_3(0#()) activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)) activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)) activate#(n__from(X)) -> c_6(from#(X)) activate#(n__nil()) -> c_7(nil#()) activate#(n__s(X)) -> c_8(s#(X)) activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)) cons#(X1,X2) -> c_10() fcons#(X,Z) -> c_11(cons#(X,Z)) first#(X1,X2) -> c_12() from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X)) from#(X) -> c_14() nil#() -> c_15() quote#(n__0()) -> c_16() quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)) quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)) quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)) quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z)) quote1#(n__nil()) -> c_21() s#(X) -> c_22() sel#(X1,X2) -> c_23() unquote#(01()) -> c_24(0#()) unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) unquote1#(nil1()) -> c_27(nil#()) * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: 0#() -> c_1() activate#(X) -> c_2() activate#(n__0()) -> c_3(0#()) activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)) activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)) activate#(n__from(X)) -> c_6(from#(X)) activate#(n__nil()) -> c_7(nil#()) activate#(n__s(X)) -> c_8(s#(X)) activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)) cons#(X1,X2) -> c_10() fcons#(X,Z) -> c_11(cons#(X,Z)) first#(X1,X2) -> c_12() from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X)) from#(X) -> c_14() nil#() -> c_15() quote#(n__0()) -> c_16() quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)) quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)) quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)) quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z)) quote1#(n__nil()) -> c_21() s#(X) -> c_22() sel#(X1,X2) -> c_23() unquote#(01()) -> c_24(0#()) unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) unquote1#(nil1()) -> c_27(nil#()) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) cons(X1,X2) -> n__cons(X1,X2) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) nil() -> n__nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() - Signature: {0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1 ,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1 ,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0 ,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0 ,c_13/2,c_14/0,c_15/0,c_16/0,c_17/2,c_18/3,c_19/4,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/2,c_26/3,c_27/1} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil# ,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from ,n__nil,n__s,n__sel,nil1,s1} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,10,12,14,15,16,21,22,23} by application of Pre({1,2,10,12,14,15,16,21,22,23}) = {3,4,5,6,7,8,9,11,13,17,18,19,20,24,25,27}. Here rules are labelled as follows: 1: 0#() -> c_1() 2: activate#(X) -> c_2() 3: activate#(n__0()) -> c_3(0#()) 4: activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)) 5: activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)) 6: activate#(n__from(X)) -> c_6(from#(X)) 7: activate#(n__nil()) -> c_7(nil#()) 8: activate#(n__s(X)) -> c_8(s#(X)) 9: activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)) 10: cons#(X1,X2) -> c_10() 11: fcons#(X,Z) -> c_11(cons#(X,Z)) 12: first#(X1,X2) -> c_12() 13: from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X)) 14: from#(X) -> c_14() 15: nil#() -> c_15() 16: quote#(n__0()) -> c_16() 17: quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)) 18: quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)) 19: quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)) 20: quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z)) 21: quote1#(n__nil()) -> c_21() 22: s#(X) -> c_22() 23: sel#(X1,X2) -> c_23() 24: unquote#(01()) -> c_24(0#()) 25: unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)) 26: unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) 27: unquote1#(nil1()) -> c_27(nil#()) * Step 5: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(n__0()) -> c_3(0#()) activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)) activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)) activate#(n__from(X)) -> c_6(from#(X)) activate#(n__nil()) -> c_7(nil#()) activate#(n__s(X)) -> c_8(s#(X)) activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)) fcons#(X,Z) -> c_11(cons#(X,Z)) from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X)) quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)) quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)) quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)) quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z)) unquote#(01()) -> c_24(0#()) unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) unquote1#(nil1()) -> c_27(nil#()) - Weak DPs: 0#() -> c_1() activate#(X) -> c_2() cons#(X1,X2) -> c_10() first#(X1,X2) -> c_12() from#(X) -> c_14() nil#() -> c_15() quote#(n__0()) -> c_16() quote1#(n__nil()) -> c_21() s#(X) -> c_22() sel#(X1,X2) -> c_23() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) cons(X1,X2) -> n__cons(X1,X2) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) nil() -> n__nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() - Signature: {0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1 ,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1 ,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0 ,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0 ,c_13/2,c_14/0,c_15/0,c_16/0,c_17/2,c_18/3,c_19/4,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/2,c_26/3,c_27/1} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil# ,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from ,n__nil,n__s,n__sel,nil1,s1} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,5,6,7,8,9,14,17} by application of Pre({1,2,3,5,6,7,8,9,14,17}) = {4,10,11,12,13,15,16}. Here rules are labelled as follows: 1: activate#(n__0()) -> c_3(0#()) 2: activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)) 3: activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)) 4: activate#(n__from(X)) -> c_6(from#(X)) 5: activate#(n__nil()) -> c_7(nil#()) 6: activate#(n__s(X)) -> c_8(s#(X)) 7: activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)) 8: fcons#(X,Z) -> c_11(cons#(X,Z)) 9: from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X)) 10: quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)) 11: quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)) 12: quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)) 13: quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z)) 14: unquote#(01()) -> c_24(0#()) 15: unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)) 16: unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) 17: unquote1#(nil1()) -> c_27(nil#()) 18: 0#() -> c_1() 19: activate#(X) -> c_2() 20: cons#(X1,X2) -> c_10() 21: first#(X1,X2) -> c_12() 22: from#(X) -> c_14() 23: nil#() -> c_15() 24: quote#(n__0()) -> c_16() 25: quote1#(n__nil()) -> c_21() 26: s#(X) -> c_22() 27: sel#(X1,X2) -> c_23() * Step 6: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(n__from(X)) -> c_6(from#(X)) quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)) quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)) quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)) quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z)) unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) - Weak DPs: 0#() -> c_1() activate#(X) -> c_2() activate#(n__0()) -> c_3(0#()) activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)) activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)) activate#(n__nil()) -> c_7(nil#()) activate#(n__s(X)) -> c_8(s#(X)) activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)) cons#(X1,X2) -> c_10() fcons#(X,Z) -> c_11(cons#(X,Z)) first#(X1,X2) -> c_12() from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X)) from#(X) -> c_14() nil#() -> c_15() quote#(n__0()) -> c_16() quote1#(n__nil()) -> c_21() s#(X) -> c_22() sel#(X1,X2) -> c_23() unquote#(01()) -> c_24(0#()) unquote1#(nil1()) -> c_27(nil#()) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) cons(X1,X2) -> n__cons(X1,X2) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) nil() -> n__nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() - Signature: {0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1 ,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1 ,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0 ,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0 ,c_13/2,c_14/0,c_15/0,c_16/0,c_17/2,c_18/3,c_19/4,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/2,c_26/3,c_27/1} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil# ,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from ,n__nil,n__s,n__sel,nil1,s1} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1} by application of Pre({1}) = {2,3,4,5}. Here rules are labelled as follows: 1: activate#(n__from(X)) -> c_6(from#(X)) 2: quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)) 3: quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)) 4: quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)) 5: quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z)) 6: unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)) 7: unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) 8: 0#() -> c_1() 9: activate#(X) -> c_2() 10: activate#(n__0()) -> c_3(0#()) 11: activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)) 12: activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)) 13: activate#(n__nil()) -> c_7(nil#()) 14: activate#(n__s(X)) -> c_8(s#(X)) 15: activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)) 16: cons#(X1,X2) -> c_10() 17: fcons#(X,Z) -> c_11(cons#(X,Z)) 18: first#(X1,X2) -> c_12() 19: from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X)) 20: from#(X) -> c_14() 21: nil#() -> c_15() 22: quote#(n__0()) -> c_16() 23: quote1#(n__nil()) -> c_21() 24: s#(X) -> c_22() 25: sel#(X1,X2) -> c_23() 26: unquote#(01()) -> c_24(0#()) 27: unquote1#(nil1()) -> c_27(nil#()) * Step 7: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)) quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)) quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)) quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z)) unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) - Weak DPs: 0#() -> c_1() activate#(X) -> c_2() activate#(n__0()) -> c_3(0#()) activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)) activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)) activate#(n__from(X)) -> c_6(from#(X)) activate#(n__nil()) -> c_7(nil#()) activate#(n__s(X)) -> c_8(s#(X)) activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)) cons#(X1,X2) -> c_10() fcons#(X,Z) -> c_11(cons#(X,Z)) first#(X1,X2) -> c_12() from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X)) from#(X) -> c_14() nil#() -> c_15() quote#(n__0()) -> c_16() quote1#(n__nil()) -> c_21() s#(X) -> c_22() sel#(X1,X2) -> c_23() unquote#(01()) -> c_24(0#()) unquote1#(nil1()) -> c_27(nil#()) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) cons(X1,X2) -> n__cons(X1,X2) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) nil() -> n__nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() - Signature: {0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1 ,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1 ,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0 ,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0 ,c_13/2,c_14/0,c_15/0,c_16/0,c_17/2,c_18/3,c_19/4,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/2,c_26/3,c_27/1} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil# ,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from ,n__nil,n__s,n__sel,nil1,s1} + 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}) = {1,3}. Here rules are labelled as follows: 1: quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)) 2: quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)) 3: quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)) 4: quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z)) 5: unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)) 6: unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) 7: 0#() -> c_1() 8: activate#(X) -> c_2() 9: activate#(n__0()) -> c_3(0#()) 10: activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)) 11: activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)) 12: activate#(n__from(X)) -> c_6(from#(X)) 13: activate#(n__nil()) -> c_7(nil#()) 14: activate#(n__s(X)) -> c_8(s#(X)) 15: activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)) 16: cons#(X1,X2) -> c_10() 17: fcons#(X,Z) -> c_11(cons#(X,Z)) 18: first#(X1,X2) -> c_12() 19: from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X)) 20: from#(X) -> c_14() 21: nil#() -> c_15() 22: quote#(n__0()) -> c_16() 23: quote1#(n__nil()) -> c_21() 24: s#(X) -> c_22() 25: sel#(X1,X2) -> c_23() 26: unquote#(01()) -> c_24(0#()) 27: unquote1#(nil1()) -> c_27(nil#()) * Step 8: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)) quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)) unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) - Weak DPs: 0#() -> c_1() activate#(X) -> c_2() activate#(n__0()) -> c_3(0#()) activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)) activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)) activate#(n__from(X)) -> c_6(from#(X)) activate#(n__nil()) -> c_7(nil#()) activate#(n__s(X)) -> c_8(s#(X)) activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)) cons#(X1,X2) -> c_10() fcons#(X,Z) -> c_11(cons#(X,Z)) first#(X1,X2) -> c_12() from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X)) from#(X) -> c_14() nil#() -> c_15() quote#(n__0()) -> c_16() quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)) quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z)) quote1#(n__nil()) -> c_21() s#(X) -> c_22() sel#(X1,X2) -> c_23() unquote#(01()) -> c_24(0#()) unquote1#(nil1()) -> c_27(nil#()) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) cons(X1,X2) -> n__cons(X1,X2) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) nil() -> n__nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() - Signature: {0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1 ,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1 ,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0 ,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0 ,c_13/2,c_14/0,c_15/0,c_16/0,c_17/2,c_18/3,c_19/4,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/2,c_26/3,c_27/1} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil# ,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from ,n__nil,n__s,n__sel,nil1,s1} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)) -->_1 quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)):21 -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)):13 -->_2 activate#(n__s(X)) -> c_8(s#(X)):12 -->_2 activate#(n__nil()) -> c_7(nil#()):11 -->_2 activate#(n__from(X)) -> c_6(from#(X)):10 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)):9 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)):8 -->_2 activate#(n__0()) -> c_3(0#()):7 -->_1 quote#(n__0()) -> c_16():20 -->_2 activate#(X) -> c_2():6 -->_1 quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)):1 2:S:quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)) -->_3 quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z)):22 -->_1 quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)):21 -->_4 activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)):13 -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)):13 -->_4 activate#(n__s(X)) -> c_8(s#(X)):12 -->_2 activate#(n__s(X)) -> c_8(s#(X)):12 -->_4 activate#(n__nil()) -> c_7(nil#()):11 -->_2 activate#(n__nil()) -> c_7(nil#()):11 -->_4 activate#(n__from(X)) -> c_6(from#(X)):10 -->_2 activate#(n__from(X)) -> c_6(from#(X)):10 -->_4 activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)):9 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)):9 -->_4 activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)):8 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)):8 -->_4 activate#(n__0()) -> c_3(0#()):7 -->_2 activate#(n__0()) -> c_3(0#()):7 -->_3 quote1#(n__nil()) -> c_21():23 -->_1 quote#(n__0()) -> c_16():20 -->_4 activate#(X) -> c_2():6 -->_2 activate#(X) -> c_2():6 -->_3 quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)):2 -->_1 quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)):1 3:S:unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)) -->_2 unquote#(01()) -> c_24(0#()):26 -->_1 s#(X) -> c_22():24 -->_2 unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)):3 4:S:unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) -->_3 unquote1#(nil1()) -> c_27(nil#()):27 -->_2 unquote#(01()) -> c_24(0#()):26 -->_1 fcons#(X,Z) -> c_11(cons#(X,Z)):15 -->_3 unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)):4 -->_2 unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)):3 5:W:0#() -> c_1() 6:W:activate#(X) -> c_2() 7:W:activate#(n__0()) -> c_3(0#()) -->_1 0#() -> c_1():5 8:W:activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)) -->_1 cons#(X1,X2) -> c_10():14 9:W:activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)) -->_1 first#(X1,X2) -> c_12():16 10:W:activate#(n__from(X)) -> c_6(from#(X)) -->_1 from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X)):17 -->_1 from#(X) -> c_14():18 11:W:activate#(n__nil()) -> c_7(nil#()) -->_1 nil#() -> c_15():19 12:W:activate#(n__s(X)) -> c_8(s#(X)) -->_1 s#(X) -> c_22():24 13:W:activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)) -->_1 sel#(X1,X2) -> c_23():25 14:W:cons#(X1,X2) -> c_10() 15:W:fcons#(X,Z) -> c_11(cons#(X,Z)) -->_1 cons#(X1,X2) -> c_10():14 16:W:first#(X1,X2) -> c_12() 17:W:from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X)) -->_2 s#(X) -> c_22():24 -->_1 cons#(X1,X2) -> c_10():14 18:W:from#(X) -> c_14() 19:W:nil#() -> c_15() 20:W:quote#(n__0()) -> c_16() 21:W:quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)) -->_3 activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)):13 -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)):13 -->_3 activate#(n__s(X)) -> c_8(s#(X)):12 -->_2 activate#(n__s(X)) -> c_8(s#(X)):12 -->_3 activate#(n__nil()) -> c_7(nil#()):11 -->_2 activate#(n__nil()) -> c_7(nil#()):11 -->_3 activate#(n__from(X)) -> c_6(from#(X)):10 -->_2 activate#(n__from(X)) -> c_6(from#(X)):10 -->_3 activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)):9 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)):9 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)):8 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)):8 -->_3 activate#(n__0()) -> c_3(0#()):7 -->_2 activate#(n__0()) -> c_3(0#()):7 -->_3 activate#(X) -> c_2():6 -->_2 activate#(X) -> c_2():6 22:W:quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z)) -->_3 activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)):13 -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)):13 -->_3 activate#(n__s(X)) -> c_8(s#(X)):12 -->_2 activate#(n__s(X)) -> c_8(s#(X)):12 -->_3 activate#(n__nil()) -> c_7(nil#()):11 -->_2 activate#(n__nil()) -> c_7(nil#()):11 -->_3 activate#(n__from(X)) -> c_6(from#(X)):10 -->_2 activate#(n__from(X)) -> c_6(from#(X)):10 -->_3 activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)):9 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)):9 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)):8 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)):8 -->_3 activate#(n__0()) -> c_3(0#()):7 -->_2 activate#(n__0()) -> c_3(0#()):7 -->_3 activate#(X) -> c_2():6 -->_2 activate#(X) -> c_2():6 23:W:quote1#(n__nil()) -> c_21() 24:W:s#(X) -> c_22() 25:W:sel#(X1,X2) -> c_23() 26:W:unquote#(01()) -> c_24(0#()) -->_1 0#() -> c_1():5 27:W:unquote1#(nil1()) -> c_27(nil#()) -->_1 nil#() -> c_15():19 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 15: fcons#(X,Z) -> c_11(cons#(X,Z)) 27: unquote1#(nil1()) -> c_27(nil#()) 26: unquote#(01()) -> c_24(0#()) 23: quote1#(n__nil()) -> c_21() 22: quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z)) 20: quote#(n__0()) -> c_16() 21: quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)) 6: activate#(X) -> c_2() 7: activate#(n__0()) -> c_3(0#()) 5: 0#() -> c_1() 8: activate#(n__cons(X1,X2)) -> c_4(cons#(X1,X2)) 9: activate#(n__first(X1,X2)) -> c_5(first#(X1,X2)) 16: first#(X1,X2) -> c_12() 10: activate#(n__from(X)) -> c_6(from#(X)) 18: from#(X) -> c_14() 17: from#(X) -> c_13(cons#(X,n__from(s(X))),s#(X)) 14: cons#(X1,X2) -> c_10() 11: activate#(n__nil()) -> c_7(nil#()) 19: nil#() -> c_15() 12: activate#(n__s(X)) -> c_8(s#(X)) 24: s#(X) -> c_22() 13: activate#(n__sel(X1,X2)) -> c_9(sel#(X1,X2)) 25: sel#(X1,X2) -> c_23() * Step 9: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)) quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)) unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) cons(X1,X2) -> n__cons(X1,X2) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) nil() -> n__nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() - Signature: {0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1 ,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1 ,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0 ,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0 ,c_13/2,c_14/0,c_15/0,c_16/0,c_17/2,c_18/3,c_19/4,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/2,c_26/3,c_27/1} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil# ,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from ,n__nil,n__s,n__sel,nil1,s1} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)) -->_1 quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)):1 2:S:quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)) -->_3 quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)):2 -->_1 quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)):1 3:S:unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)) -->_2 unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)):3 4:S:unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)) -->_3 unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)):4 -->_2 unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: quote#(n__s(X)) -> c_17(quote#(activate(X))) quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z))) unquote#(s1(X)) -> c_25(unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) * Step 10: UsableRules MAYBE + Considered Problem: - Strict DPs: quote#(n__s(X)) -> c_17(quote#(activate(X))) quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z))) unquote#(s1(X)) -> c_25(unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) cons(X1,X2) -> n__cons(X1,X2) fcons(X,Z) -> cons(X,Z) first(X1,X2) -> n__first(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) nil() -> n__nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) unquote(01()) -> 0() unquote(s1(X)) -> s(unquote(X)) unquote1(cons1(X,Z)) -> fcons(unquote(X),unquote1(Z)) unquote1(nil1()) -> nil() - Signature: {0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1 ,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1 ,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0 ,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0 ,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/2,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil# ,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from ,n__nil,n__s,n__sel,nil1,s1} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) cons(X1,X2) -> n__cons(X1,X2) first(X1,X2) -> n__first(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) nil() -> n__nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) quote#(n__s(X)) -> c_17(quote#(activate(X))) quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z))) unquote#(s1(X)) -> c_25(unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) * Step 11: Failure MAYBE + Considered Problem: - Strict DPs: quote#(n__s(X)) -> c_17(quote#(activate(X))) quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z))) unquote#(s1(X)) -> c_25(unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__sel(X1,X2)) -> sel(X1,X2) cons(X1,X2) -> n__cons(X1,X2) first(X1,X2) -> n__first(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) nil() -> n__nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) - Signature: {0/0,activate/1,cons/2,fcons/2,first/2,first1/2,from/1,nil/0,quote/1,quote1/1,s/1,sel/2,sel1/2,unquote/1 ,unquote1/1,0#/0,activate#/1,cons#/2,fcons#/2,first#/2,first1#/2,from#/1,nil#/0,quote#/1,quote1#/1,s#/1 ,sel#/2,sel1#/2,unquote#/1,unquote1#/1} / {01/0,cons1/2,n__0/0,n__cons/2,n__first/2,n__from/1,n__nil/0 ,n__s/1,n__sel/2,nil1/0,s1/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/1,c_12/0 ,c_13/2,c_14/0,c_15/0,c_16/0,c_17/1,c_18/3,c_19/2,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/2,c_27/1} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,cons#,fcons#,first#,first1#,from#,nil# ,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} and constructors {01,cons1,n__0,n__cons,n__first,n__from ,n__nil,n__s,n__sel,nil1,s1} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE