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: Decompose 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: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: quote#(n__s(X)) -> c_17(quote#(activate(X))) - Weak DPs: 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} Problem (S) - Strict DPs: 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 DPs: quote#(n__s(X)) -> c_17(quote#(activate(X))) - 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} ** Step 11.a:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: quote#(n__s(X)) -> c_17(quote#(activate(X))) - Weak DPs: 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: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:quote#(n__s(X)) -> c_17(quote#(activate(X))) -->_1 quote#(n__s(X)) -> c_17(quote#(activate(X))):1 2:W:quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z))) -->_1 quote#(n__s(X)) -> c_17(quote#(activate(X))):1 -->_2 quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z))):2 3:W:unquote#(s1(X)) -> c_25(unquote#(X)) -->_1 unquote#(s1(X)) -> c_25(unquote#(X)):3 4:W:unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) -->_1 unquote#(s1(X)) -> c_25(unquote#(X)):3 -->_2 unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)):4 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 4: unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) 3: unquote#(s1(X)) -> c_25(unquote#(X)) ** Step 11.a:2: Failure MAYBE + Considered Problem: - Strict DPs: quote#(n__s(X)) -> c_17(quote#(activate(X))) - Weak DPs: quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(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. ** Step 11.b:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: 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 DPs: quote#(n__s(X)) -> c_17(quote#(activate(X))) - 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: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z))) -->_1 quote#(n__s(X)) -> c_17(quote#(activate(X))):4 -->_2 quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z))):1 2:S:unquote#(s1(X)) -> c_25(unquote#(X)) -->_1 unquote#(s1(X)) -> c_25(unquote#(X)):2 3:S:unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) -->_2 unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)):3 -->_1 unquote#(s1(X)) -> c_25(unquote#(X)):2 4:W:quote#(n__s(X)) -> c_17(quote#(activate(X))) -->_1 quote#(n__s(X)) -> c_17(quote#(activate(X))):4 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 4: quote#(n__s(X)) -> c_17(quote#(activate(X))) ** Step 11.b:2: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: 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: SimplifyRHS + Details: Consider the dependency graph 1:S:quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z))) -->_2 quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),quote1#(activate(Z))):1 2:S:unquote#(s1(X)) -> c_25(unquote#(X)) -->_1 unquote#(s1(X)) -> c_25(unquote#(X)):2 3:S:unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) -->_2 unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)):3 -->_1 unquote#(s1(X)) -> c_25(unquote#(X)):2 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(Z))) ** Step 11.b:3: Decompose MAYBE + Considered Problem: - Strict DPs: quote1#(n__cons(X,Z)) -> c_19(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/1,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: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(Z))) - Weak DPs: 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/1,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} Problem (S) - Strict DPs: unquote#(s1(X)) -> c_25(unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) - Weak DPs: quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(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/1,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} *** Step 11.b:3.a:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(Z))) - Weak DPs: 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/1,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: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(Z))) -->_1 quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(Z))):1 2:W:unquote#(s1(X)) -> c_25(unquote#(X)) -->_1 unquote#(s1(X)) -> c_25(unquote#(X)):2 3:W:unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) -->_1 unquote#(s1(X)) -> c_25(unquote#(X)):2 -->_2 unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)):3 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) 2: unquote#(s1(X)) -> c_25(unquote#(X)) *** Step 11.b:3.a:2: Failure MAYBE + Considered Problem: - Strict DPs: quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(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/1,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. *** Step 11.b:3.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: unquote#(s1(X)) -> c_25(unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) - Weak DPs: quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(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/1,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: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:unquote#(s1(X)) -> c_25(unquote#(X)) -->_1 unquote#(s1(X)) -> c_25(unquote#(X)):1 2:S:unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) -->_2 unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)):2 -->_1 unquote#(s1(X)) -> c_25(unquote#(X)):1 3:W:quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(Z))) -->_1 quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(Z))):3 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: quote1#(n__cons(X,Z)) -> c_19(quote1#(activate(Z))) *** Step 11.b:3.b:2: Decompose WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: 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/1,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: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: unquote#(s1(X)) -> c_25(unquote#(X)) - Weak DPs: 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/1,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} Problem (S) - Strict DPs: unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) - Weak DPs: unquote#(s1(X)) -> c_25(unquote#(X)) - 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/1,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} **** Step 11.b:3.b:2.a:1: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: unquote#(s1(X)) -> c_25(unquote#(X)) - Weak DPs: 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/1,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: unquote#(s1(X)) -> c_25(unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) **** Step 11.b:3.b:2.a:2: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: unquote#(s1(X)) -> c_25(unquote#(X)) - Weak DPs: unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) - 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/1,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: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: unquote#(s1(X)) -> c_25(unquote#(X)) The strictly oriented rules are moved into the weak component. ***** Step 11.b:3.b:2.a:2.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: unquote#(s1(X)) -> c_25(unquote#(X)) - Weak DPs: unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) - 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/1,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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_25) = {1}, uargs(c_26) = {1,2} Following symbols are considered usable: {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} TcT has computed the following interpretation: p(0) = [0] p(01) = [0] p(activate) = [0] p(cons) = [0] p(cons1) = [1] x1 + [1] x2 + [3] p(fcons) = [0] p(first) = [0] p(first1) = [0] p(from) = [0] p(n__0) = [0] p(n__cons) = [1] x1 + [1] x2 + [0] p(n__first) = [1] x1 + [1] x2 + [0] p(n__from) = [1] x1 + [0] p(n__nil) = [0] p(n__s) = [0] p(n__sel) = [1] x1 + [1] p(nil) = [0] p(nil1) = [1] p(quote) = [1] p(quote1) = [1] x1 + [8] p(s) = [1] p(s1) = [1] x1 + [2] p(sel) = [2] x1 + [2] x2 + [0] p(sel1) = [0] p(unquote) = [8] p(unquote1) = [8] x1 + [1] p(0#) = [0] p(activate#) = [1] x1 + [8] p(cons#) = [0] p(fcons#) = [2] p(first#) = [0] p(first1#) = [1] x1 + [1] x2 + [0] p(from#) = [0] p(nil#) = [2] p(quote#) = [1] x1 + [1] p(quote1#) = [8] x1 + [0] p(s#) = [1] x1 + [1] p(sel#) = [1] x1 + [1] p(sel1#) = [2] p(unquote#) = [2] x1 + [2] p(unquote1#) = [8] x1 + [0] p(c_1) = [0] p(c_2) = [1] p(c_3) = [8] x1 + [1] p(c_4) = [1] x1 + [1] p(c_5) = [1] x1 + [0] p(c_6) = [1] x1 + [0] p(c_7) = [1] x1 + [0] p(c_8) = [1] x1 + [0] p(c_9) = [0] p(c_10) = [2] p(c_11) = [0] p(c_12) = [0] p(c_13) = [4] x1 + [1] x2 + [1] p(c_14) = [1] p(c_15) = [2] p(c_16) = [0] p(c_17) = [1] p(c_18) = [1] x3 + [1] p(c_19) = [0] p(c_20) = [4] x1 + [4] x2 + [1] x3 + [0] p(c_21) = [1] p(c_22) = [0] p(c_23) = [4] p(c_24) = [0] p(c_25) = [1] x1 + [2] p(c_26) = [4] x1 + [1] x2 + [11] p(c_27) = [1] x1 + [0] Following rules are strictly oriented: unquote#(s1(X)) = [2] X + [6] > [2] X + [4] = c_25(unquote#(X)) Following rules are (at-least) weakly oriented: unquote1#(cons1(X,Z)) = [8] X + [8] Z + [24] >= [8] X + [8] Z + [19] = c_26(unquote#(X),unquote1#(Z)) ***** Step 11.b:3.b:2.a:2.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: unquote#(s1(X)) -> c_25(unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) - 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/1,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: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ***** Step 11.b:3.b:2.a:2.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: unquote#(s1(X)) -> c_25(unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) - 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/1,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: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:unquote#(s1(X)) -> c_25(unquote#(X)) -->_1 unquote#(s1(X)) -> c_25(unquote#(X)):1 2:W:unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) -->_2 unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)):2 -->_1 unquote#(s1(X)) -> c_25(unquote#(X)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) 1: unquote#(s1(X)) -> c_25(unquote#(X)) ***** Step 11.b:3.b:2.a:2.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - 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/1,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 already closed. The intended complexity is O(1). **** Step 11.b:3.b:2.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) - Weak DPs: unquote#(s1(X)) -> c_25(unquote#(X)) - 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/1,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: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) -->_1 unquote#(s1(X)) -> c_25(unquote#(X)):2 -->_2 unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)):1 2:W:unquote#(s1(X)) -> c_25(unquote#(X)) -->_1 unquote#(s1(X)) -> c_25(unquote#(X)):2 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: unquote#(s1(X)) -> c_25(unquote#(X)) **** Step 11.b:3.b:2.b:2: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: 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/1,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: SimplifyRHS + Details: Consider the dependency graph 1:S:unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) -->_2 unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z)) **** Step 11.b:3.b:2.b:3: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: unquote1#(cons1(X,Z)) -> c_26(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/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/1,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: unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z)) **** Step 11.b:3.b:2.b:4: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z)) - 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/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/1,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: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z)) The strictly oriented rules are moved into the weak component. ***** Step 11.b:3.b:2.b:4.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z)) - 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/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/1,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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_26) = {1} Following symbols are considered usable: {0#,activate#,cons#,fcons#,first#,first1#,from#,nil#,quote#,quote1#,s#,sel#,sel1#,unquote#,unquote1#} TcT has computed the following interpretation: p(0) = [0] p(01) = [0] p(activate) = [0] p(cons) = [0] p(cons1) = [1] x2 + [8] p(fcons) = [0] p(first) = [0] p(first1) = [0] p(from) = [0] p(n__0) = [1] p(n__cons) = [1] x1 + [1] x2 + [1] p(n__first) = [1] p(n__from) = [1] x1 + [1] p(n__nil) = [2] p(n__s) = [0] p(n__sel) = [2] p(nil) = [1] p(nil1) = [0] p(quote) = [1] x1 + [2] p(quote1) = [1] p(s) = [1] p(s1) = [1] x1 + [2] p(sel) = [1] p(sel1) = [0] p(unquote) = [0] p(unquote1) = [0] p(0#) = [0] p(activate#) = [0] p(cons#) = [0] p(fcons#) = [0] p(first#) = [0] p(first1#) = [0] p(from#) = [0] p(nil#) = [0] p(quote#) = [0] p(quote1#) = [0] p(s#) = [0] p(sel#) = [0] p(sel1#) = [0] p(unquote#) = [0] p(unquote1#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [8] x1 + [0] p(c_4) = [2] x1 + [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [2] x1 + [0] p(c_8) = [1] x1 + [4] p(c_9) = [0] p(c_10) = [2] p(c_11) = [8] p(c_12) = [1] p(c_13) = [4] p(c_14) = [2] p(c_15) = [0] p(c_16) = [0] p(c_17) = [2] x1 + [1] p(c_18) = [2] x1 + [1] x2 + [1] p(c_19) = [2] x1 + [1] p(c_20) = [1] x1 + [1] x2 + [1] x3 + [1] p(c_21) = [0] p(c_22) = [1] p(c_23) = [1] p(c_24) = [1] p(c_25) = [2] x1 + [1] p(c_26) = [1] x1 + [4] p(c_27) = [1] x1 + [0] Following rules are strictly oriented: unquote1#(cons1(X,Z)) = [1] Z + [8] > [1] Z + [4] = c_26(unquote1#(Z)) Following rules are (at-least) weakly oriented: ***** Step 11.b:3.b:2.b:4.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z)) - 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/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/1,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: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ***** Step 11.b:3.b:2.b:4.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z)) - 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/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/1,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:W:unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z)) -->_1 unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: unquote1#(cons1(X,Z)) -> c_26(unquote1#(Z)) ***** Step 11.b:3.b:2.b:4.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - 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/1,c_20/3,c_21/0,c_22/0,c_23/0,c_24/1,c_25/1,c_26/1,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 already closed. The intended complexity is O(1). MAYBE