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(activate(X1),X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(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(n__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(activate(X1),X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(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(n__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#(activate(X1),X2),activate#(X1)) activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)) activate#(n__nil()) -> c_7(nil#()) activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(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(n__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#(activate(X1),X2),activate#(X1)) activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)) activate#(n__nil()) -> c_7(nil#()) activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(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(n__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(activate(X1),X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(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(n__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/2,c_5/3,c_6/2,c_7/1,c_8/2,c_9/3,c_10/0,c_11/1,c_12/0 ,c_13/1,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(activate(X1),X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(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(n__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#(activate(X1),X2),activate#(X1)) activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)) activate#(n__nil()) -> c_7(nil#()) activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(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(n__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#(activate(X1),X2),activate#(X1)) activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)) activate#(n__nil()) -> c_7(nil#()) activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(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(n__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(activate(X1),X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(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(n__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/2,c_5/3,c_6/2,c_7/1,c_8/2,c_9/3,c_10/0,c_11/1,c_12/0 ,c_13/1,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#(activate(X1),X2),activate#(X1)) 5: activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 6: activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)) 7: activate#(n__nil()) -> c_7(nil#()) 8: activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) 9: activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(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(n__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#(activate(X1),X2),activate#(X1)) activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)) activate#(n__nil()) -> c_7(nil#()) activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) fcons#(X,Z) -> c_11(cons#(X,Z)) from#(X) -> c_13(cons#(X,n__from(n__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(activate(X1),X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(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(n__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/2,c_5/3,c_6/2,c_7/1,c_8/2,c_9/3,c_10/0,c_11/1,c_12/0 ,c_13/1,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,5,8,9,14,17} by application of Pre({1,5,8,9,14,17}) = {2,3,4,6,7,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#(activate(X1),X2),activate#(X1)) 3: activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 4: activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)) 5: activate#(n__nil()) -> c_7(nil#()) 6: activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) 7: activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 8: fcons#(X,Z) -> c_11(cons#(X,Z)) 9: from#(X) -> c_13(cons#(X,n__from(n__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: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)) activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 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__nil()) -> c_7(nil#()) 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(n__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(activate(X1),X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(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(n__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/2,c_5/3,c_6/2,c_7/1,c_8/2,c_9/3,c_10/0,c_11/1,c_12/0 ,c_13/1,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:activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)) -->_2 activate#(n__nil()) -> c_7(nil#()):15 -->_2 activate#(n__0()) -> c_3(0#()):14 -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_1 cons#(X1,X2) -> c_10():16 -->_2 activate#(X) -> c_2():13 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 2:S:activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__nil()) -> c_7(nil#()):15 -->_2 activate#(n__nil()) -> c_7(nil#()):15 -->_3 activate#(n__0()) -> c_3(0#()):14 -->_2 activate#(n__0()) -> c_3(0#()):14 -->_3 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_3 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_2 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_1 first#(X1,X2) -> c_12():18 -->_3 activate#(X) -> c_2():13 -->_2 activate#(X) -> c_2():13 -->_3 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 3:S:activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)) -->_1 from#(X) -> c_13(cons#(X,n__from(n__s(X)))):19 -->_2 activate#(n__nil()) -> c_7(nil#()):15 -->_2 activate#(n__0()) -> c_3(0#()):14 -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_1 from#(X) -> c_14():20 -->_2 activate#(X) -> c_2():13 -->_2 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 4:S:activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) -->_2 activate#(n__nil()) -> c_7(nil#()):15 -->_2 activate#(n__0()) -> c_3(0#()):14 -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 s#(X) -> c_22():24 -->_2 activate#(X) -> c_2():13 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 5:S:activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__nil()) -> c_7(nil#()):15 -->_2 activate#(n__nil()) -> c_7(nil#()):15 -->_3 activate#(n__0()) -> c_3(0#()):14 -->_2 activate#(n__0()) -> c_3(0#()):14 -->_1 sel#(X1,X2) -> c_23():25 -->_3 activate#(X) -> c_2():13 -->_2 activate#(X) -> c_2():13 -->_3 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_3 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_2 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_3 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 6:S:quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)) -->_2 activate#(n__nil()) -> c_7(nil#()):15 -->_2 activate#(n__0()) -> c_3(0#()):14 -->_1 quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)):7 -->_1 quote#(n__0()) -> c_16():22 -->_2 activate#(X) -> c_2():13 -->_1 quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)):6 -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 7:S:quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)) -->_3 activate#(n__nil()) -> c_7(nil#()):15 -->_2 activate#(n__nil()) -> c_7(nil#()):15 -->_3 activate#(n__0()) -> c_3(0#()):14 -->_2 activate#(n__0()) -> c_3(0#()):14 -->_3 activate#(X) -> c_2():13 -->_2 activate#(X) -> c_2():13 -->_3 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_3 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_2 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_3 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 8:S:quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)) -->_4 activate#(n__nil()) -> c_7(nil#()):15 -->_2 activate#(n__nil()) -> c_7(nil#()):15 -->_4 activate#(n__0()) -> c_3(0#()):14 -->_2 activate#(n__0()) -> c_3(0#()):14 -->_3 quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z)):9 -->_3 quote1#(n__nil()) -> c_21():23 -->_1 quote#(n__0()) -> c_16():22 -->_4 activate#(X) -> c_2():13 -->_2 activate#(X) -> c_2():13 -->_3 quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)):8 -->_1 quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)):7 -->_1 quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)):6 -->_4 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_4 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_4 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_2 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_4 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_4 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 9:S:quote1#(n__first(X,Z)) -> c_20(first1#(activate(X),activate(Z)),activate#(X),activate#(Z)) -->_3 activate#(n__nil()) -> c_7(nil#()):15 -->_2 activate#(n__nil()) -> c_7(nil#()):15 -->_3 activate#(n__0()) -> c_3(0#()):14 -->_2 activate#(n__0()) -> c_3(0#()):14 -->_3 activate#(X) -> c_2():13 -->_2 activate#(X) -> c_2():13 -->_3 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_3 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_2 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_3 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 10: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)):10 11: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)):17 -->_3 unquote1#(cons1(X,Z)) -> c_26(fcons#(unquote(X),unquote1(Z)),unquote#(X),unquote1#(Z)):11 -->_2 unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)):10 12:W:0#() -> c_1() 13:W:activate#(X) -> c_2() 14:W:activate#(n__0()) -> c_3(0#()) -->_1 0#() -> c_1():12 15:W:activate#(n__nil()) -> c_7(nil#()) -->_1 nil#() -> c_15():21 16:W:cons#(X1,X2) -> c_10() 17:W:fcons#(X,Z) -> c_11(cons#(X,Z)) -->_1 cons#(X1,X2) -> c_10():16 18:W:first#(X1,X2) -> c_12() 19:W:from#(X) -> c_13(cons#(X,n__from(n__s(X)))) -->_1 cons#(X1,X2) -> c_10():16 20:W:from#(X) -> c_14() 21:W:nil#() -> c_15() 22:W:quote#(n__0()) -> c_16() 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():12 27:W:unquote1#(nil1()) -> c_27(nil#()) -->_1 nil#() -> c_15():21 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 17: 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: quote#(n__0()) -> c_16() 18: first#(X1,X2) -> c_12() 20: from#(X) -> c_14() 19: from#(X) -> c_13(cons#(X,n__from(n__s(X)))) 16: cons#(X1,X2) -> c_10() 24: s#(X) -> c_22() 13: activate#(X) -> c_2() 25: sel#(X1,X2) -> c_23() 14: activate#(n__0()) -> c_3(0#()) 12: 0#() -> c_1() 15: activate#(n__nil()) -> c_7(nil#()) 21: nil#() -> c_15() * Step 7: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)) activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 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 TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(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(n__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/2,c_5/3,c_6/2,c_7/1,c_8/2,c_9/3,c_10/0,c_11/1,c_12/0 ,c_13/1,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:activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)) -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 2:S:activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_3 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_2 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_3 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 3:S:activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)) -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 4:S:activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)) -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 5:S:activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_3 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_2 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_3 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 6: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)):7 -->_1 quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)):6 -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 7:S: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#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_3 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_2 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_3 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 8: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)):9 -->_3 quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)):8 -->_1 quote#(n__sel(X,Z)) -> c_18(sel1#(activate(X),activate(Z)),activate#(X),activate#(Z)):7 -->_1 quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)):6 -->_4 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_4 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_4 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_2 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_4 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_4 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 9:S: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#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n__sel(X1,X2)) -> c_9(sel#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_2 activate#(n__s(X)) -> c_8(s#(activate(X)),activate#(X)):4 -->_3 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_2 activate#(n__from(X)) -> c_6(from#(activate(X)),activate#(X)):3 -->_3 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_2 activate#(n__first(X1,X2)) -> c_5(first#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):2 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 10:S:unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)) -->_2 unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)):10 11: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)):11 -->_2 unquote#(s1(X)) -> c_25(s#(unquote(X)),unquote#(X)):10 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__first(X1,X2)) -> c_5(activate#(X1),activate#(X2)) activate#(n__from(X)) -> c_6(activate#(X)) activate#(n__s(X)) -> c_8(activate#(X)) activate#(n__sel(X1,X2)) -> c_9(activate#(X1),activate#(X2)) quote#(n__sel(X,Z)) -> c_18(activate#(X),activate#(Z)) quote1#(n__first(X,Z)) -> c_20(activate#(X),activate#(Z)) unquote#(s1(X)) -> c_25(unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) * Step 8: UsableRules MAYBE + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__first(X1,X2)) -> c_5(activate#(X1),activate#(X2)) activate#(n__from(X)) -> c_6(activate#(X)) activate#(n__s(X)) -> c_8(activate#(X)) activate#(n__sel(X1,X2)) -> c_9(activate#(X1),activate#(X2)) quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)) quote#(n__sel(X,Z)) -> c_18(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(activate#(X),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(activate(X1),X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(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(n__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/2,c_6/1,c_7/1,c_8/1,c_9/2,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/0,c_17/2,c_18/2,c_19/4,c_20/2,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(activate(X1),X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) cons(X1,X2) -> n__cons(X1,X2) first(X1,X2) -> n__first(X1,X2) from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) nil() -> n__nil() s(X) -> n__s(X) sel(X1,X2) -> n__sel(X1,X2) activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__first(X1,X2)) -> c_5(activate#(X1),activate#(X2)) activate#(n__from(X)) -> c_6(activate#(X)) activate#(n__s(X)) -> c_8(activate#(X)) activate#(n__sel(X1,X2)) -> c_9(activate#(X1),activate#(X2)) quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)) quote#(n__sel(X,Z)) -> c_18(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(activate#(X),activate#(Z)) unquote#(s1(X)) -> c_25(unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) * Step 9: NaturalMI MAYBE + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__first(X1,X2)) -> c_5(activate#(X1),activate#(X2)) activate#(n__from(X)) -> c_6(activate#(X)) activate#(n__s(X)) -> c_8(activate#(X)) activate#(n__sel(X1,X2)) -> c_9(activate#(X1),activate#(X2)) quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)) quote#(n__sel(X,Z)) -> c_18(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(activate#(X),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(activate(X1),X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) cons(X1,X2) -> n__cons(X1,X2) first(X1,X2) -> n__first(X1,X2) from(X) -> cons(X,n__from(n__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/2,c_6/1,c_7/1,c_8/1,c_9/2,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/0,c_17/2,c_18/2,c_19/4,c_20/2,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 = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_4) = {1}, uargs(c_5) = {1,2}, uargs(c_6) = {1}, uargs(c_8) = {1}, uargs(c_9) = {1,2}, uargs(c_17) = {1,2}, uargs(c_18) = {1,2}, uargs(c_19) = {1,2,3,4}, uargs(c_20) = {1,2}, 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) = [1] p(activate) = [2] p(cons) = [2] x1 + [5] x2 + [3] p(cons1) = [0] p(fcons) = [1] x2 + [0] p(first) = [4] x2 + [0] p(first1) = [1] p(from) = [2] p(n__0) = [1] p(n__cons) = [0] p(n__first) = [0] p(n__from) = [1] p(n__nil) = [0] p(n__s) = [4] p(n__sel) = [0] p(nil) = [1] p(nil1) = [1] p(quote) = [1] x1 + [2] p(quote1) = [2] x1 + [1] p(s) = [2] x1 + [1] p(s1) = [2] p(sel) = [4] x2 + [2] p(sel1) = [4] x1 + [1] x2 + [1] p(unquote) = [0] p(unquote1) = [0] p(0#) = [0] p(activate#) = [0] p(cons#) = [1] x2 + [0] p(fcons#) = [1] p(first#) = [1] x2 + [0] p(first1#) = [1] x2 + [2] p(from#) = [1] x1 + [0] p(nil#) = [1] p(quote#) = [0] p(quote1#) = [2] p(s#) = [1] p(sel#) = [2] x2 + [4] p(sel1#) = [4] p(unquote#) = [0] p(unquote1#) = [0] p(c_1) = [1] p(c_2) = [0] p(c_3) = [0] p(c_4) = [4] x1 + [0] p(c_5) = [2] x1 + [1] x2 + [0] p(c_6) = [4] x1 + [0] p(c_7) = [1] x1 + [1] p(c_8) = [4] x1 + [0] p(c_9) = [2] x1 + [1] x2 + [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [1] x1 + [1] p(c_14) = [1] p(c_15) = [0] p(c_16) = [0] p(c_17) = [1] x1 + [1] x2 + [0] p(c_18) = [1] x1 + [4] x2 + [0] p(c_19) = [2] x1 + [4] x2 + [1] x3 + [4] x4 + [0] p(c_20) = [1] x1 + [4] x2 + [1] p(c_21) = [0] p(c_22) = [0] p(c_23) = [1] p(c_24) = [0] p(c_25) = [4] x1 + [0] p(c_26) = [1] x1 + [4] x2 + [0] p(c_27) = [0] Following rules are strictly oriented: quote1#(n__first(X,Z)) = [2] > [1] = c_20(activate#(X),activate#(Z)) Following rules are (at-least) weakly oriented: activate#(n__cons(X1,X2)) = [0] >= [0] = c_4(activate#(X1)) activate#(n__first(X1,X2)) = [0] >= [0] = c_5(activate#(X1),activate#(X2)) activate#(n__from(X)) = [0] >= [0] = c_6(activate#(X)) activate#(n__s(X)) = [0] >= [0] = c_8(activate#(X)) activate#(n__sel(X1,X2)) = [0] >= [0] = c_9(activate#(X1),activate#(X2)) quote#(n__s(X)) = [0] >= [0] = c_17(quote#(activate(X)),activate#(X)) quote#(n__sel(X,Z)) = [0] >= [0] = c_18(activate#(X),activate#(Z)) quote1#(n__cons(X,Z)) = [2] >= [2] = c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)) unquote#(s1(X)) = [0] >= [0] = c_25(unquote#(X)) unquote1#(cons1(X,Z)) = [0] >= [0] = c_26(unquote#(X),unquote1#(Z)) * Step 10: Failure MAYBE + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__first(X1,X2)) -> c_5(activate#(X1),activate#(X2)) activate#(n__from(X)) -> c_6(activate#(X)) activate#(n__s(X)) -> c_8(activate#(X)) activate#(n__sel(X1,X2)) -> c_9(activate#(X1),activate#(X2)) quote#(n__s(X)) -> c_17(quote#(activate(X)),activate#(X)) quote#(n__sel(X,Z)) -> c_18(activate#(X),activate#(Z)) quote1#(n__cons(X,Z)) -> c_19(quote#(activate(X)),activate#(X),quote1#(activate(Z)),activate#(Z)) unquote#(s1(X)) -> c_25(unquote#(X)) unquote1#(cons1(X,Z)) -> c_26(unquote#(X),unquote1#(Z)) - Weak DPs: quote1#(n__first(X,Z)) -> c_20(activate#(X),activate#(Z)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) cons(X1,X2) -> n__cons(X1,X2) first(X1,X2) -> n__first(X1,X2) from(X) -> cons(X,n__from(n__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/2,c_6/1,c_7/1,c_8/1,c_9/2,c_10/0,c_11/1,c_12/0 ,c_13/1,c_14/0,c_15/0,c_16/0,c_17/2,c_18/2,c_19/4,c_20/2,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