WORST_CASE(?,O(n^1)) * Step 1: InnermostRuleRemoval WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() U61(tt()) -> tt() U71(tt(),P) -> U72(isPal(activate(P))) U72(tt()) -> tt() U81(tt()) -> tt() __(X,nil()) -> X __(X1,X2) -> n____(X1,X2) __(__(X,Y),Z) -> __(X,__(Y,Z)) __(nil(),X) -> X a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isNePal(V) -> U61(isQid(activate(V))) isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) isPal(V) -> U81(isNePal(activate(V))) isPal(n__nil()) -> tt() isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0 ,n__o/0,n__u/0,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a ,activate,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil ,n__o,n__u,tt} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. __(X,nil()) -> X __(__(X,Y),Z) -> __(X,__(Y,Z)) __(nil(),X) -> X isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P)) All above mentioned rules can be savely removed. * Step 2: DependencyPairs WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() U61(tt()) -> tt() U71(tt(),P) -> U72(isPal(activate(P))) U72(tt()) -> tt() U81(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isNePal(V) -> U61(isQid(activate(V))) isPal(V) -> U81(isNePal(activate(V))) isPal(n__nil()) -> tt() isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0 ,n__o/0,n__u/0,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11,U21,U22,U31,U41,U42,U51,U52,U61,U71,U72,U81,__,a ,activate,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,u} and constructors {n____,n__a,n__e,n__i,n__nil ,n__o,n__u,tt} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs U11#(tt()) -> c_1() U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) U22#(tt()) -> c_3() U31#(tt()) -> c_4() U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)) U42#(tt()) -> c_6() U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) U52#(tt()) -> c_8() U61#(tt()) -> c_9() U71#(tt(),P) -> c_10(U72#(isPal(activate(P))),isPal#(activate(P)),activate#(P)) U72#(tt()) -> c_11() U81#(tt()) -> c_12() __#(X1,X2) -> c_13() a#() -> c_14() activate#(X) -> c_15() activate#(n____(X1,X2)) -> c_16(__#(X1,X2)) activate#(n__a()) -> c_17(a#()) activate#(n__e()) -> c_18(e#()) activate#(n__i()) -> c_19(i#()) activate#(n__nil()) -> c_20(nil#()) activate#(n__o()) -> c_21(o#()) activate#(n__u()) -> c_22(u#()) e#() -> c_23() i#() -> c_24() isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isList#(n__nil()) -> c_27() isNeList#(V) -> c_28(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNePal#(V) -> c_31(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isPal#(V) -> c_32(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) isPal#(n__nil()) -> c_33() isQid#(n__a()) -> c_34() isQid#(n__e()) -> c_35() isQid#(n__i()) -> c_36() isQid#(n__o()) -> c_37() isQid#(n__u()) -> c_38() nil#() -> c_39() o#() -> c_40() u#() -> c_41() Weak DPs and mark the set of starting terms. * Step 3: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: U11#(tt()) -> c_1() U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) U22#(tt()) -> c_3() U31#(tt()) -> c_4() U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)) U42#(tt()) -> c_6() U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) U52#(tt()) -> c_8() U61#(tt()) -> c_9() U71#(tt(),P) -> c_10(U72#(isPal(activate(P))),isPal#(activate(P)),activate#(P)) U72#(tt()) -> c_11() U81#(tt()) -> c_12() __#(X1,X2) -> c_13() a#() -> c_14() activate#(X) -> c_15() activate#(n____(X1,X2)) -> c_16(__#(X1,X2)) activate#(n__a()) -> c_17(a#()) activate#(n__e()) -> c_18(e#()) activate#(n__i()) -> c_19(i#()) activate#(n__nil()) -> c_20(nil#()) activate#(n__o()) -> c_21(o#()) activate#(n__u()) -> c_22(u#()) e#() -> c_23() i#() -> c_24() isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isList#(n__nil()) -> c_27() isNeList#(V) -> c_28(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNePal#(V) -> c_31(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isPal#(V) -> c_32(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) isPal#(n__nil()) -> c_33() isQid#(n__a()) -> c_34() isQid#(n__e()) -> c_35() isQid#(n__i()) -> c_36() isQid#(n__o()) -> c_37() isQid#(n__u()) -> c_38() nil#() -> c_39() o#() -> c_40() u#() -> c_41() - Weak TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() U61(tt()) -> tt() U71(tt(),P) -> U72(isPal(activate(P))) U72(tt()) -> tt() U81(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isNePal(V) -> U61(isQid(activate(V))) isPal(V) -> U81(isNePal(activate(V))) isPal(n__nil()) -> tt() isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0,U11#/1,U21#/2,U22#/1,U31#/1,U41#/2,U42#/1 ,U51#/2,U52#/1,U61#/1,U71#/2,U72#/1,U81#/1,__#/2,a#/0,activate#/1,e#/0,i#/0,isList#/1,isNeList#/1,isNePal#/1 ,isPal#/1,isQid#/1,nil#/0,o#/0,u#/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0,n__o/0,n__u/0,tt/0,c_1/0,c_2/3 ,c_3/0,c_4/0,c_5/3,c_6/0,c_7/3,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/3,c_26/4,c_27/0,c_28/3,c_29/4,c_30/4,c_31/3,c_32/3,c_33/0 ,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72# ,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} and constructors {n____ ,n__a,n__e,n__i,n__nil,n__o,n__u,tt} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() U61(tt()) -> tt() U81(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isNePal(V) -> U61(isQid(activate(V))) isPal(V) -> U81(isNePal(activate(V))) isPal(n__nil()) -> tt() isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() U11#(tt()) -> c_1() U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) U22#(tt()) -> c_3() U31#(tt()) -> c_4() U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)) U42#(tt()) -> c_6() U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) U52#(tt()) -> c_8() U61#(tt()) -> c_9() U71#(tt(),P) -> c_10(U72#(isPal(activate(P))),isPal#(activate(P)),activate#(P)) U72#(tt()) -> c_11() U81#(tt()) -> c_12() __#(X1,X2) -> c_13() a#() -> c_14() activate#(X) -> c_15() activate#(n____(X1,X2)) -> c_16(__#(X1,X2)) activate#(n__a()) -> c_17(a#()) activate#(n__e()) -> c_18(e#()) activate#(n__i()) -> c_19(i#()) activate#(n__nil()) -> c_20(nil#()) activate#(n__o()) -> c_21(o#()) activate#(n__u()) -> c_22(u#()) e#() -> c_23() i#() -> c_24() isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isList#(n__nil()) -> c_27() isNeList#(V) -> c_28(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNePal#(V) -> c_31(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isPal#(V) -> c_32(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) isPal#(n__nil()) -> c_33() isQid#(n__a()) -> c_34() isQid#(n__e()) -> c_35() isQid#(n__i()) -> c_36() isQid#(n__o()) -> c_37() isQid#(n__u()) -> c_38() nil#() -> c_39() o#() -> c_40() u#() -> c_41() * Step 4: PredecessorEstimation WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: U11#(tt()) -> c_1() U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) U22#(tt()) -> c_3() U31#(tt()) -> c_4() U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)) U42#(tt()) -> c_6() U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) U52#(tt()) -> c_8() U61#(tt()) -> c_9() U71#(tt(),P) -> c_10(U72#(isPal(activate(P))),isPal#(activate(P)),activate#(P)) U72#(tt()) -> c_11() U81#(tt()) -> c_12() __#(X1,X2) -> c_13() a#() -> c_14() activate#(X) -> c_15() activate#(n____(X1,X2)) -> c_16(__#(X1,X2)) activate#(n__a()) -> c_17(a#()) activate#(n__e()) -> c_18(e#()) activate#(n__i()) -> c_19(i#()) activate#(n__nil()) -> c_20(nil#()) activate#(n__o()) -> c_21(o#()) activate#(n__u()) -> c_22(u#()) e#() -> c_23() i#() -> c_24() isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isList#(n__nil()) -> c_27() isNeList#(V) -> c_28(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNePal#(V) -> c_31(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isPal#(V) -> c_32(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) isPal#(n__nil()) -> c_33() isQid#(n__a()) -> c_34() isQid#(n__e()) -> c_35() isQid#(n__i()) -> c_36() isQid#(n__o()) -> c_37() isQid#(n__u()) -> c_38() nil#() -> c_39() o#() -> c_40() u#() -> c_41() - Weak TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() U61(tt()) -> tt() U81(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isNePal(V) -> U61(isQid(activate(V))) isPal(V) -> U81(isNePal(activate(V))) isPal(n__nil()) -> tt() isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0,U11#/1,U21#/2,U22#/1,U31#/1,U41#/2,U42#/1 ,U51#/2,U52#/1,U61#/1,U71#/2,U72#/1,U81#/1,__#/2,a#/0,activate#/1,e#/0,i#/0,isList#/1,isNeList#/1,isNePal#/1 ,isPal#/1,isQid#/1,nil#/0,o#/0,u#/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0,n__o/0,n__u/0,tt/0,c_1/0,c_2/3 ,c_3/0,c_4/0,c_5/3,c_6/0,c_7/3,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/3,c_26/4,c_27/0,c_28/3,c_29/4,c_30/4,c_31/3,c_32/3,c_33/0 ,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72# ,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} and constructors {n____ ,n__a,n__e,n__i,n__nil,n__o,n__u,tt} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,3,4,6,8,9,11,12,13,14,15,23,24,27,33,34,35,36,37,38,39,40,41} by application of Pre({1,3,4,6,8,9,11,12,13,14,15,23,24,27,33,34,35,36,37,38,39,40,41}) = {2,5,7,10,16,17,18,19,20,21,22,25 ,26,28,29,30,31,32}. Here rules are labelled as follows: 1: U11#(tt()) -> c_1() 2: U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) 3: U22#(tt()) -> c_3() 4: U31#(tt()) -> c_4() 5: U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)) 6: U42#(tt()) -> c_6() 7: U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) 8: U52#(tt()) -> c_8() 9: U61#(tt()) -> c_9() 10: U71#(tt(),P) -> c_10(U72#(isPal(activate(P))),isPal#(activate(P)),activate#(P)) 11: U72#(tt()) -> c_11() 12: U81#(tt()) -> c_12() 13: __#(X1,X2) -> c_13() 14: a#() -> c_14() 15: activate#(X) -> c_15() 16: activate#(n____(X1,X2)) -> c_16(__#(X1,X2)) 17: activate#(n__a()) -> c_17(a#()) 18: activate#(n__e()) -> c_18(e#()) 19: activate#(n__i()) -> c_19(i#()) 20: activate#(n__nil()) -> c_20(nil#()) 21: activate#(n__o()) -> c_21(o#()) 22: activate#(n__u()) -> c_22(u#()) 23: e#() -> c_23() 24: i#() -> c_24() 25: isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) 26: isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 27: isList#(n__nil()) -> c_27() 28: isNeList#(V) -> c_28(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) 29: isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 30: isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 31: isNePal#(V) -> c_31(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) 32: isPal#(V) -> c_32(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) 33: isPal#(n__nil()) -> c_33() 34: isQid#(n__a()) -> c_34() 35: isQid#(n__e()) -> c_35() 36: isQid#(n__i()) -> c_36() 37: isQid#(n__o()) -> c_37() 38: isQid#(n__u()) -> c_38() 39: nil#() -> c_39() 40: o#() -> c_40() 41: u#() -> c_41() * Step 5: PredecessorEstimation WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)) U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) U71#(tt(),P) -> c_10(U72#(isPal(activate(P))),isPal#(activate(P)),activate#(P)) activate#(n____(X1,X2)) -> c_16(__#(X1,X2)) activate#(n__a()) -> c_17(a#()) activate#(n__e()) -> c_18(e#()) activate#(n__i()) -> c_19(i#()) activate#(n__nil()) -> c_20(nil#()) activate#(n__o()) -> c_21(o#()) activate#(n__u()) -> c_22(u#()) isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(V) -> c_28(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNePal#(V) -> c_31(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isPal#(V) -> c_32(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) - Weak DPs: U11#(tt()) -> c_1() U22#(tt()) -> c_3() U31#(tt()) -> c_4() U42#(tt()) -> c_6() U52#(tt()) -> c_8() U61#(tt()) -> c_9() U72#(tt()) -> c_11() U81#(tt()) -> c_12() __#(X1,X2) -> c_13() a#() -> c_14() activate#(X) -> c_15() e#() -> c_23() i#() -> c_24() isList#(n__nil()) -> c_27() isPal#(n__nil()) -> c_33() isQid#(n__a()) -> c_34() isQid#(n__e()) -> c_35() isQid#(n__i()) -> c_36() isQid#(n__o()) -> c_37() isQid#(n__u()) -> c_38() nil#() -> c_39() o#() -> c_40() u#() -> c_41() - Weak TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() U61(tt()) -> tt() U81(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isNePal(V) -> U61(isQid(activate(V))) isPal(V) -> U81(isNePal(activate(V))) isPal(n__nil()) -> tt() isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0,U11#/1,U21#/2,U22#/1,U31#/1,U41#/2,U42#/1 ,U51#/2,U52#/1,U61#/1,U71#/2,U72#/1,U81#/1,__#/2,a#/0,activate#/1,e#/0,i#/0,isList#/1,isNeList#/1,isNePal#/1 ,isPal#/1,isQid#/1,nil#/0,o#/0,u#/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0,n__o/0,n__u/0,tt/0,c_1/0,c_2/3 ,c_3/0,c_4/0,c_5/3,c_6/0,c_7/3,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/3,c_26/4,c_27/0,c_28/3,c_29/4,c_30/4,c_31/3,c_32/3,c_33/0 ,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72# ,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} and constructors {n____ ,n__a,n__e,n__i,n__nil,n__o,n__u,tt} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {5,6,7,8,9,10,11} by application of Pre({5,6,7,8,9,10,11}) = {1,2,3,4,12,13,14,15,16,17,18}. Here rules are labelled as follows: 1: U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) 2: U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)) 3: U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) 4: U71#(tt(),P) -> c_10(U72#(isPal(activate(P))),isPal#(activate(P)),activate#(P)) 5: activate#(n____(X1,X2)) -> c_16(__#(X1,X2)) 6: activate#(n__a()) -> c_17(a#()) 7: activate#(n__e()) -> c_18(e#()) 8: activate#(n__i()) -> c_19(i#()) 9: activate#(n__nil()) -> c_20(nil#()) 10: activate#(n__o()) -> c_21(o#()) 11: activate#(n__u()) -> c_22(u#()) 12: isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) 13: isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 14: isNeList#(V) -> c_28(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) 15: isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 16: isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 17: isNePal#(V) -> c_31(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) 18: isPal#(V) -> c_32(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) 19: U11#(tt()) -> c_1() 20: U22#(tt()) -> c_3() 21: U31#(tt()) -> c_4() 22: U42#(tt()) -> c_6() 23: U52#(tt()) -> c_8() 24: U61#(tt()) -> c_9() 25: U72#(tt()) -> c_11() 26: U81#(tt()) -> c_12() 27: __#(X1,X2) -> c_13() 28: a#() -> c_14() 29: activate#(X) -> c_15() 30: e#() -> c_23() 31: i#() -> c_24() 32: isList#(n__nil()) -> c_27() 33: isPal#(n__nil()) -> c_33() 34: isQid#(n__a()) -> c_34() 35: isQid#(n__e()) -> c_35() 36: isQid#(n__i()) -> c_36() 37: isQid#(n__o()) -> c_37() 38: isQid#(n__u()) -> c_38() 39: nil#() -> c_39() 40: o#() -> c_40() 41: u#() -> c_41() * Step 6: PredecessorEstimation WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)) U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) U71#(tt(),P) -> c_10(U72#(isPal(activate(P))),isPal#(activate(P)),activate#(P)) isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(V) -> c_28(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNePal#(V) -> c_31(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isPal#(V) -> c_32(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) - Weak DPs: U11#(tt()) -> c_1() U22#(tt()) -> c_3() U31#(tt()) -> c_4() U42#(tt()) -> c_6() U52#(tt()) -> c_8() U61#(tt()) -> c_9() U72#(tt()) -> c_11() U81#(tt()) -> c_12() __#(X1,X2) -> c_13() a#() -> c_14() activate#(X) -> c_15() activate#(n____(X1,X2)) -> c_16(__#(X1,X2)) activate#(n__a()) -> c_17(a#()) activate#(n__e()) -> c_18(e#()) activate#(n__i()) -> c_19(i#()) activate#(n__nil()) -> c_20(nil#()) activate#(n__o()) -> c_21(o#()) activate#(n__u()) -> c_22(u#()) e#() -> c_23() i#() -> c_24() isList#(n__nil()) -> c_27() isPal#(n__nil()) -> c_33() isQid#(n__a()) -> c_34() isQid#(n__e()) -> c_35() isQid#(n__i()) -> c_36() isQid#(n__o()) -> c_37() isQid#(n__u()) -> c_38() nil#() -> c_39() o#() -> c_40() u#() -> c_41() - Weak TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() U61(tt()) -> tt() U81(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isNePal(V) -> U61(isQid(activate(V))) isPal(V) -> U81(isNePal(activate(V))) isPal(n__nil()) -> tt() isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0,U11#/1,U21#/2,U22#/1,U31#/1,U41#/2,U42#/1 ,U51#/2,U52#/1,U61#/1,U71#/2,U72#/1,U81#/1,__#/2,a#/0,activate#/1,e#/0,i#/0,isList#/1,isNeList#/1,isNePal#/1 ,isPal#/1,isQid#/1,nil#/0,o#/0,u#/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0,n__o/0,n__u/0,tt/0,c_1/0,c_2/3 ,c_3/0,c_4/0,c_5/3,c_6/0,c_7/3,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/3,c_26/4,c_27/0,c_28/3,c_29/4,c_30/4,c_31/3,c_32/3,c_33/0 ,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72# ,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} and constructors {n____ ,n__a,n__e,n__i,n__nil,n__o,n__u,tt} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {7,10} by application of Pre({7,10}) = {2,5,9,11}. Here rules are labelled as follows: 1: U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) 2: U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)) 3: U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) 4: U71#(tt(),P) -> c_10(U72#(isPal(activate(P))),isPal#(activate(P)),activate#(P)) 5: isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) 6: isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 7: isNeList#(V) -> c_28(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) 8: isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 9: isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 10: isNePal#(V) -> c_31(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) 11: isPal#(V) -> c_32(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) 12: U11#(tt()) -> c_1() 13: U22#(tt()) -> c_3() 14: U31#(tt()) -> c_4() 15: U42#(tt()) -> c_6() 16: U52#(tt()) -> c_8() 17: U61#(tt()) -> c_9() 18: U72#(tt()) -> c_11() 19: U81#(tt()) -> c_12() 20: __#(X1,X2) -> c_13() 21: a#() -> c_14() 22: activate#(X) -> c_15() 23: activate#(n____(X1,X2)) -> c_16(__#(X1,X2)) 24: activate#(n__a()) -> c_17(a#()) 25: activate#(n__e()) -> c_18(e#()) 26: activate#(n__i()) -> c_19(i#()) 27: activate#(n__nil()) -> c_20(nil#()) 28: activate#(n__o()) -> c_21(o#()) 29: activate#(n__u()) -> c_22(u#()) 30: e#() -> c_23() 31: i#() -> c_24() 32: isList#(n__nil()) -> c_27() 33: isPal#(n__nil()) -> c_33() 34: isQid#(n__a()) -> c_34() 35: isQid#(n__e()) -> c_35() 36: isQid#(n__i()) -> c_36() 37: isQid#(n__o()) -> c_37() 38: isQid#(n__u()) -> c_38() 39: nil#() -> c_39() 40: o#() -> c_40() 41: u#() -> c_41() * Step 7: PredecessorEstimation WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)) U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) U71#(tt(),P) -> c_10(U72#(isPal(activate(P))),isPal#(activate(P)),activate#(P)) isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isPal#(V) -> c_32(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) - Weak DPs: U11#(tt()) -> c_1() U22#(tt()) -> c_3() U31#(tt()) -> c_4() U42#(tt()) -> c_6() U52#(tt()) -> c_8() U61#(tt()) -> c_9() U72#(tt()) -> c_11() U81#(tt()) -> c_12() __#(X1,X2) -> c_13() a#() -> c_14() activate#(X) -> c_15() activate#(n____(X1,X2)) -> c_16(__#(X1,X2)) activate#(n__a()) -> c_17(a#()) activate#(n__e()) -> c_18(e#()) activate#(n__i()) -> c_19(i#()) activate#(n__nil()) -> c_20(nil#()) activate#(n__o()) -> c_21(o#()) activate#(n__u()) -> c_22(u#()) e#() -> c_23() i#() -> c_24() isList#(n__nil()) -> c_27() isNeList#(V) -> c_28(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isNePal#(V) -> c_31(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isPal#(n__nil()) -> c_33() isQid#(n__a()) -> c_34() isQid#(n__e()) -> c_35() isQid#(n__i()) -> c_36() isQid#(n__o()) -> c_37() isQid#(n__u()) -> c_38() nil#() -> c_39() o#() -> c_40() u#() -> c_41() - Weak TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() U61(tt()) -> tt() U81(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isNePal(V) -> U61(isQid(activate(V))) isPal(V) -> U81(isNePal(activate(V))) isPal(n__nil()) -> tt() isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0,U11#/1,U21#/2,U22#/1,U31#/1,U41#/2,U42#/1 ,U51#/2,U52#/1,U61#/1,U71#/2,U72#/1,U81#/1,__#/2,a#/0,activate#/1,e#/0,i#/0,isList#/1,isNeList#/1,isNePal#/1 ,isPal#/1,isQid#/1,nil#/0,o#/0,u#/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0,n__o/0,n__u/0,tt/0,c_1/0,c_2/3 ,c_3/0,c_4/0,c_5/3,c_6/0,c_7/3,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/3,c_26/4,c_27/0,c_28/3,c_29/4,c_30/4,c_31/3,c_32/3,c_33/0 ,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72# ,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} and constructors {n____ ,n__a,n__e,n__i,n__nil,n__o,n__u,tt} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {9} by application of Pre({9}) = {4}. Here rules are labelled as follows: 1: U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) 2: U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)) 3: U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) 4: U71#(tt(),P) -> c_10(U72#(isPal(activate(P))),isPal#(activate(P)),activate#(P)) 5: isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) 6: isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 7: isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 8: isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 9: isPal#(V) -> c_32(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) 10: U11#(tt()) -> c_1() 11: U22#(tt()) -> c_3() 12: U31#(tt()) -> c_4() 13: U42#(tt()) -> c_6() 14: U52#(tt()) -> c_8() 15: U61#(tt()) -> c_9() 16: U72#(tt()) -> c_11() 17: U81#(tt()) -> c_12() 18: __#(X1,X2) -> c_13() 19: a#() -> c_14() 20: activate#(X) -> c_15() 21: activate#(n____(X1,X2)) -> c_16(__#(X1,X2)) 22: activate#(n__a()) -> c_17(a#()) 23: activate#(n__e()) -> c_18(e#()) 24: activate#(n__i()) -> c_19(i#()) 25: activate#(n__nil()) -> c_20(nil#()) 26: activate#(n__o()) -> c_21(o#()) 27: activate#(n__u()) -> c_22(u#()) 28: e#() -> c_23() 29: i#() -> c_24() 30: isList#(n__nil()) -> c_27() 31: isNeList#(V) -> c_28(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) 32: isNePal#(V) -> c_31(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) 33: isPal#(n__nil()) -> c_33() 34: isQid#(n__a()) -> c_34() 35: isQid#(n__e()) -> c_35() 36: isQid#(n__i()) -> c_36() 37: isQid#(n__o()) -> c_37() 38: isQid#(n__u()) -> c_38() 39: nil#() -> c_39() 40: o#() -> c_40() 41: u#() -> c_41() * Step 8: PredecessorEstimation WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)) U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) U71#(tt(),P) -> c_10(U72#(isPal(activate(P))),isPal#(activate(P)),activate#(P)) isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) - Weak DPs: U11#(tt()) -> c_1() U22#(tt()) -> c_3() U31#(tt()) -> c_4() U42#(tt()) -> c_6() U52#(tt()) -> c_8() U61#(tt()) -> c_9() U72#(tt()) -> c_11() U81#(tt()) -> c_12() __#(X1,X2) -> c_13() a#() -> c_14() activate#(X) -> c_15() activate#(n____(X1,X2)) -> c_16(__#(X1,X2)) activate#(n__a()) -> c_17(a#()) activate#(n__e()) -> c_18(e#()) activate#(n__i()) -> c_19(i#()) activate#(n__nil()) -> c_20(nil#()) activate#(n__o()) -> c_21(o#()) activate#(n__u()) -> c_22(u#()) e#() -> c_23() i#() -> c_24() isList#(n__nil()) -> c_27() isNeList#(V) -> c_28(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isNePal#(V) -> c_31(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isPal#(V) -> c_32(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) isPal#(n__nil()) -> c_33() isQid#(n__a()) -> c_34() isQid#(n__e()) -> c_35() isQid#(n__i()) -> c_36() isQid#(n__o()) -> c_37() isQid#(n__u()) -> c_38() nil#() -> c_39() o#() -> c_40() u#() -> c_41() - Weak TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() U61(tt()) -> tt() U81(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isNePal(V) -> U61(isQid(activate(V))) isPal(V) -> U81(isNePal(activate(V))) isPal(n__nil()) -> tt() isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0,U11#/1,U21#/2,U22#/1,U31#/1,U41#/2,U42#/1 ,U51#/2,U52#/1,U61#/1,U71#/2,U72#/1,U81#/1,__#/2,a#/0,activate#/1,e#/0,i#/0,isList#/1,isNeList#/1,isNePal#/1 ,isPal#/1,isQid#/1,nil#/0,o#/0,u#/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0,n__o/0,n__u/0,tt/0,c_1/0,c_2/3 ,c_3/0,c_4/0,c_5/3,c_6/0,c_7/3,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/3,c_26/4,c_27/0,c_28/3,c_29/4,c_30/4,c_31/3,c_32/3,c_33/0 ,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72# ,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} and constructors {n____ ,n__a,n__e,n__i,n__nil,n__o,n__u,tt} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {4} by application of Pre({4}) = {}. Here rules are labelled as follows: 1: U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) 2: U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)) 3: U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) 4: U71#(tt(),P) -> c_10(U72#(isPal(activate(P))),isPal#(activate(P)),activate#(P)) 5: isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) 6: isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 7: isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 8: isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 9: U11#(tt()) -> c_1() 10: U22#(tt()) -> c_3() 11: U31#(tt()) -> c_4() 12: U42#(tt()) -> c_6() 13: U52#(tt()) -> c_8() 14: U61#(tt()) -> c_9() 15: U72#(tt()) -> c_11() 16: U81#(tt()) -> c_12() 17: __#(X1,X2) -> c_13() 18: a#() -> c_14() 19: activate#(X) -> c_15() 20: activate#(n____(X1,X2)) -> c_16(__#(X1,X2)) 21: activate#(n__a()) -> c_17(a#()) 22: activate#(n__e()) -> c_18(e#()) 23: activate#(n__i()) -> c_19(i#()) 24: activate#(n__nil()) -> c_20(nil#()) 25: activate#(n__o()) -> c_21(o#()) 26: activate#(n__u()) -> c_22(u#()) 27: e#() -> c_23() 28: i#() -> c_24() 29: isList#(n__nil()) -> c_27() 30: isNeList#(V) -> c_28(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) 31: isNePal#(V) -> c_31(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) 32: isPal#(V) -> c_32(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) 33: isPal#(n__nil()) -> c_33() 34: isQid#(n__a()) -> c_34() 35: isQid#(n__e()) -> c_35() 36: isQid#(n__i()) -> c_36() 37: isQid#(n__o()) -> c_37() 38: isQid#(n__u()) -> c_38() 39: nil#() -> c_39() 40: o#() -> c_40() 41: u#() -> c_41() * Step 9: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)) U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) - Weak DPs: U11#(tt()) -> c_1() U22#(tt()) -> c_3() U31#(tt()) -> c_4() U42#(tt()) -> c_6() U52#(tt()) -> c_8() U61#(tt()) -> c_9() U71#(tt(),P) -> c_10(U72#(isPal(activate(P))),isPal#(activate(P)),activate#(P)) U72#(tt()) -> c_11() U81#(tt()) -> c_12() __#(X1,X2) -> c_13() a#() -> c_14() activate#(X) -> c_15() activate#(n____(X1,X2)) -> c_16(__#(X1,X2)) activate#(n__a()) -> c_17(a#()) activate#(n__e()) -> c_18(e#()) activate#(n__i()) -> c_19(i#()) activate#(n__nil()) -> c_20(nil#()) activate#(n__o()) -> c_21(o#()) activate#(n__u()) -> c_22(u#()) e#() -> c_23() i#() -> c_24() isList#(n__nil()) -> c_27() isNeList#(V) -> c_28(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isNePal#(V) -> c_31(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isPal#(V) -> c_32(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) isPal#(n__nil()) -> c_33() isQid#(n__a()) -> c_34() isQid#(n__e()) -> c_35() isQid#(n__i()) -> c_36() isQid#(n__o()) -> c_37() isQid#(n__u()) -> c_38() nil#() -> c_39() o#() -> c_40() u#() -> c_41() - Weak TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() U61(tt()) -> tt() U81(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isNePal(V) -> U61(isQid(activate(V))) isPal(V) -> U81(isNePal(activate(V))) isPal(n__nil()) -> tt() isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0,U11#/1,U21#/2,U22#/1,U31#/1,U41#/2,U42#/1 ,U51#/2,U52#/1,U61#/1,U71#/2,U72#/1,U81#/1,__#/2,a#/0,activate#/1,e#/0,i#/0,isList#/1,isNeList#/1,isNePal#/1 ,isPal#/1,isQid#/1,nil#/0,o#/0,u#/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0,n__o/0,n__u/0,tt/0,c_1/0,c_2/3 ,c_3/0,c_4/0,c_5/3,c_6/0,c_7/3,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/3,c_26/4,c_27/0,c_28/3,c_29/4,c_30/4,c_31/3,c_32/3,c_33/0 ,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72# ,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} and constructors {n____ ,n__a,n__e,n__i,n__nil,n__o,n__u,tt} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) -->_3 activate#(n__u()) -> c_22(u#()):26 -->_3 activate#(n__o()) -> c_21(o#()):25 -->_3 activate#(n__nil()) -> c_20(nil#()):24 -->_3 activate#(n__i()) -> c_19(i#()):23 -->_3 activate#(n__e()) -> c_18(e#()):22 -->_3 activate#(n__a()) -> c_17(a#()):21 -->_3 activate#(n____(X1,X2)) -> c_16(__#(X1,X2)):20 -->_2 isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):5 -->_2 isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)):4 -->_2 isList#(n__nil()) -> c_27():29 -->_3 activate#(X) -> c_15():19 -->_1 U22#(tt()) -> c_3():9 2:S:U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)) -->_2 isNeList#(V) -> c_28(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)):30 -->_3 activate#(n__u()) -> c_22(u#()):26 -->_3 activate#(n__o()) -> c_21(o#()):25 -->_3 activate#(n__nil()) -> c_20(nil#()):24 -->_3 activate#(n__i()) -> c_19(i#()):23 -->_3 activate#(n__e()) -> c_18(e#()):22 -->_3 activate#(n__a()) -> c_17(a#()):21 -->_3 activate#(n____(X1,X2)) -> c_16(__#(X1,X2)):20 -->_2 isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_2 isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):6 -->_3 activate#(X) -> c_15():19 -->_1 U42#(tt()) -> c_6():11 3:S:U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) -->_3 activate#(n__u()) -> c_22(u#()):26 -->_3 activate#(n__o()) -> c_21(o#()):25 -->_3 activate#(n__nil()) -> c_20(nil#()):24 -->_3 activate#(n__i()) -> c_19(i#()):23 -->_3 activate#(n__e()) -> c_18(e#()):22 -->_3 activate#(n__a()) -> c_17(a#()):21 -->_3 activate#(n____(X1,X2)) -> c_16(__#(X1,X2)):20 -->_2 isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):5 -->_2 isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)):4 -->_2 isList#(n__nil()) -> c_27():29 -->_3 activate#(X) -> c_15():19 -->_1 U52#(tt()) -> c_8():12 4:S:isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) -->_2 isNeList#(V) -> c_28(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)):30 -->_3 activate#(n__u()) -> c_22(u#()):26 -->_3 activate#(n__o()) -> c_21(o#()):25 -->_3 activate#(n__nil()) -> c_20(nil#()):24 -->_3 activate#(n__i()) -> c_19(i#()):23 -->_3 activate#(n__e()) -> c_18(e#()):22 -->_3 activate#(n__a()) -> c_17(a#()):21 -->_3 activate#(n____(X1,X2)) -> c_16(__#(X1,X2)):20 -->_2 isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_2 isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):6 -->_3 activate#(X) -> c_15():19 -->_1 U11#(tt()) -> c_1():8 5:S:isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_4 activate#(n__u()) -> c_22(u#()):26 -->_3 activate#(n__u()) -> c_22(u#()):26 -->_4 activate#(n__o()) -> c_21(o#()):25 -->_3 activate#(n__o()) -> c_21(o#()):25 -->_4 activate#(n__nil()) -> c_20(nil#()):24 -->_3 activate#(n__nil()) -> c_20(nil#()):24 -->_4 activate#(n__i()) -> c_19(i#()):23 -->_3 activate#(n__i()) -> c_19(i#()):23 -->_4 activate#(n__e()) -> c_18(e#()):22 -->_3 activate#(n__e()) -> c_18(e#()):22 -->_4 activate#(n__a()) -> c_17(a#()):21 -->_3 activate#(n__a()) -> c_17(a#()):21 -->_4 activate#(n____(X1,X2)) -> c_16(__#(X1,X2)):20 -->_3 activate#(n____(X1,X2)) -> c_16(__#(X1,X2)):20 -->_2 isList#(n__nil()) -> c_27():29 -->_4 activate#(X) -> c_15():19 -->_3 activate#(X) -> c_15():19 -->_2 isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):5 -->_2 isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)):4 -->_1 U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)):1 6:S:isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_4 activate#(n__u()) -> c_22(u#()):26 -->_3 activate#(n__u()) -> c_22(u#()):26 -->_4 activate#(n__o()) -> c_21(o#()):25 -->_3 activate#(n__o()) -> c_21(o#()):25 -->_4 activate#(n__nil()) -> c_20(nil#()):24 -->_3 activate#(n__nil()) -> c_20(nil#()):24 -->_4 activate#(n__i()) -> c_19(i#()):23 -->_3 activate#(n__i()) -> c_19(i#()):23 -->_4 activate#(n__e()) -> c_18(e#()):22 -->_3 activate#(n__e()) -> c_18(e#()):22 -->_4 activate#(n__a()) -> c_17(a#()):21 -->_3 activate#(n__a()) -> c_17(a#()):21 -->_4 activate#(n____(X1,X2)) -> c_16(__#(X1,X2)):20 -->_3 activate#(n____(X1,X2)) -> c_16(__#(X1,X2)):20 -->_2 isList#(n__nil()) -> c_27():29 -->_4 activate#(X) -> c_15():19 -->_3 activate#(X) -> c_15():19 -->_2 isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):5 -->_2 isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)):4 -->_1 U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)):2 7:S:isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNeList#(V) -> c_28(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)):30 -->_4 activate#(n__u()) -> c_22(u#()):26 -->_3 activate#(n__u()) -> c_22(u#()):26 -->_4 activate#(n__o()) -> c_21(o#()):25 -->_3 activate#(n__o()) -> c_21(o#()):25 -->_4 activate#(n__nil()) -> c_20(nil#()):24 -->_3 activate#(n__nil()) -> c_20(nil#()):24 -->_4 activate#(n__i()) -> c_19(i#()):23 -->_3 activate#(n__i()) -> c_19(i#()):23 -->_4 activate#(n__e()) -> c_18(e#()):22 -->_3 activate#(n__e()) -> c_18(e#()):22 -->_4 activate#(n__a()) -> c_17(a#()):21 -->_3 activate#(n__a()) -> c_17(a#()):21 -->_4 activate#(n____(X1,X2)) -> c_16(__#(X1,X2)):20 -->_3 activate#(n____(X1,X2)) -> c_16(__#(X1,X2)):20 -->_4 activate#(X) -> c_15():19 -->_3 activate#(X) -> c_15():19 -->_2 isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_2 isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):6 -->_1 U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)):3 8:W:U11#(tt()) -> c_1() 9:W:U22#(tt()) -> c_3() 10:W:U31#(tt()) -> c_4() 11:W:U42#(tt()) -> c_6() 12:W:U52#(tt()) -> c_8() 13:W:U61#(tt()) -> c_9() 14:W:U71#(tt(),P) -> c_10(U72#(isPal(activate(P))),isPal#(activate(P)),activate#(P)) -->_2 isPal#(V) -> c_32(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)):32 -->_3 activate#(n__u()) -> c_22(u#()):26 -->_3 activate#(n__o()) -> c_21(o#()):25 -->_3 activate#(n__nil()) -> c_20(nil#()):24 -->_3 activate#(n__i()) -> c_19(i#()):23 -->_3 activate#(n__e()) -> c_18(e#()):22 -->_3 activate#(n__a()) -> c_17(a#()):21 -->_3 activate#(n____(X1,X2)) -> c_16(__#(X1,X2)):20 -->_2 isPal#(n__nil()) -> c_33():33 -->_3 activate#(X) -> c_15():19 -->_1 U72#(tt()) -> c_11():15 15:W:U72#(tt()) -> c_11() 16:W:U81#(tt()) -> c_12() 17:W:__#(X1,X2) -> c_13() 18:W:a#() -> c_14() 19:W:activate#(X) -> c_15() 20:W:activate#(n____(X1,X2)) -> c_16(__#(X1,X2)) -->_1 __#(X1,X2) -> c_13():17 21:W:activate#(n__a()) -> c_17(a#()) -->_1 a#() -> c_14():18 22:W:activate#(n__e()) -> c_18(e#()) -->_1 e#() -> c_23():27 23:W:activate#(n__i()) -> c_19(i#()) -->_1 i#() -> c_24():28 24:W:activate#(n__nil()) -> c_20(nil#()) -->_1 nil#() -> c_39():39 25:W:activate#(n__o()) -> c_21(o#()) -->_1 o#() -> c_40():40 26:W:activate#(n__u()) -> c_22(u#()) -->_1 u#() -> c_41():41 27:W:e#() -> c_23() 28:W:i#() -> c_24() 29:W:isList#(n__nil()) -> c_27() 30:W:isNeList#(V) -> c_28(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) -->_2 isQid#(n__u()) -> c_38():38 -->_2 isQid#(n__o()) -> c_37():37 -->_2 isQid#(n__i()) -> c_36():36 -->_2 isQid#(n__e()) -> c_35():35 -->_2 isQid#(n__a()) -> c_34():34 -->_3 activate#(n__u()) -> c_22(u#()):26 -->_3 activate#(n__o()) -> c_21(o#()):25 -->_3 activate#(n__nil()) -> c_20(nil#()):24 -->_3 activate#(n__i()) -> c_19(i#()):23 -->_3 activate#(n__e()) -> c_18(e#()):22 -->_3 activate#(n__a()) -> c_17(a#()):21 -->_3 activate#(n____(X1,X2)) -> c_16(__#(X1,X2)):20 -->_3 activate#(X) -> c_15():19 -->_1 U31#(tt()) -> c_4():10 31:W:isNePal#(V) -> c_31(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) -->_2 isQid#(n__u()) -> c_38():38 -->_2 isQid#(n__o()) -> c_37():37 -->_2 isQid#(n__i()) -> c_36():36 -->_2 isQid#(n__e()) -> c_35():35 -->_2 isQid#(n__a()) -> c_34():34 -->_3 activate#(n__u()) -> c_22(u#()):26 -->_3 activate#(n__o()) -> c_21(o#()):25 -->_3 activate#(n__nil()) -> c_20(nil#()):24 -->_3 activate#(n__i()) -> c_19(i#()):23 -->_3 activate#(n__e()) -> c_18(e#()):22 -->_3 activate#(n__a()) -> c_17(a#()):21 -->_3 activate#(n____(X1,X2)) -> c_16(__#(X1,X2)):20 -->_3 activate#(X) -> c_15():19 -->_1 U61#(tt()) -> c_9():13 32:W:isPal#(V) -> c_32(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) -->_2 isNePal#(V) -> c_31(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)):31 -->_3 activate#(n__u()) -> c_22(u#()):26 -->_3 activate#(n__o()) -> c_21(o#()):25 -->_3 activate#(n__nil()) -> c_20(nil#()):24 -->_3 activate#(n__i()) -> c_19(i#()):23 -->_3 activate#(n__e()) -> c_18(e#()):22 -->_3 activate#(n__a()) -> c_17(a#()):21 -->_3 activate#(n____(X1,X2)) -> c_16(__#(X1,X2)):20 -->_3 activate#(X) -> c_15():19 -->_1 U81#(tt()) -> c_12():16 33:W:isPal#(n__nil()) -> c_33() 34:W:isQid#(n__a()) -> c_34() 35:W:isQid#(n__e()) -> c_35() 36:W:isQid#(n__i()) -> c_36() 37:W:isQid#(n__o()) -> c_37() 38:W:isQid#(n__u()) -> c_38() 39:W:nil#() -> c_39() 40:W:o#() -> c_40() 41:W:u#() -> c_41() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 14: U71#(tt(),P) -> c_10(U72#(isPal(activate(P))),isPal#(activate(P)),activate#(P)) 15: U72#(tt()) -> c_11() 33: isPal#(n__nil()) -> c_33() 32: isPal#(V) -> c_32(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) 16: U81#(tt()) -> c_12() 31: isNePal#(V) -> c_31(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) 13: U61#(tt()) -> c_9() 9: U22#(tt()) -> c_3() 8: U11#(tt()) -> c_1() 12: U52#(tt()) -> c_8() 11: U42#(tt()) -> c_6() 30: isNeList#(V) -> c_28(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) 10: U31#(tt()) -> c_4() 34: isQid#(n__a()) -> c_34() 35: isQid#(n__e()) -> c_35() 36: isQid#(n__i()) -> c_36() 37: isQid#(n__o()) -> c_37() 38: isQid#(n__u()) -> c_38() 19: activate#(X) -> c_15() 29: isList#(n__nil()) -> c_27() 20: activate#(n____(X1,X2)) -> c_16(__#(X1,X2)) 17: __#(X1,X2) -> c_13() 21: activate#(n__a()) -> c_17(a#()) 18: a#() -> c_14() 22: activate#(n__e()) -> c_18(e#()) 27: e#() -> c_23() 23: activate#(n__i()) -> c_19(i#()) 28: i#() -> c_24() 24: activate#(n__nil()) -> c_20(nil#()) 39: nil#() -> c_39() 25: activate#(n__o()) -> c_21(o#()) 40: o#() -> c_40() 26: activate#(n__u()) -> c_22(u#()) 41: u#() -> c_41() * Step 10: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)) U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) - Weak TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() U61(tt()) -> tt() U81(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isNePal(V) -> U61(isQid(activate(V))) isPal(V) -> U81(isNePal(activate(V))) isPal(n__nil()) -> tt() isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0,U11#/1,U21#/2,U22#/1,U31#/1,U41#/2,U42#/1 ,U51#/2,U52#/1,U61#/1,U71#/2,U72#/1,U81#/1,__#/2,a#/0,activate#/1,e#/0,i#/0,isList#/1,isNeList#/1,isNePal#/1 ,isPal#/1,isQid#/1,nil#/0,o#/0,u#/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0,n__o/0,n__u/0,tt/0,c_1/0,c_2/3 ,c_3/0,c_4/0,c_5/3,c_6/0,c_7/3,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/3,c_26/4,c_27/0,c_28/3,c_29/4,c_30/4,c_31/3,c_32/3,c_33/0 ,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72# ,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} and constructors {n____ ,n__a,n__e,n__i,n__nil,n__o,n__u,tt} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) -->_2 isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):5 -->_2 isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)):4 2:S:U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)) -->_2 isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_2 isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):6 3:S:U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) -->_2 isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):5 -->_2 isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)):4 4:S:isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) -->_2 isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_2 isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):6 5:S:isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):5 -->_2 isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)):4 -->_1 U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)):1 6:S:isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):5 -->_2 isList#(V) -> c_25(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)):4 -->_1 U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)):2 7:S:isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_2 isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):6 -->_1 U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: U21#(tt(),V2) -> c_2(isList#(activate(V2))) U41#(tt(),V2) -> c_5(isNeList#(activate(V2))) U51#(tt(),V2) -> c_7(isList#(activate(V2))) isList#(V) -> c_25(isNeList#(activate(V))) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) * Step 11: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: U21#(tt(),V2) -> c_2(isList#(activate(V2))) U41#(tt(),V2) -> c_5(isNeList#(activate(V2))) U51#(tt(),V2) -> c_7(isList#(activate(V2))) isList#(V) -> c_25(isNeList#(activate(V))) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) - Weak TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() U61(tt()) -> tt() U81(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isNePal(V) -> U61(isQid(activate(V))) isPal(V) -> U81(isNePal(activate(V))) isPal(n__nil()) -> tt() isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0,U11#/1,U21#/2,U22#/1,U31#/1,U41#/2,U42#/1 ,U51#/2,U52#/1,U61#/1,U71#/2,U72#/1,U81#/1,__#/2,a#/0,activate#/1,e#/0,i#/0,isList#/1,isNeList#/1,isNePal#/1 ,isPal#/1,isQid#/1,nil#/0,o#/0,u#/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0,n__o/0,n__u/0,tt/0,c_1/0,c_2/1 ,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/2,c_27/0,c_28/3,c_29/2,c_30/2,c_31/3,c_32/3,c_33/0 ,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72# ,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} and constructors {n____ ,n__a,n__e,n__i,n__nil,n__o,n__u,tt} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() U21#(tt(),V2) -> c_2(isList#(activate(V2))) U41#(tt(),V2) -> c_5(isNeList#(activate(V2))) U51#(tt(),V2) -> c_7(isList#(activate(V2))) isList#(V) -> c_25(isNeList#(activate(V))) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) * Step 12: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: U21#(tt(),V2) -> c_2(isList#(activate(V2))) U41#(tt(),V2) -> c_5(isNeList#(activate(V2))) U51#(tt(),V2) -> c_7(isList#(activate(V2))) isList#(V) -> c_25(isNeList#(activate(V))) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) - Weak TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0,U11#/1,U21#/2,U22#/1,U31#/1,U41#/2,U42#/1 ,U51#/2,U52#/1,U61#/1,U71#/2,U72#/1,U81#/1,__#/2,a#/0,activate#/1,e#/0,i#/0,isList#/1,isNeList#/1,isNePal#/1 ,isPal#/1,isQid#/1,nil#/0,o#/0,u#/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0,n__o/0,n__u/0,tt/0,c_1/0,c_2/1 ,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/2,c_27/0,c_28/3,c_29/2,c_30/2,c_31/3,c_32/3,c_33/0 ,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72# ,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} and constructors {n____ ,n__a,n__e,n__i,n__nil,n__o,n__u,tt} + 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: U21#(tt(),V2) -> c_2(isList#(activate(V2))) The strictly oriented rules are moved into the weak component. ** Step 12.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: U21#(tt(),V2) -> c_2(isList#(activate(V2))) U41#(tt(),V2) -> c_5(isNeList#(activate(V2))) U51#(tt(),V2) -> c_7(isList#(activate(V2))) isList#(V) -> c_25(isNeList#(activate(V))) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) - Weak TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0,U11#/1,U21#/2,U22#/1,U31#/1,U41#/2,U42#/1 ,U51#/2,U52#/1,U61#/1,U71#/2,U72#/1,U81#/1,__#/2,a#/0,activate#/1,e#/0,i#/0,isList#/1,isNeList#/1,isNePal#/1 ,isPal#/1,isQid#/1,nil#/0,o#/0,u#/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0,n__o/0,n__u/0,tt/0,c_1/0,c_2/1 ,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/2,c_27/0,c_28/3,c_29/2,c_30/2,c_31/3,c_32/3,c_33/0 ,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72# ,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} and constructors {n____ ,n__a,n__e,n__i,n__nil,n__o,n__u,tt} + 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_2) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1}, uargs(c_25) = {1}, uargs(c_26) = {1,2}, uargs(c_29) = {1,2}, uargs(c_30) = {1,2} Following symbols are considered usable: {U11,U21,U22,__,a,activate,e,i,isList,nil,o,u,U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72#,U81# ,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} TcT has computed the following interpretation: p(U11) = [0] p(U21) = [1] x1 + [0] p(U22) = [0] p(U31) = [2] x1 + [0] p(U41) = [3] p(U42) = [0] p(U51) = [3] p(U52) = [2] x1 + [4] p(U61) = [0] p(U71) = [2] x2 + [1] p(U72) = [4] x1 + [0] p(U81) = [1] x1 + [1] p(__) = [1] x1 + [1] x2 + [1] p(a) = [0] p(activate) = [1] x1 + [0] p(e) = [0] p(i) = [0] p(isList) = [1] p(isNeList) = [0] p(isNePal) = [2] x1 + [4] p(isPal) = [2] x1 + [0] p(isQid) = [7] p(n____) = [1] x1 + [1] x2 + [1] p(n__a) = [0] p(n__e) = [0] p(n__i) = [0] p(n__nil) = [0] p(n__o) = [0] p(n__u) = [1] p(nil) = [0] p(o) = [0] p(tt) = [0] p(u) = [1] p(U11#) = [1] x1 + [1] p(U21#) = [4] x2 + [4] p(U22#) = [1] x1 + [1] p(U31#) = [0] p(U41#) = [4] x1 + [4] x2 + [0] p(U42#) = [1] x1 + [1] p(U51#) = [4] x2 + [0] p(U52#) = [1] x1 + [1] p(U61#) = [0] p(U71#) = [1] x2 + [0] p(U72#) = [4] p(U81#) = [2] x1 + [0] p(__#) = [4] x2 + [1] p(a#) = [4] p(activate#) = [1] x1 + [4] p(e#) = [0] p(i#) = [1] p(isList#) = [4] x1 + [0] p(isNeList#) = [4] x1 + [0] p(isNePal#) = [1] p(isPal#) = [2] x1 + [0] p(isQid#) = [2] p(nil#) = [0] p(o#) = [2] p(u#) = [1] p(c_1) = [0] p(c_2) = [1] x1 + [2] p(c_3) = [1] p(c_4) = [1] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [1] x1 + [0] p(c_8) = [2] p(c_9) = [1] p(c_10) = [1] x3 + [0] p(c_11) = [0] p(c_12) = [1] p(c_13) = [0] p(c_14) = [0] p(c_15) = [1] p(c_16) = [1] p(c_17) = [1] x1 + [1] p(c_18) = [1] p(c_19) = [1] x1 + [1] p(c_20) = [1] p(c_21) = [1] p(c_22) = [0] p(c_23) = [1] p(c_24) = [1] p(c_25) = [1] x1 + [0] p(c_26) = [1] x1 + [1] x2 + [0] p(c_27) = [0] p(c_28) = [1] x2 + [1] p(c_29) = [1] x1 + [1] x2 + [0] p(c_30) = [1] x1 + [1] x2 + [4] p(c_31) = [4] x1 + [2] x3 + [2] p(c_32) = [2] x1 + [4] x2 + [1] x3 + [0] p(c_33) = [1] p(c_34) = [0] p(c_35) = [0] p(c_36) = [1] p(c_37) = [0] p(c_38) = [1] p(c_39) = [1] p(c_40) = [0] p(c_41) = [0] Following rules are strictly oriented: U21#(tt(),V2) = [4] V2 + [4] > [4] V2 + [2] = c_2(isList#(activate(V2))) Following rules are (at-least) weakly oriented: U41#(tt(),V2) = [4] V2 + [0] >= [4] V2 + [0] = c_5(isNeList#(activate(V2))) U51#(tt(),V2) = [4] V2 + [0] >= [4] V2 + [0] = c_7(isList#(activate(V2))) isList#(V) = [4] V + [0] >= [4] V + [0] = c_25(isNeList#(activate(V))) isList#(n____(V1,V2)) = [4] V1 + [4] V2 + [4] >= [4] V1 + [4] V2 + [4] = c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) = [4] V1 + [4] V2 + [4] >= [4] V1 + [4] V2 + [4] = c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) = [4] V1 + [4] V2 + [4] >= [4] V1 + [4] V2 + [4] = c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) U11(tt()) = [0] >= [0] = tt() U21(tt(),V2) = [0] >= [0] = U22(isList(activate(V2))) U22(tt()) = [0] >= [0] = tt() __(X1,X2) = [1] X1 + [1] X2 + [1] >= [1] X1 + [1] X2 + [1] = n____(X1,X2) a() = [0] >= [0] = n__a() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n____(X1,X2)) = [1] X1 + [1] X2 + [1] >= [1] X1 + [1] X2 + [1] = __(X1,X2) activate(n__a()) = [0] >= [0] = a() activate(n__e()) = [0] >= [0] = e() activate(n__i()) = [0] >= [0] = i() activate(n__nil()) = [0] >= [0] = nil() activate(n__o()) = [0] >= [0] = o() activate(n__u()) = [1] >= [1] = u() e() = [0] >= [0] = n__e() i() = [0] >= [0] = n__i() isList(V) = [1] >= [0] = U11(isNeList(activate(V))) isList(n____(V1,V2)) = [1] >= [1] = U21(isList(activate(V1)),activate(V2)) isList(n__nil()) = [1] >= [0] = tt() nil() = [0] >= [0] = n__nil() o() = [0] >= [0] = n__o() u() = [1] >= [1] = n__u() ** Step 12.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: U41#(tt(),V2) -> c_5(isNeList#(activate(V2))) U51#(tt(),V2) -> c_7(isList#(activate(V2))) isList#(V) -> c_25(isNeList#(activate(V))) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) - Weak DPs: U21#(tt(),V2) -> c_2(isList#(activate(V2))) - Weak TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0,U11#/1,U21#/2,U22#/1,U31#/1,U41#/2,U42#/1 ,U51#/2,U52#/1,U61#/1,U71#/2,U72#/1,U81#/1,__#/2,a#/0,activate#/1,e#/0,i#/0,isList#/1,isNeList#/1,isNePal#/1 ,isPal#/1,isQid#/1,nil#/0,o#/0,u#/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0,n__o/0,n__u/0,tt/0,c_1/0,c_2/1 ,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/2,c_27/0,c_28/3,c_29/2,c_30/2,c_31/3,c_32/3,c_33/0 ,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72# ,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} and constructors {n____ ,n__a,n__e,n__i,n__nil,n__o,n__u,tt} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ** Step 12.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: U41#(tt(),V2) -> c_5(isNeList#(activate(V2))) U51#(tt(),V2) -> c_7(isList#(activate(V2))) isList#(V) -> c_25(isNeList#(activate(V))) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) - Weak DPs: U21#(tt(),V2) -> c_2(isList#(activate(V2))) - Weak TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0,U11#/1,U21#/2,U22#/1,U31#/1,U41#/2,U42#/1 ,U51#/2,U52#/1,U61#/1,U71#/2,U72#/1,U81#/1,__#/2,a#/0,activate#/1,e#/0,i#/0,isList#/1,isNeList#/1,isNePal#/1 ,isPal#/1,isQid#/1,nil#/0,o#/0,u#/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0,n__o/0,n__u/0,tt/0,c_1/0,c_2/1 ,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/2,c_27/0,c_28/3,c_29/2,c_30/2,c_31/3,c_32/3,c_33/0 ,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72# ,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} and constructors {n____ ,n__a,n__e,n__i,n__nil,n__o,n__u,tt} + 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: 2: U51#(tt(),V2) -> c_7(isList#(activate(V2))) 4: isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) 5: isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) Consider the set of all dependency pairs 1: U41#(tt(),V2) -> c_5(isNeList#(activate(V2))) 2: U51#(tt(),V2) -> c_7(isList#(activate(V2))) 3: isList#(V) -> c_25(isNeList#(activate(V))) 4: isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) 5: isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) 6: isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) 7: U21#(tt(),V2) -> c_2(isList#(activate(V2))) Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1)) SPACE(?,?)on application of the dependency pairs {2,4,5} These cover all (indirect) predecessors of dependency pairs {1,2,3,4,5,7} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. *** Step 12.b:1.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: U41#(tt(),V2) -> c_5(isNeList#(activate(V2))) U51#(tt(),V2) -> c_7(isList#(activate(V2))) isList#(V) -> c_25(isNeList#(activate(V))) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) - Weak DPs: U21#(tt(),V2) -> c_2(isList#(activate(V2))) - Weak TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0,U11#/1,U21#/2,U22#/1,U31#/1,U41#/2,U42#/1 ,U51#/2,U52#/1,U61#/1,U71#/2,U72#/1,U81#/1,__#/2,a#/0,activate#/1,e#/0,i#/0,isList#/1,isNeList#/1,isNePal#/1 ,isPal#/1,isQid#/1,nil#/0,o#/0,u#/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0,n__o/0,n__u/0,tt/0,c_1/0,c_2/1 ,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/2,c_27/0,c_28/3,c_29/2,c_30/2,c_31/3,c_32/3,c_33/0 ,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72# ,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} and constructors {n____ ,n__a,n__e,n__i,n__nil,n__o,n__u,tt} + 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_2) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1}, uargs(c_25) = {1}, uargs(c_26) = {1,2}, uargs(c_29) = {1,2}, uargs(c_30) = {1,2} Following symbols are considered usable: {U31,U41,U42,U51,U52,__,a,activate,e,i,isNeList,nil,o,u,U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71# ,U72#,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} TcT has computed the following interpretation: p(U11) = [1] x1 + [0] p(U21) = [1] x1 + [1] x2 + [7] p(U22) = [1] x1 + [2] p(U31) = [4] p(U41) = [4] p(U42) = [4] p(U51) = [4] p(U52) = [4] p(U61) = [1] p(U71) = [1] x1 + [1] p(U72) = [0] p(U81) = [1] x1 + [2] p(__) = [1] x1 + [1] x2 + [7] p(a) = [2] p(activate) = [1] x1 + [0] p(e) = [0] p(i) = [0] p(isList) = [0] p(isNeList) = [4] p(isNePal) = [4] p(isPal) = [0] p(isQid) = [0] p(n____) = [1] x1 + [1] x2 + [7] p(n__a) = [2] p(n__e) = [0] p(n__i) = [0] p(n__nil) = [0] p(n__o) = [0] p(n__u) = [0] p(nil) = [0] p(o) = [0] p(tt) = [0] p(u) = [0] p(U11#) = [0] p(U21#) = [2] x2 + [0] p(U22#) = [0] p(U31#) = [0] p(U41#) = [2] x2 + [0] p(U42#) = [1] x1 + [0] p(U51#) = [3] x1 + [2] x2 + [2] p(U52#) = [0] p(U61#) = [0] p(U71#) = [0] p(U72#) = [2] p(U81#) = [1] p(__#) = [1] x1 + [0] p(a#) = [0] p(activate#) = [0] p(e#) = [1] p(i#) = [1] p(isList#) = [2] x1 + [0] p(isNeList#) = [2] x1 + [0] p(isNePal#) = [4] p(isPal#) = [1] p(isQid#) = [4] x1 + [0] p(nil#) = [1] p(o#) = [2] p(u#) = [0] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [1] p(c_7) = [1] x1 + [1] p(c_8) = [1] p(c_9) = [4] p(c_10) = [1] x1 + [4] x2 + [4] x3 + [0] p(c_11) = [1] p(c_12) = [2] p(c_13) = [1] p(c_14) = [0] p(c_15) = [1] p(c_16) = [2] p(c_17) = [4] x1 + [1] p(c_18) = [1] p(c_19) = [1] p(c_20) = [4] x1 + [1] p(c_21) = [4] x1 + [0] p(c_22) = [4] x1 + [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [1] x1 + [0] p(c_26) = [1] x1 + [1] x2 + [0] p(c_27) = [2] p(c_28) = [4] p(c_29) = [1] x1 + [1] x2 + [0] p(c_30) = [1] x1 + [1] x2 + [0] p(c_31) = [1] x3 + [4] p(c_32) = [4] x1 + [1] x2 + [4] x3 + [1] p(c_33) = [2] p(c_34) = [2] p(c_35) = [1] p(c_36) = [1] p(c_37) = [1] p(c_38) = [1] p(c_39) = [0] p(c_40) = [1] p(c_41) = [1] Following rules are strictly oriented: U51#(tt(),V2) = [2] V2 + [2] > [2] V2 + [1] = c_7(isList#(activate(V2))) isList#(n____(V1,V2)) = [2] V1 + [2] V2 + [14] > [2] V1 + [2] V2 + [0] = c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) = [2] V1 + [2] V2 + [14] > [2] V1 + [2] V2 + [0] = c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) Following rules are (at-least) weakly oriented: U21#(tt(),V2) = [2] V2 + [0] >= [2] V2 + [0] = c_2(isList#(activate(V2))) U41#(tt(),V2) = [2] V2 + [0] >= [2] V2 + [0] = c_5(isNeList#(activate(V2))) isList#(V) = [2] V + [0] >= [2] V + [0] = c_25(isNeList#(activate(V))) isNeList#(n____(V1,V2)) = [2] V1 + [2] V2 + [14] >= [2] V1 + [2] V2 + [14] = c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) U31(tt()) = [4] >= [0] = tt() U41(tt(),V2) = [4] >= [4] = U42(isNeList(activate(V2))) U42(tt()) = [4] >= [0] = tt() U51(tt(),V2) = [4] >= [4] = U52(isList(activate(V2))) U52(tt()) = [4] >= [0] = tt() __(X1,X2) = [1] X1 + [1] X2 + [7] >= [1] X1 + [1] X2 + [7] = n____(X1,X2) a() = [2] >= [2] = n__a() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n____(X1,X2)) = [1] X1 + [1] X2 + [7] >= [1] X1 + [1] X2 + [7] = __(X1,X2) activate(n__a()) = [2] >= [2] = a() activate(n__e()) = [0] >= [0] = e() activate(n__i()) = [0] >= [0] = i() activate(n__nil()) = [0] >= [0] = nil() activate(n__o()) = [0] >= [0] = o() activate(n__u()) = [0] >= [0] = u() e() = [0] >= [0] = n__e() i() = [0] >= [0] = n__i() isNeList(V) = [4] >= [4] = U31(isQid(activate(V))) isNeList(n____(V1,V2)) = [4] >= [4] = U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) = [4] >= [4] = U51(isNeList(activate(V1)),activate(V2)) nil() = [0] >= [0] = n__nil() o() = [0] >= [0] = n__o() u() = [0] >= [0] = n__u() *** Step 12.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: U41#(tt(),V2) -> c_5(isNeList#(activate(V2))) isList#(V) -> c_25(isNeList#(activate(V))) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) - Weak DPs: U21#(tt(),V2) -> c_2(isList#(activate(V2))) U51#(tt(),V2) -> c_7(isList#(activate(V2))) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) - Weak TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0,U11#/1,U21#/2,U22#/1,U31#/1,U41#/2,U42#/1 ,U51#/2,U52#/1,U61#/1,U71#/2,U72#/1,U81#/1,__#/2,a#/0,activate#/1,e#/0,i#/0,isList#/1,isNeList#/1,isNePal#/1 ,isPal#/1,isQid#/1,nil#/0,o#/0,u#/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0,n__o/0,n__u/0,tt/0,c_1/0,c_2/1 ,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/2,c_27/0,c_28/3,c_29/2,c_30/2,c_31/3,c_32/3,c_33/0 ,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72# ,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} and constructors {n____ ,n__a,n__e,n__i,n__nil,n__o,n__u,tt} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () *** Step 12.b:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) - Weak DPs: U21#(tt(),V2) -> c_2(isList#(activate(V2))) U41#(tt(),V2) -> c_5(isNeList#(activate(V2))) U51#(tt(),V2) -> c_7(isList#(activate(V2))) isList#(V) -> c_25(isNeList#(activate(V))) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) - Weak TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0,U11#/1,U21#/2,U22#/1,U31#/1,U41#/2,U42#/1 ,U51#/2,U52#/1,U61#/1,U71#/2,U72#/1,U81#/1,__#/2,a#/0,activate#/1,e#/0,i#/0,isList#/1,isNeList#/1,isNePal#/1 ,isPal#/1,isQid#/1,nil#/0,o#/0,u#/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0,n__o/0,n__u/0,tt/0,c_1/0,c_2/1 ,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/2,c_27/0,c_28/3,c_29/2,c_30/2,c_31/3,c_32/3,c_33/0 ,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72# ,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} and constructors {n____ ,n__a,n__e,n__i,n__nil,n__o,n__u,tt} + 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: isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) Consider the set of all dependency pairs 1: isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) 2: U21#(tt(),V2) -> c_2(isList#(activate(V2))) 3: U41#(tt(),V2) -> c_5(isNeList#(activate(V2))) 4: U51#(tt(),V2) -> c_7(isList#(activate(V2))) 5: isList#(V) -> c_25(isNeList#(activate(V))) 6: isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) 7: isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1)) SPACE(?,?)on application of the dependency pairs {1} These cover all (indirect) predecessors of dependency pairs {1,4} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. **** Step 12.b:1.b:1.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) - Weak DPs: U21#(tt(),V2) -> c_2(isList#(activate(V2))) U41#(tt(),V2) -> c_5(isNeList#(activate(V2))) U51#(tt(),V2) -> c_7(isList#(activate(V2))) isList#(V) -> c_25(isNeList#(activate(V))) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) - Weak TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0,U11#/1,U21#/2,U22#/1,U31#/1,U41#/2,U42#/1 ,U51#/2,U52#/1,U61#/1,U71#/2,U72#/1,U81#/1,__#/2,a#/0,activate#/1,e#/0,i#/0,isList#/1,isNeList#/1,isNePal#/1 ,isPal#/1,isQid#/1,nil#/0,o#/0,u#/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0,n__o/0,n__u/0,tt/0,c_1/0,c_2/1 ,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/2,c_27/0,c_28/3,c_29/2,c_30/2,c_31/3,c_32/3,c_33/0 ,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72# ,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} and constructors {n____ ,n__a,n__e,n__i,n__nil,n__o,n__u,tt} + 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_2) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1}, uargs(c_25) = {1}, uargs(c_26) = {1,2}, uargs(c_29) = {1,2}, uargs(c_30) = {1,2} Following symbols are considered usable: {U31,U41,U42,U51,U52,__,a,activate,e,i,isNeList,nil,o,u,U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71# ,U72#,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} TcT has computed the following interpretation: p(U11) = [3] x1 + [6] p(U21) = [1] x2 + [0] p(U22) = [5] p(U31) = [1] p(U41) = [0] p(U42) = [0] p(U51) = [0] p(U52) = [0] p(U61) = [2] p(U71) = [1] x2 + [1] p(U72) = [1] x1 + [0] p(U81) = [2] p(__) = [1] x1 + [1] x2 + [7] p(a) = [2] p(activate) = [1] x1 + [0] p(e) = [0] p(i) = [0] p(isList) = [0] p(isNeList) = [2] p(isNePal) = [4] x1 + [0] p(isPal) = [0] p(isQid) = [0] p(n____) = [1] x1 + [1] x2 + [7] p(n__a) = [2] p(n__e) = [0] p(n__i) = [0] p(n__nil) = [0] p(n__o) = [0] p(n__u) = [1] p(nil) = [0] p(o) = [0] p(tt) = [0] p(u) = [1] p(U11#) = [4] x1 + [0] p(U21#) = [1] x2 + [0] p(U22#) = [1] x1 + [2] p(U31#) = [1] x1 + [2] p(U41#) = [1] x2 + [0] p(U42#) = [0] p(U51#) = [3] x1 + [1] x2 + [0] p(U52#) = [4] x1 + [1] p(U61#) = [1] p(U71#) = [1] x1 + [1] p(U72#) = [4] x1 + [4] p(U81#) = [4] x1 + [2] p(__#) = [0] p(a#) = [0] p(activate#) = [2] x1 + [1] p(e#) = [1] p(i#) = [1] p(isList#) = [1] x1 + [0] p(isNeList#) = [1] x1 + [0] p(isNePal#) = [2] x1 + [1] p(isPal#) = [0] p(isQid#) = [2] x1 + [1] p(nil#) = [2] p(o#) = [0] p(u#) = [2] p(c_1) = [1] p(c_2) = [1] x1 + [0] p(c_3) = [4] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [1] x1 + [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [2] p(c_13) = [0] p(c_14) = [1] p(c_15) = [1] p(c_16) = [4] p(c_17) = [0] p(c_18) = [0] p(c_19) = [4] x1 + [2] p(c_20) = [0] p(c_21) = [1] x1 + [2] p(c_22) = [1] x1 + [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [1] x1 + [0] p(c_26) = [1] x1 + [1] x2 + [0] p(c_27) = [4] p(c_28) = [1] x1 + [4] x3 + [1] p(c_29) = [1] x1 + [1] x2 + [0] p(c_30) = [1] x1 + [1] x2 + [0] p(c_31) = [0] p(c_32) = [1] p(c_33) = [1] p(c_34) = [2] p(c_35) = [0] p(c_36) = [2] p(c_37) = [0] p(c_38) = [0] p(c_39) = [0] p(c_40) = [0] p(c_41) = [2] Following rules are strictly oriented: isNeList#(n____(V1,V2)) = [1] V1 + [1] V2 + [7] > [1] V1 + [1] V2 + [6] = c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) Following rules are (at-least) weakly oriented: U21#(tt(),V2) = [1] V2 + [0] >= [1] V2 + [0] = c_2(isList#(activate(V2))) U41#(tt(),V2) = [1] V2 + [0] >= [1] V2 + [0] = c_5(isNeList#(activate(V2))) U51#(tt(),V2) = [1] V2 + [0] >= [1] V2 + [0] = c_7(isList#(activate(V2))) isList#(V) = [1] V + [0] >= [1] V + [0] = c_25(isNeList#(activate(V))) isList#(n____(V1,V2)) = [1] V1 + [1] V2 + [7] >= [1] V1 + [1] V2 + [0] = c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) = [1] V1 + [1] V2 + [7] >= [1] V1 + [1] V2 + [0] = c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) U31(tt()) = [1] >= [0] = tt() U41(tt(),V2) = [0] >= [0] = U42(isNeList(activate(V2))) U42(tt()) = [0] >= [0] = tt() U51(tt(),V2) = [0] >= [0] = U52(isList(activate(V2))) U52(tt()) = [0] >= [0] = tt() __(X1,X2) = [1] X1 + [1] X2 + [7] >= [1] X1 + [1] X2 + [7] = n____(X1,X2) a() = [2] >= [2] = n__a() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n____(X1,X2)) = [1] X1 + [1] X2 + [7] >= [1] X1 + [1] X2 + [7] = __(X1,X2) activate(n__a()) = [2] >= [2] = a() activate(n__e()) = [0] >= [0] = e() activate(n__i()) = [0] >= [0] = i() activate(n__nil()) = [0] >= [0] = nil() activate(n__o()) = [0] >= [0] = o() activate(n__u()) = [1] >= [1] = u() e() = [0] >= [0] = n__e() i() = [0] >= [0] = n__i() isNeList(V) = [2] >= [1] = U31(isQid(activate(V))) isNeList(n____(V1,V2)) = [2] >= [0] = U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) = [2] >= [0] = U51(isNeList(activate(V1)),activate(V2)) nil() = [0] >= [0] = n__nil() o() = [0] >= [0] = n__o() u() = [1] >= [1] = n__u() **** Step 12.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: U21#(tt(),V2) -> c_2(isList#(activate(V2))) U41#(tt(),V2) -> c_5(isNeList#(activate(V2))) U51#(tt(),V2) -> c_7(isList#(activate(V2))) isList#(V) -> c_25(isNeList#(activate(V))) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) - Weak TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0,U11#/1,U21#/2,U22#/1,U31#/1,U41#/2,U42#/1 ,U51#/2,U52#/1,U61#/1,U71#/2,U72#/1,U81#/1,__#/2,a#/0,activate#/1,e#/0,i#/0,isList#/1,isNeList#/1,isNePal#/1 ,isPal#/1,isQid#/1,nil#/0,o#/0,u#/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0,n__o/0,n__u/0,tt/0,c_1/0,c_2/1 ,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/2,c_27/0,c_28/3,c_29/2,c_30/2,c_31/3,c_32/3,c_33/0 ,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72# ,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} and constructors {n____ ,n__a,n__e,n__i,n__nil,n__o,n__u,tt} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 12.b:1.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: U21#(tt(),V2) -> c_2(isList#(activate(V2))) U41#(tt(),V2) -> c_5(isNeList#(activate(V2))) U51#(tt(),V2) -> c_7(isList#(activate(V2))) isList#(V) -> c_25(isNeList#(activate(V))) isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) - Weak TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0,U11#/1,U21#/2,U22#/1,U31#/1,U41#/2,U42#/1 ,U51#/2,U52#/1,U61#/1,U71#/2,U72#/1,U81#/1,__#/2,a#/0,activate#/1,e#/0,i#/0,isList#/1,isNeList#/1,isNePal#/1 ,isPal#/1,isQid#/1,nil#/0,o#/0,u#/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0,n__o/0,n__u/0,tt/0,c_1/0,c_2/1 ,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/2,c_27/0,c_28/3,c_29/2,c_30/2,c_31/3,c_32/3,c_33/0 ,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72# ,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} and constructors {n____ ,n__a,n__e,n__i,n__nil,n__o,n__u,tt} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:U21#(tt(),V2) -> c_2(isList#(activate(V2))) -->_1 isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))):5 -->_1 isList#(V) -> c_25(isNeList#(activate(V))):4 2:W:U41#(tt(),V2) -> c_5(isNeList#(activate(V2))) -->_1 isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1))):7 -->_1 isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))):6 3:W:U51#(tt(),V2) -> c_7(isList#(activate(V2))) -->_1 isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))):5 -->_1 isList#(V) -> c_25(isNeList#(activate(V))):4 4:W:isList#(V) -> c_25(isNeList#(activate(V))) -->_1 isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1))):7 -->_1 isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))):6 5:W:isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) -->_2 isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))):5 -->_2 isList#(V) -> c_25(isNeList#(activate(V))):4 -->_1 U21#(tt(),V2) -> c_2(isList#(activate(V2))):1 6:W:isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) -->_2 isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))):5 -->_2 isList#(V) -> c_25(isNeList#(activate(V))):4 -->_1 U41#(tt(),V2) -> c_5(isNeList#(activate(V2))):2 7:W:isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) -->_2 isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1))):7 -->_2 isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))):6 -->_1 U51#(tt(),V2) -> c_7(isList#(activate(V2))):3 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: U21#(tt(),V2) -> c_2(isList#(activate(V2))) 5: isList#(n____(V1,V2)) -> c_26(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) 6: isNeList#(n____(V1,V2)) -> c_29(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) 7: isNeList#(n____(V1,V2)) -> c_30(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) 4: isList#(V) -> c_25(isNeList#(activate(V))) 3: U51#(tt(),V2) -> c_7(isList#(activate(V2))) 2: U41#(tt(),V2) -> c_5(isNeList#(activate(V2))) **** Step 12.b:1.b:1.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: U11(tt()) -> tt() U21(tt(),V2) -> U22(isList(activate(V2))) U22(tt()) -> tt() U31(tt()) -> tt() U41(tt(),V2) -> U42(isNeList(activate(V2))) U42(tt()) -> tt() U51(tt(),V2) -> U52(isList(activate(V2))) U52(tt()) -> tt() __(X1,X2) -> n____(X1,X2) a() -> n__a() activate(X) -> X activate(n____(X1,X2)) -> __(X1,X2) activate(n__a()) -> a() activate(n__e()) -> e() activate(n__i()) -> i() activate(n__nil()) -> nil() activate(n__o()) -> o() activate(n__u()) -> u() e() -> n__e() i() -> n__i() isList(V) -> U11(isNeList(activate(V))) isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2)) isList(n__nil()) -> tt() isNeList(V) -> U31(isQid(activate(V))) isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2)) isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() o() -> n__o() u() -> n__u() - Signature: {U11/1,U21/2,U22/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/1,U71/2,U72/1,U81/1,__/2,a/0,activate/1,e/0,i/0 ,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,u/0,U11#/1,U21#/2,U22#/1,U31#/1,U41#/2,U42#/1 ,U51#/2,U52#/1,U61#/1,U71#/2,U72#/1,U81#/1,__#/2,a#/0,activate#/1,e#/0,i#/0,isList#/1,isNeList#/1,isNePal#/1 ,isPal#/1,isQid#/1,nil#/0,o#/0,u#/0} / {n____/2,n__a/0,n__e/0,n__i/0,n__nil/0,n__o/0,n__u/0,tt/0,c_1/0,c_2/1 ,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/1,c_17/1,c_18/1 ,c_19/1,c_20/1,c_21/1,c_22/1,c_23/0,c_24/0,c_25/1,c_26/2,c_27/0,c_28/3,c_29/2,c_30/2,c_31/3,c_32/3,c_33/0 ,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,U21#,U22#,U31#,U41#,U42#,U51#,U52#,U61#,U71#,U72# ,U81#,__#,a#,activate#,e#,i#,isList#,isNeList#,isNePal#,isPal#,isQid#,nil#,o#,u#} and constructors {n____ ,n__a,n__e,n__i,n__nil,n__o,n__u,tt} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))