WORST_CASE(?,O(n^2)) * Step 1: DependencyPairs WORST_CASE(?,O(n^2)) + 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)) -> __(activate(X1),activate(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,n____(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: 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() __#(X,nil()) -> c_13() __#(X1,X2) -> c_14() __#(__(X,Y),Z) -> c_15(__#(X,__(Y,Z)),__#(Y,Z)) __#(nil(),X) -> c_16() a#() -> c_17() activate#(X) -> c_18() activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__a()) -> c_20(a#()) activate#(n__e()) -> c_21(e#()) activate#(n__i()) -> c_22(i#()) activate#(n__nil()) -> c_23(nil#()) activate#(n__o()) -> c_24(o#()) activate#(n__u()) -> c_25(u#()) e#() -> c_26() i#() -> c_27() isList#(V) -> c_28(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isList#(n__nil()) -> c_30() isNeList#(V) -> c_31(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNePal#(V) -> c_34(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P)) ,isQid#(activate(I)) ,activate#(I) ,activate#(P)) isPal#(V) -> c_36(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) isPal#(n__nil()) -> c_37() isQid#(n__a()) -> c_38() isQid#(n__e()) -> c_39() isQid#(n__i()) -> c_40() isQid#(n__o()) -> c_41() isQid#(n__u()) -> c_42() nil#() -> c_43() o#() -> c_44() u#() -> c_45() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^2)) + 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() __#(X,nil()) -> c_13() __#(X1,X2) -> c_14() __#(__(X,Y),Z) -> c_15(__#(X,__(Y,Z)),__#(Y,Z)) __#(nil(),X) -> c_16() a#() -> c_17() activate#(X) -> c_18() activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__a()) -> c_20(a#()) activate#(n__e()) -> c_21(e#()) activate#(n__i()) -> c_22(i#()) activate#(n__nil()) -> c_23(nil#()) activate#(n__o()) -> c_24(o#()) activate#(n__u()) -> c_25(u#()) e#() -> c_26() i#() -> c_27() isList#(V) -> c_28(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isList#(n__nil()) -> c_30() isNeList#(V) -> c_31(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNePal#(V) -> c_34(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P)) ,isQid#(activate(I)) ,activate#(I) ,activate#(P)) isPal#(V) -> c_36(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) isPal#(n__nil()) -> c_37() isQid#(n__a()) -> c_38() isQid#(n__e()) -> c_39() isQid#(n__i()) -> c_40() isQid#(n__o()) -> c_41() isQid#(n__u()) -> c_42() nil#() -> c_43() o#() -> c_44() u#() -> c_45() - 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() __(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)) -> __(activate(X1),activate(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,n____(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,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/2,c_16/0,c_17/0,c_18/0 ,c_19/3,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/3,c_29/4,c_30/0,c_31/3,c_32/4,c_33/4 ,c_34/3,c_35/4,c_36/3,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/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,16,17,18,26,27,30,37,38,39,40,41,42,43,44,45} by application of Pre({1,3,4,6,8,9,11,12,13,14,15,16,17,18,26,27,30,37,38,39,40,41,42,43,44,45}) = {2,5,7,10,19,20,21,22,23 ,24,25,28,29,31,32,33,34,35,36}. 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: __#(X,nil()) -> c_13() 14: __#(X1,X2) -> c_14() 15: __#(__(X,Y),Z) -> c_15(__#(X,__(Y,Z)),__#(Y,Z)) 16: __#(nil(),X) -> c_16() 17: a#() -> c_17() 18: activate#(X) -> c_18() 19: activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 20: activate#(n__a()) -> c_20(a#()) 21: activate#(n__e()) -> c_21(e#()) 22: activate#(n__i()) -> c_22(i#()) 23: activate#(n__nil()) -> c_23(nil#()) 24: activate#(n__o()) -> c_24(o#()) 25: activate#(n__u()) -> c_25(u#()) 26: e#() -> c_26() 27: i#() -> c_27() 28: isList#(V) -> c_28(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) 29: isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 30: isList#(n__nil()) -> c_30() 31: isNeList#(V) -> c_31(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) 32: isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 33: isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 34: isNePal#(V) -> c_34(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) 35: isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P)) ,isQid#(activate(I)) ,activate#(I) ,activate#(P)) 36: isPal#(V) -> c_36(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) 37: isPal#(n__nil()) -> c_37() 38: isQid#(n__a()) -> c_38() 39: isQid#(n__e()) -> c_39() 40: isQid#(n__i()) -> c_40() 41: isQid#(n__o()) -> c_41() 42: isQid#(n__u()) -> c_42() 43: nil#() -> c_43() 44: o#() -> c_44() 45: u#() -> c_45() * Step 3: PredecessorEstimation WORST_CASE(?,O(n^2)) + 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_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__a()) -> c_20(a#()) activate#(n__e()) -> c_21(e#()) activate#(n__i()) -> c_22(i#()) activate#(n__nil()) -> c_23(nil#()) activate#(n__o()) -> c_24(o#()) activate#(n__u()) -> c_25(u#()) isList#(V) -> c_28(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(V) -> c_31(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNePal#(V) -> c_34(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P)) ,isQid#(activate(I)) ,activate#(I) ,activate#(P)) isPal#(V) -> c_36(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() __#(X,nil()) -> c_13() __#(X1,X2) -> c_14() __#(__(X,Y),Z) -> c_15(__#(X,__(Y,Z)),__#(Y,Z)) __#(nil(),X) -> c_16() a#() -> c_17() activate#(X) -> c_18() e#() -> c_26() i#() -> c_27() isList#(n__nil()) -> c_30() isPal#(n__nil()) -> c_37() isQid#(n__a()) -> c_38() isQid#(n__e()) -> c_39() isQid#(n__i()) -> c_40() isQid#(n__o()) -> c_41() isQid#(n__u()) -> c_42() nil#() -> c_43() o#() -> c_44() u#() -> c_45() - 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() __(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)) -> __(activate(X1),activate(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,n____(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,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/2,c_16/0,c_17/0,c_18/0 ,c_19/3,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/3,c_29/4,c_30/0,c_31/3,c_32/4,c_33/4 ,c_34/3,c_35/4,c_36/3,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/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 {6,7,8,9,10,11} by application of Pre({6,7,8,9,10,11}) = {1,2,3,4,5,12,13,14,15,16,17,18,19}. 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_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 6: activate#(n__a()) -> c_20(a#()) 7: activate#(n__e()) -> c_21(e#()) 8: activate#(n__i()) -> c_22(i#()) 9: activate#(n__nil()) -> c_23(nil#()) 10: activate#(n__o()) -> c_24(o#()) 11: activate#(n__u()) -> c_25(u#()) 12: isList#(V) -> c_28(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) 13: isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 14: isNeList#(V) -> c_31(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) 15: isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 16: isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) 17: isNePal#(V) -> c_34(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) 18: isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P)) ,isQid#(activate(I)) ,activate#(I) ,activate#(P)) 19: isPal#(V) -> c_36(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) 20: U11#(tt()) -> c_1() 21: U22#(tt()) -> c_3() 22: U31#(tt()) -> c_4() 23: U42#(tt()) -> c_6() 24: U52#(tt()) -> c_8() 25: U61#(tt()) -> c_9() 26: U72#(tt()) -> c_11() 27: U81#(tt()) -> c_12() 28: __#(X,nil()) -> c_13() 29: __#(X1,X2) -> c_14() 30: __#(__(X,Y),Z) -> c_15(__#(X,__(Y,Z)),__#(Y,Z)) 31: __#(nil(),X) -> c_16() 32: a#() -> c_17() 33: activate#(X) -> c_18() 34: e#() -> c_26() 35: i#() -> c_27() 36: isList#(n__nil()) -> c_30() 37: isPal#(n__nil()) -> c_37() 38: isQid#(n__a()) -> c_38() 39: isQid#(n__e()) -> c_39() 40: isQid#(n__i()) -> c_40() 41: isQid#(n__o()) -> c_41() 42: isQid#(n__u()) -> c_42() 43: nil#() -> c_43() 44: o#() -> c_44() 45: u#() -> c_45() * Step 4: RemoveWeakSuffixes WORST_CASE(?,O(n^2)) + 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_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) isList#(V) -> c_28(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(V) -> c_31(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNePal#(V) -> c_34(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P)) ,isQid#(activate(I)) ,activate#(I) ,activate#(P)) isPal#(V) -> c_36(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() __#(X,nil()) -> c_13() __#(X1,X2) -> c_14() __#(__(X,Y),Z) -> c_15(__#(X,__(Y,Z)),__#(Y,Z)) __#(nil(),X) -> c_16() a#() -> c_17() activate#(X) -> c_18() activate#(n__a()) -> c_20(a#()) activate#(n__e()) -> c_21(e#()) activate#(n__i()) -> c_22(i#()) activate#(n__nil()) -> c_23(nil#()) activate#(n__o()) -> c_24(o#()) activate#(n__u()) -> c_25(u#()) e#() -> c_26() i#() -> c_27() isList#(n__nil()) -> c_30() isPal#(n__nil()) -> c_37() isQid#(n__a()) -> c_38() isQid#(n__e()) -> c_39() isQid#(n__i()) -> c_40() isQid#(n__o()) -> c_41() isQid#(n__u()) -> c_42() nil#() -> c_43() o#() -> c_44() u#() -> c_45() - 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() __(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)) -> __(activate(X1),activate(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,n____(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,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/2,c_16/0,c_17/0,c_18/0 ,c_19/3,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/3,c_29/4,c_30/0,c_31/3,c_32/4,c_33/4 ,c_34/3,c_35/4,c_36/3,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/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_25(u#()):33 -->_3 activate#(n__o()) -> c_24(o#()):32 -->_3 activate#(n__nil()) -> c_23(nil#()):31 -->_3 activate#(n__i()) -> c_22(i#()):30 -->_3 activate#(n__e()) -> c_21(e#()):29 -->_3 activate#(n__a()) -> c_20(a#()):28 -->_2 isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_2 isList#(V) -> c_28(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)):6 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 isList#(n__nil()) -> c_30():36 -->_3 activate#(X) -> c_18():27 -->_1 U22#(tt()) -> c_3():15 2:S:U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)) -->_3 activate#(n__u()) -> c_25(u#()):33 -->_3 activate#(n__o()) -> c_24(o#()):32 -->_3 activate#(n__nil()) -> c_23(nil#()):31 -->_3 activate#(n__i()) -> c_22(i#()):30 -->_3 activate#(n__e()) -> c_21(e#()):29 -->_3 activate#(n__a()) -> c_20(a#()):28 -->_2 isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)):10 -->_2 isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 -->_2 isNeList#(V) -> c_31(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)):8 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(X) -> c_18():27 -->_1 U42#(tt()) -> c_6():17 3:S:U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) -->_3 activate#(n__u()) -> c_25(u#()):33 -->_3 activate#(n__o()) -> c_24(o#()):32 -->_3 activate#(n__nil()) -> c_23(nil#()):31 -->_3 activate#(n__i()) -> c_22(i#()):30 -->_3 activate#(n__e()) -> c_21(e#()):29 -->_3 activate#(n__a()) -> c_20(a#()):28 -->_2 isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_2 isList#(V) -> c_28(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)):6 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 isList#(n__nil()) -> c_30():36 -->_3 activate#(X) -> c_18():27 -->_1 U52#(tt()) -> c_8():18 4:S:U71#(tt(),P) -> c_10(U72#(isPal(activate(P))),isPal#(activate(P)),activate#(P)) -->_3 activate#(n__u()) -> c_25(u#()):33 -->_3 activate#(n__o()) -> c_24(o#()):32 -->_3 activate#(n__nil()) -> c_23(nil#()):31 -->_3 activate#(n__i()) -> c_22(i#()):30 -->_3 activate#(n__e()) -> c_21(e#()):29 -->_3 activate#(n__a()) -> c_20(a#()):28 -->_2 isPal#(V) -> c_36(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)):13 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 isPal#(n__nil()) -> c_37():37 -->_3 activate#(X) -> c_18():27 -->_1 U72#(tt()) -> c_11():20 5:S:activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__u()) -> c_25(u#()):33 -->_2 activate#(n__u()) -> c_25(u#()):33 -->_3 activate#(n__o()) -> c_24(o#()):32 -->_2 activate#(n__o()) -> c_24(o#()):32 -->_3 activate#(n__nil()) -> c_23(nil#()):31 -->_2 activate#(n__nil()) -> c_23(nil#()):31 -->_3 activate#(n__i()) -> c_22(i#()):30 -->_2 activate#(n__i()) -> c_22(i#()):30 -->_3 activate#(n__e()) -> c_21(e#()):29 -->_2 activate#(n__e()) -> c_21(e#()):29 -->_3 activate#(n__a()) -> c_20(a#()):28 -->_2 activate#(n__a()) -> c_20(a#()):28 -->_3 activate#(X) -> c_18():27 -->_2 activate#(X) -> c_18():27 -->_1 __#(X1,X2) -> c_14():23 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 6:S:isList#(V) -> c_28(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) -->_3 activate#(n__u()) -> c_25(u#()):33 -->_3 activate#(n__o()) -> c_24(o#()):32 -->_3 activate#(n__nil()) -> c_23(nil#()):31 -->_3 activate#(n__i()) -> c_22(i#()):30 -->_3 activate#(n__e()) -> c_21(e#()):29 -->_3 activate#(n__a()) -> c_20(a#()):28 -->_2 isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)):10 -->_2 isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 -->_2 isNeList#(V) -> c_31(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)):8 -->_3 activate#(X) -> c_18():27 -->_1 U11#(tt()) -> c_1():14 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 7:S:isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_4 activate#(n__u()) -> c_25(u#()):33 -->_3 activate#(n__u()) -> c_25(u#()):33 -->_4 activate#(n__o()) -> c_24(o#()):32 -->_3 activate#(n__o()) -> c_24(o#()):32 -->_4 activate#(n__nil()) -> c_23(nil#()):31 -->_3 activate#(n__nil()) -> c_23(nil#()):31 -->_4 activate#(n__i()) -> c_22(i#()):30 -->_3 activate#(n__i()) -> c_22(i#()):30 -->_4 activate#(n__e()) -> c_21(e#()):29 -->_3 activate#(n__e()) -> c_21(e#()):29 -->_4 activate#(n__a()) -> c_20(a#()):28 -->_3 activate#(n__a()) -> c_20(a#()):28 -->_2 isList#(n__nil()) -> c_30():36 -->_4 activate#(X) -> c_18():27 -->_3 activate#(X) -> c_18():27 -->_2 isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_2 isList#(V) -> c_28(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)):6 -->_4 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)):1 8:S:isNeList#(V) -> c_31(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) -->_3 activate#(n__u()) -> c_25(u#()):33 -->_3 activate#(n__o()) -> c_24(o#()):32 -->_3 activate#(n__nil()) -> c_23(nil#()):31 -->_3 activate#(n__i()) -> c_22(i#()):30 -->_3 activate#(n__e()) -> c_21(e#()):29 -->_3 activate#(n__a()) -> c_20(a#()):28 -->_2 isQid#(n__u()) -> c_42():42 -->_2 isQid#(n__o()) -> c_41():41 -->_2 isQid#(n__i()) -> c_40():40 -->_2 isQid#(n__e()) -> c_39():39 -->_2 isQid#(n__a()) -> c_38():38 -->_3 activate#(X) -> c_18():27 -->_1 U31#(tt()) -> c_4():16 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 9:S:isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_4 activate#(n__u()) -> c_25(u#()):33 -->_3 activate#(n__u()) -> c_25(u#()):33 -->_4 activate#(n__o()) -> c_24(o#()):32 -->_3 activate#(n__o()) -> c_24(o#()):32 -->_4 activate#(n__nil()) -> c_23(nil#()):31 -->_3 activate#(n__nil()) -> c_23(nil#()):31 -->_4 activate#(n__i()) -> c_22(i#()):30 -->_3 activate#(n__i()) -> c_22(i#()):30 -->_4 activate#(n__e()) -> c_21(e#()):29 -->_3 activate#(n__e()) -> c_21(e#()):29 -->_4 activate#(n__a()) -> c_20(a#()):28 -->_3 activate#(n__a()) -> c_20(a#()):28 -->_2 isList#(n__nil()) -> c_30():36 -->_4 activate#(X) -> c_18():27 -->_3 activate#(X) -> c_18():27 -->_2 isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_2 isList#(V) -> c_28(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)):6 -->_4 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)):2 10:S:isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_4 activate#(n__u()) -> c_25(u#()):33 -->_3 activate#(n__u()) -> c_25(u#()):33 -->_4 activate#(n__o()) -> c_24(o#()):32 -->_3 activate#(n__o()) -> c_24(o#()):32 -->_4 activate#(n__nil()) -> c_23(nil#()):31 -->_3 activate#(n__nil()) -> c_23(nil#()):31 -->_4 activate#(n__i()) -> c_22(i#()):30 -->_3 activate#(n__i()) -> c_22(i#()):30 -->_4 activate#(n__e()) -> c_21(e#()):29 -->_3 activate#(n__e()) -> c_21(e#()):29 -->_4 activate#(n__a()) -> c_20(a#()):28 -->_3 activate#(n__a()) -> c_20(a#()):28 -->_4 activate#(X) -> c_18():27 -->_3 activate#(X) -> c_18():27 -->_2 isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)):10 -->_2 isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 -->_2 isNeList#(V) -> c_31(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)):8 -->_4 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)):3 11:S:isNePal#(V) -> c_34(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) -->_3 activate#(n__u()) -> c_25(u#()):33 -->_3 activate#(n__o()) -> c_24(o#()):32 -->_3 activate#(n__nil()) -> c_23(nil#()):31 -->_3 activate#(n__i()) -> c_22(i#()):30 -->_3 activate#(n__e()) -> c_21(e#()):29 -->_3 activate#(n__a()) -> c_20(a#()):28 -->_2 isQid#(n__u()) -> c_42():42 -->_2 isQid#(n__o()) -> c_41():41 -->_2 isQid#(n__i()) -> c_40():40 -->_2 isQid#(n__e()) -> c_39():39 -->_2 isQid#(n__a()) -> c_38():38 -->_3 activate#(X) -> c_18():27 -->_1 U61#(tt()) -> c_9():19 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 12:S:isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P)) ,isQid#(activate(I)) ,activate#(I) ,activate#(P)) -->_4 activate#(n__u()) -> c_25(u#()):33 -->_3 activate#(n__u()) -> c_25(u#()):33 -->_4 activate#(n__o()) -> c_24(o#()):32 -->_3 activate#(n__o()) -> c_24(o#()):32 -->_4 activate#(n__nil()) -> c_23(nil#()):31 -->_3 activate#(n__nil()) -> c_23(nil#()):31 -->_4 activate#(n__i()) -> c_22(i#()):30 -->_3 activate#(n__i()) -> c_22(i#()):30 -->_4 activate#(n__e()) -> c_21(e#()):29 -->_3 activate#(n__e()) -> c_21(e#()):29 -->_4 activate#(n__a()) -> c_20(a#()):28 -->_3 activate#(n__a()) -> c_20(a#()):28 -->_2 isQid#(n__u()) -> c_42():42 -->_2 isQid#(n__o()) -> c_41():41 -->_2 isQid#(n__i()) -> c_40():40 -->_2 isQid#(n__e()) -> c_39():39 -->_2 isQid#(n__a()) -> c_38():38 -->_4 activate#(X) -> c_18():27 -->_3 activate#(X) -> c_18():27 -->_4 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 U71#(tt(),P) -> c_10(U72#(isPal(activate(P))),isPal#(activate(P)),activate#(P)):4 13:S:isPal#(V) -> c_36(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) -->_3 activate#(n__u()) -> c_25(u#()):33 -->_3 activate#(n__o()) -> c_24(o#()):32 -->_3 activate#(n__nil()) -> c_23(nil#()):31 -->_3 activate#(n__i()) -> c_22(i#()):30 -->_3 activate#(n__e()) -> c_21(e#()):29 -->_3 activate#(n__a()) -> c_20(a#()):28 -->_3 activate#(X) -> c_18():27 -->_1 U81#(tt()) -> c_12():21 -->_2 isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P)) ,isQid#(activate(I)) ,activate#(I) ,activate#(P)):12 -->_2 isNePal#(V) -> c_34(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)):11 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 14:W:U11#(tt()) -> c_1() 15:W:U22#(tt()) -> c_3() 16:W:U31#(tt()) -> c_4() 17:W:U42#(tt()) -> c_6() 18:W:U52#(tt()) -> c_8() 19:W:U61#(tt()) -> c_9() 20:W:U72#(tt()) -> c_11() 21:W:U81#(tt()) -> c_12() 22:W:__#(X,nil()) -> c_13() 23:W:__#(X1,X2) -> c_14() 24:W:__#(__(X,Y),Z) -> c_15(__#(X,__(Y,Z)),__#(Y,Z)) 25:W:__#(nil(),X) -> c_16() 26:W:a#() -> c_17() 27:W:activate#(X) -> c_18() 28:W:activate#(n__a()) -> c_20(a#()) -->_1 a#() -> c_17():26 29:W:activate#(n__e()) -> c_21(e#()) -->_1 e#() -> c_26():34 30:W:activate#(n__i()) -> c_22(i#()) -->_1 i#() -> c_27():35 31:W:activate#(n__nil()) -> c_23(nil#()) -->_1 nil#() -> c_43():43 32:W:activate#(n__o()) -> c_24(o#()) -->_1 o#() -> c_44():44 33:W:activate#(n__u()) -> c_25(u#()) -->_1 u#() -> c_45():45 34:W:e#() -> c_26() 35:W:i#() -> c_27() 36:W:isList#(n__nil()) -> c_30() 37:W:isPal#(n__nil()) -> c_37() 38:W:isQid#(n__a()) -> c_38() 39:W:isQid#(n__e()) -> c_39() 40:W:isQid#(n__i()) -> c_40() 41:W:isQid#(n__o()) -> c_41() 42:W:isQid#(n__u()) -> c_42() 43:W:nil#() -> c_43() 44:W:o#() -> c_44() 45:W:u#() -> c_45() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 25: __#(nil(),X) -> c_16() 24: __#(__(X,Y),Z) -> c_15(__#(X,__(Y,Z)),__#(Y,Z)) 22: __#(X,nil()) -> c_13() 20: U72#(tt()) -> c_11() 37: isPal#(n__nil()) -> c_37() 19: U61#(tt()) -> c_9() 21: U81#(tt()) -> c_12() 15: U22#(tt()) -> c_3() 14: U11#(tt()) -> c_1() 18: U52#(tt()) -> c_8() 17: U42#(tt()) -> c_6() 16: U31#(tt()) -> c_4() 38: isQid#(n__a()) -> c_38() 39: isQid#(n__e()) -> c_39() 40: isQid#(n__i()) -> c_40() 41: isQid#(n__o()) -> c_41() 42: isQid#(n__u()) -> c_42() 23: __#(X1,X2) -> c_14() 27: activate#(X) -> c_18() 36: isList#(n__nil()) -> c_30() 28: activate#(n__a()) -> c_20(a#()) 26: a#() -> c_17() 29: activate#(n__e()) -> c_21(e#()) 34: e#() -> c_26() 30: activate#(n__i()) -> c_22(i#()) 35: i#() -> c_27() 31: activate#(n__nil()) -> c_23(nil#()) 43: nil#() -> c_43() 32: activate#(n__o()) -> c_24(o#()) 44: o#() -> c_44() 33: activate#(n__u()) -> c_25(u#()) 45: u#() -> c_45() * Step 5: SimplifyRHS WORST_CASE(?,O(n^2)) + 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_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) isList#(V) -> c_28(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(V) -> c_31(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNePal#(V) -> c_34(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P)) ,isQid#(activate(I)) ,activate#(I) ,activate#(P)) isPal#(V) -> c_36(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) - 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() __(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)) -> __(activate(X1),activate(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,n____(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,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/2,c_16/0,c_17/0,c_18/0 ,c_19/3,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/3,c_29/4,c_30/0,c_31/3,c_32/4,c_33/4 ,c_34/3,c_35/4,c_36/3,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/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_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_2 isList#(V) -> c_28(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)):6 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 2:S:U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)) -->_2 isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)):10 -->_2 isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 -->_2 isNeList#(V) -> c_31(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)):8 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 3:S:U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)) -->_2 isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_2 isList#(V) -> c_28(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)):6 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 4:S:U71#(tt(),P) -> c_10(U72#(isPal(activate(P))),isPal#(activate(P)),activate#(P)) -->_2 isPal#(V) -> c_36(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)):13 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 5:S:activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_2 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 6:S:isList#(V) -> c_28(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)) -->_2 isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)):10 -->_2 isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 -->_2 isNeList#(V) -> c_31(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)):8 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 7:S:isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_2 isList#(V) -> c_28(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)):6 -->_4 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 U21#(tt(),V2) -> c_2(U22#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)):1 8:S:isNeList#(V) -> c_31(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 9:S:isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_2 isList#(V) -> c_28(U11#(isNeList(activate(V))),isNeList#(activate(V)),activate#(V)):6 -->_4 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 U41#(tt(),V2) -> c_5(U42#(isNeList(activate(V2))),isNeList#(activate(V2)),activate#(V2)):2 10:S:isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)):10 -->_2 isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 -->_2 isNeList#(V) -> c_31(U31#(isQid(activate(V))),isQid#(activate(V)),activate#(V)):8 -->_4 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 U51#(tt(),V2) -> c_7(U52#(isList(activate(V2))),isList#(activate(V2)),activate#(V2)):3 11:S:isNePal#(V) -> c_34(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)) -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 12:S:isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P)) ,isQid#(activate(I)) ,activate#(I) ,activate#(P)) -->_4 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 -->_1 U71#(tt(),P) -> c_10(U72#(isPal(activate(P))),isPal#(activate(P)),activate#(P)):4 13:S:isPal#(V) -> c_36(U81#(isNePal(activate(V))),isNePal#(activate(V)),activate#(V)) -->_2 isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P)) ,isQid#(activate(I)) ,activate#(I) ,activate#(P)):12 -->_2 isNePal#(V) -> c_34(U61#(isQid(activate(V))),isQid#(activate(V)),activate#(V)):11 -->_3 activate#(n____(X1,X2)) -> c_19(__#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):5 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)),activate#(V2)) U41#(tt(),V2) -> c_5(isNeList#(activate(V2)),activate#(V2)) U51#(tt(),V2) -> c_7(isList#(activate(V2)),activate#(V2)) U71#(tt(),P) -> c_10(isPal#(activate(P)),activate#(P)) activate#(n____(X1,X2)) -> c_19(activate#(X1),activate#(X2)) isList#(V) -> c_28(isNeList#(activate(V)),activate#(V)) isNeList#(V) -> c_31(activate#(V)) isNePal#(V) -> c_34(activate#(V)) isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P)),activate#(I),activate#(P)) isPal#(V) -> c_36(isNePal#(activate(V)),activate#(V)) * Step 6: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: U21#(tt(),V2) -> c_2(isList#(activate(V2)),activate#(V2)) U41#(tt(),V2) -> c_5(isNeList#(activate(V2)),activate#(V2)) U51#(tt(),V2) -> c_7(isList#(activate(V2)),activate#(V2)) U71#(tt(),P) -> c_10(isPal#(activate(P)),activate#(P)) activate#(n____(X1,X2)) -> c_19(activate#(X1),activate#(X2)) isList#(V) -> c_28(isNeList#(activate(V)),activate#(V)) isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(V) -> c_31(activate#(V)) isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNePal#(V) -> c_34(activate#(V)) isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P)),activate#(I),activate#(P)) isPal#(V) -> c_36(isNePal#(activate(V)),activate#(V)) - 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() __(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)) -> __(activate(X1),activate(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,n____(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,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/2 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/2,c_8/0,c_9/0,c_10/2,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/0 ,c_19/2,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/4,c_30/0,c_31/1,c_32/4,c_33/4 ,c_34/1,c_35/3,c_36/2,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/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() __(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)) -> __(activate(X1),activate(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)),activate#(V2)) U41#(tt(),V2) -> c_5(isNeList#(activate(V2)),activate#(V2)) U51#(tt(),V2) -> c_7(isList#(activate(V2)),activate#(V2)) U71#(tt(),P) -> c_10(isPal#(activate(P)),activate#(P)) activate#(n____(X1,X2)) -> c_19(activate#(X1),activate#(X2)) isList#(V) -> c_28(isNeList#(activate(V)),activate#(V)) isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(V) -> c_31(activate#(V)) isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNePal#(V) -> c_34(activate#(V)) isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P)),activate#(I),activate#(P)) isPal#(V) -> c_36(isNePal#(activate(V)),activate#(V)) * Step 7: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: U21#(tt(),V2) -> c_2(isList#(activate(V2)),activate#(V2)) U41#(tt(),V2) -> c_5(isNeList#(activate(V2)),activate#(V2)) U51#(tt(),V2) -> c_7(isList#(activate(V2)),activate#(V2)) U71#(tt(),P) -> c_10(isPal#(activate(P)),activate#(P)) activate#(n____(X1,X2)) -> c_19(activate#(X1),activate#(X2)) isList#(V) -> c_28(isNeList#(activate(V)),activate#(V)) isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(V) -> c_31(activate#(V)) isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNePal#(V) -> c_34(activate#(V)) isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P)),activate#(I),activate#(P)) isPal#(V) -> c_36(isNePal#(activate(V)),activate#(V)) - 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() __(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)) -> __(activate(X1),activate(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/2 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/2,c_8/0,c_9/0,c_10/2,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/0 ,c_19/2,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/4,c_30/0,c_31/1,c_32/4,c_33/4 ,c_34/1,c_35/3,c_36/2,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/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: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component U21#(tt(),V2) -> c_2(isList#(activate(V2)),activate#(V2)) U41#(tt(),V2) -> c_5(isNeList#(activate(V2)),activate#(V2)) U51#(tt(),V2) -> c_7(isList#(activate(V2)),activate#(V2)) U71#(tt(),P) -> c_10(isPal#(activate(P)),activate#(P)) isList#(V) -> c_28(isNeList#(activate(V)),activate#(V)) isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P)),activate#(I),activate#(P)) isPal#(V) -> c_36(isNePal#(activate(V)),activate#(V)) and a lower component activate#(n____(X1,X2)) -> c_19(activate#(X1),activate#(X2)) isNeList#(V) -> c_31(activate#(V)) isNePal#(V) -> c_34(activate#(V)) Further, following extension rules are added to the lower component. U21#(tt(),V2) -> activate#(V2) U21#(tt(),V2) -> isList#(activate(V2)) U41#(tt(),V2) -> activate#(V2) U41#(tt(),V2) -> isNeList#(activate(V2)) U51#(tt(),V2) -> activate#(V2) U51#(tt(),V2) -> isList#(activate(V2)) U71#(tt(),P) -> activate#(P) U71#(tt(),P) -> isPal#(activate(P)) isList#(V) -> activate#(V) isList#(V) -> isNeList#(activate(V)) isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2)) isList#(n____(V1,V2)) -> activate#(V1) isList#(n____(V1,V2)) -> activate#(V2) isList#(n____(V1,V2)) -> isList#(activate(V1)) isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2)) isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2)) isNeList#(n____(V1,V2)) -> activate#(V1) isNeList#(n____(V1,V2)) -> activate#(V2) isNeList#(n____(V1,V2)) -> isList#(activate(V1)) isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) isNePal#(n____(I,n____(P,I))) -> U71#(isQid(activate(I)),activate(P)) isNePal#(n____(I,n____(P,I))) -> activate#(I) isNePal#(n____(I,n____(P,I))) -> activate#(P) isPal#(V) -> activate#(V) isPal#(V) -> isNePal#(activate(V)) ** Step 7.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: U21#(tt(),V2) -> c_2(isList#(activate(V2)),activate#(V2)) U41#(tt(),V2) -> c_5(isNeList#(activate(V2)),activate#(V2)) U51#(tt(),V2) -> c_7(isList#(activate(V2)),activate#(V2)) U71#(tt(),P) -> c_10(isPal#(activate(P)),activate#(P)) isList#(V) -> c_28(isNeList#(activate(V)),activate#(V)) isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P)),activate#(I),activate#(P)) isPal#(V) -> c_36(isNePal#(activate(V)),activate#(V)) - 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() __(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)) -> __(activate(X1),activate(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/2 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/2,c_8/0,c_9/0,c_10/2,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/0 ,c_19/2,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/4,c_30/0,c_31/1,c_32/4,c_33/4 ,c_34/1,c_35/3,c_36/2,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/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(isList#(activate(V2)),activate#(V2)) -->_1 isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):6 -->_1 isList#(V) -> c_28(isNeList#(activate(V)),activate#(V)):5 2:S:U41#(tt(),V2) -> c_5(isNeList#(activate(V2)),activate#(V2)) -->_1 isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)):8 -->_1 isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 3:S:U51#(tt(),V2) -> c_7(isList#(activate(V2)),activate#(V2)) -->_1 isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):6 -->_1 isList#(V) -> c_28(isNeList#(activate(V)),activate#(V)):5 4:S:U71#(tt(),P) -> c_10(isPal#(activate(P)),activate#(P)) -->_1 isPal#(V) -> c_36(isNePal#(activate(V)),activate#(V)):10 5:S:isList#(V) -> c_28(isNeList#(activate(V)),activate#(V)) -->_1 isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)):8 -->_1 isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 6:S:isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):6 -->_2 isList#(V) -> c_28(isNeList#(activate(V)),activate#(V)):5 -->_1 U21#(tt(),V2) -> c_2(isList#(activate(V2)),activate#(V2)):1 7:S:isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):6 -->_2 isList#(V) -> c_28(isNeList#(activate(V)),activate#(V)):5 -->_1 U41#(tt(),V2) -> c_5(isNeList#(activate(V2)),activate#(V2)):2 8:S:isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)) ,isNeList#(activate(V1)) ,activate#(V1) ,activate#(V2)):8 -->_2 isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)) ,isList#(activate(V1)) ,activate#(V1) ,activate#(V2)):7 -->_1 U51#(tt(),V2) -> c_7(isList#(activate(V2)),activate#(V2)):3 9:S:isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P)),activate#(I),activate#(P)) -->_1 U71#(tt(),P) -> c_10(isPal#(activate(P)),activate#(P)):4 10:S:isPal#(V) -> c_36(isNePal#(activate(V)),activate#(V)) -->_1 isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P)) ,activate#(I) ,activate#(P)):9 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))) U71#(tt(),P) -> c_10(isPal#(activate(P))) isList#(V) -> c_28(isNeList#(activate(V))) isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P))) isPal#(V) -> c_36(isNePal#(activate(V))) ** Step 7.a:2: 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))) U71#(tt(),P) -> c_10(isPal#(activate(P))) isList#(V) -> c_28(isNeList#(activate(V))) isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P))) isPal#(V) -> c_36(isNePal#(activate(V))) - 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() __(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)) -> __(activate(X1),activate(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/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/0 ,c_19/2,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/2,c_30/0,c_31/1,c_32/2,c_33/2 ,c_34/1,c_35/1,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/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 any 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_10) = {1}, uargs(c_28) = {1}, uargs(c_29) = {1,2}, uargs(c_32) = {1,2}, uargs(c_33) = {1,2}, uargs(c_35) = {1}, uargs(c_36) = {1} Following symbols are considered usable: {__,a,activate,e,i,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] x2 + [3] p(U22) = [4] p(U31) = [2] x1 + [3] p(U41) = [1] x2 + [0] p(U42) = [1] x1 + [1] p(U51) = [4] x2 + [4] p(U52) = [0] p(U61) = [1] x1 + [0] p(U71) = [1] x1 + [1] p(U72) = [1] p(U81) = [4] x1 + [4] p(__) = [1] x1 + [1] x2 + [4] p(a) = [6] p(activate) = [1] x1 + [0] p(e) = [2] p(i) = [4] p(isList) = [7] p(isNeList) = [2] p(isNePal) = [1] p(isPal) = [1] x1 + [0] p(isQid) = [6] p(n____) = [1] x1 + [1] x2 + [4] p(n__a) = [6] p(n__e) = [2] p(n__i) = [4] p(n__nil) = [1] p(n__o) = [0] p(n__u) = [0] p(nil) = [1] p(o) = [0] p(tt) = [0] p(u) = [0] p(U11#) = [0] p(U21#) = [0] p(U22#) = [1] x1 + [1] p(U31#) = [0] p(U41#) = [0] p(U42#) = [0] p(U51#) = [0] p(U52#) = [2] x1 + [0] p(U61#) = [2] x1 + [0] p(U71#) = [1] x2 + [0] p(U72#) = [2] p(U81#) = [4] x1 + [0] p(__#) = [1] x1 + [1] x2 + [0] p(a#) = [1] p(activate#) = [1] x1 + [1] p(e#) = [0] p(i#) = [1] p(isList#) = [0] p(isNeList#) = [0] p(isNePal#) = [1] x1 + [0] p(isPal#) = [1] x1 + [0] p(isQid#) = [1] x1 + [0] p(nil#) = [1] p(o#) = [1] p(u#) = [0] p(c_1) = [0] p(c_2) = [2] x1 + [0] p(c_3) = [0] p(c_4) = [4] p(c_5) = [4] x1 + [0] p(c_6) = [2] p(c_7) = [2] x1 + [0] p(c_8) = [0] p(c_9) = [1] p(c_10) = [1] x1 + [0] p(c_11) = [0] p(c_12) = [1] p(c_13) = [1] p(c_14) = [1] p(c_15) = [1] x2 + [1] p(c_16) = [4] p(c_17) = [1] p(c_18) = [4] p(c_19) = [1] x2 + [1] p(c_20) = [0] p(c_21) = [1] x1 + [1] p(c_22) = [1] x1 + [0] p(c_23) = [4] p(c_24) = [1] x1 + [1] p(c_25) = [1] x1 + [1] p(c_26) = [0] p(c_27) = [1] p(c_28) = [2] x1 + [0] p(c_29) = [2] x1 + [1] x2 + [0] p(c_30) = [1] p(c_31) = [1] p(c_32) = [4] x1 + [1] x2 + [0] p(c_33) = [4] x1 + [4] x2 + [0] p(c_34) = [0] p(c_35) = [1] x1 + [7] p(c_36) = [1] x1 + [0] p(c_37) = [1] p(c_38) = [1] p(c_39) = [2] p(c_40) = [4] p(c_41) = [0] p(c_42) = [0] p(c_43) = [4] p(c_44) = [2] p(c_45) = [2] Following rules are strictly oriented: isNePal#(n____(I,n____(P,I))) = [2] I + [1] P + [8] > [1] P + [7] = c_35(U71#(isQid(activate(I)),activate(P))) Following rules are (at-least) weakly oriented: U21#(tt(),V2) = [0] >= [0] = c_2(isList#(activate(V2))) U41#(tt(),V2) = [0] >= [0] = c_5(isNeList#(activate(V2))) U51#(tt(),V2) = [0] >= [0] = c_7(isList#(activate(V2))) U71#(tt(),P) = [1] P + [0] >= [1] P + [0] = c_10(isPal#(activate(P))) isList#(V) = [0] >= [0] = c_28(isNeList#(activate(V))) isList#(n____(V1,V2)) = [0] >= [0] = c_29(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) = [0] >= [0] = c_32(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) = [0] >= [0] = c_33(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) isPal#(V) = [1] V + [0] >= [1] V + [0] = c_36(isNePal#(activate(V))) __(X,nil()) = [1] X + [5] >= [1] X + [0] = X __(X1,X2) = [1] X1 + [1] X2 + [4] >= [1] X1 + [1] X2 + [4] = n____(X1,X2) __(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [8] >= [1] X + [1] Y + [1] Z + [8] = __(X,__(Y,Z)) __(nil(),X) = [1] X + [5] >= [1] X + [0] = X a() = [6] >= [6] = n__a() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n____(X1,X2)) = [1] X1 + [1] X2 + [4] >= [1] X1 + [1] X2 + [4] = __(activate(X1),activate(X2)) activate(n__a()) = [6] >= [6] = a() activate(n__e()) = [2] >= [2] = e() activate(n__i()) = [4] >= [4] = i() activate(n__nil()) = [1] >= [1] = nil() activate(n__o()) = [0] >= [0] = o() activate(n__u()) = [0] >= [0] = u() e() = [2] >= [2] = n__e() i() = [4] >= [4] = n__i() nil() = [1] >= [1] = n__nil() o() = [0] >= [0] = n__o() u() = [0] >= [0] = n__u() ** Step 7.a:3: 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))) U71#(tt(),P) -> c_10(isPal#(activate(P))) isList#(V) -> c_28(isNeList#(activate(V))) isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) isPal#(V) -> c_36(isNePal#(activate(V))) - Weak DPs: isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P))) - 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() __(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)) -> __(activate(X1),activate(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/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/0 ,c_19/2,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/2,c_30/0,c_31/1,c_32/2,c_33/2 ,c_34/1,c_35/1,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/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 any 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_10) = {1}, uargs(c_28) = {1}, uargs(c_29) = {1,2}, uargs(c_32) = {1,2}, uargs(c_33) = {1,2}, uargs(c_35) = {1}, uargs(c_36) = {1} 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) = [2] p(U21) = [3] p(U22) = [2] p(U31) = [0] p(U41) = [2] x2 + [4] p(U42) = [2] x1 + [0] p(U51) = [5] x1 + [3] p(U52) = [2] x1 + [5] p(U61) = [0] p(U71) = [1] x2 + [0] p(U72) = [1] x1 + [1] p(U81) = [1] x1 + [0] p(__) = [1] x1 + [1] x2 + [2] p(a) = [1] p(activate) = [1] x1 + [0] p(e) = [1] p(i) = [1] p(isList) = [4] p(isNeList) = [2] x1 + [0] p(isNePal) = [1] x1 + [1] p(isPal) = [1] x1 + [0] p(isQid) = [2] p(n____) = [1] x1 + [1] x2 + [2] p(n__a) = [1] p(n__e) = [1] p(n__i) = [1] p(n__nil) = [0] p(n__o) = [0] p(n__u) = [0] p(nil) = [0] p(o) = [0] p(tt) = [1] p(u) = [0] p(U11#) = [4] p(U21#) = [4] x2 + [4] p(U22#) = [1] x1 + [1] p(U31#) = [1] x1 + [1] p(U41#) = [2] x1 + [4] x2 + [0] p(U42#) = [0] p(U51#) = [4] x2 + [4] p(U52#) = [0] p(U61#) = [4] p(U71#) = [0] p(U72#) = [1] p(U81#) = [1] x1 + [2] p(__#) = [1] x1 + [0] p(a#) = [1] p(activate#) = [4] x1 + [1] p(e#) = [2] p(i#) = [2] p(isList#) = [4] x1 + [0] p(isNeList#) = [4] x1 + [0] p(isNePal#) = [0] p(isPal#) = [0] p(isQid#) = [0] p(nil#) = [0] p(o#) = [0] p(u#) = [0] p(c_1) = [2] p(c_2) = [1] x1 + [0] p(c_3) = [0] p(c_4) = [1] p(c_5) = [1] x1 + [2] p(c_6) = [0] p(c_7) = [1] x1 + [4] p(c_8) = [0] p(c_9) = [2] p(c_10) = [1] x1 + [0] p(c_11) = [2] p(c_12) = [2] p(c_13) = [1] p(c_14) = [1] p(c_15) = [2] x1 + [1] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [1] p(c_20) = [1] x1 + [1] p(c_21) = [2] p(c_22) = [2] x1 + [1] p(c_23) = [1] x1 + [1] p(c_24) = [1] x1 + [1] p(c_25) = [1] x1 + [0] p(c_26) = [0] p(c_27) = [1] p(c_28) = [1] x1 + [0] p(c_29) = [1] x1 + [1] x2 + [4] p(c_30) = [1] p(c_31) = [2] x1 + [4] p(c_32) = [1] x1 + [1] x2 + [0] p(c_33) = [1] x1 + [1] x2 + [0] p(c_34) = [1] x1 + [0] p(c_35) = [2] x1 + [0] p(c_36) = [4] x1 + [0] p(c_37) = [1] p(c_38) = [0] p(c_39) = [0] p(c_40) = [4] p(c_41) = [0] p(c_42) = [2] p(c_43) = [1] p(c_44) = [4] p(c_45) = [1] Following rules are strictly oriented: U21#(tt(),V2) = [4] V2 + [4] > [4] V2 + [0] = c_2(isList#(activate(V2))) isNeList#(n____(V1,V2)) = [4] V1 + [4] V2 + [8] > [4] V1 + [4] V2 + [4] = c_33(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) Following rules are (at-least) weakly oriented: U41#(tt(),V2) = [4] V2 + [2] >= [4] V2 + [2] = c_5(isNeList#(activate(V2))) U51#(tt(),V2) = [4] V2 + [4] >= [4] V2 + [4] = c_7(isList#(activate(V2))) U71#(tt(),P) = [0] >= [0] = c_10(isPal#(activate(P))) isList#(V) = [4] V + [0] >= [4] V + [0] = c_28(isNeList#(activate(V))) isList#(n____(V1,V2)) = [4] V1 + [4] V2 + [8] >= [4] V1 + [4] V2 + [8] = c_29(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) = [4] V1 + [4] V2 + [8] >= [4] V1 + [4] V2 + [8] = c_32(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNePal#(n____(I,n____(P,I))) = [0] >= [0] = c_35(U71#(isQid(activate(I)),activate(P))) isPal#(V) = [0] >= [0] = c_36(isNePal#(activate(V))) U11(tt()) = [2] >= [1] = tt() U21(tt(),V2) = [3] >= [2] = U22(isList(activate(V2))) U22(tt()) = [2] >= [1] = tt() __(X,nil()) = [1] X + [2] >= [1] X + [0] = X __(X1,X2) = [1] X1 + [1] X2 + [2] >= [1] X1 + [1] X2 + [2] = n____(X1,X2) __(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [4] >= [1] X + [1] Y + [1] Z + [4] = __(X,__(Y,Z)) __(nil(),X) = [1] X + [2] >= [1] X + [0] = X a() = [1] >= [1] = n__a() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n____(X1,X2)) = [1] X1 + [1] X2 + [2] >= [1] X1 + [1] X2 + [2] = __(activate(X1),activate(X2)) activate(n__a()) = [1] >= [1] = a() activate(n__e()) = [1] >= [1] = e() activate(n__i()) = [1] >= [1] = i() activate(n__nil()) = [0] >= [0] = nil() activate(n__o()) = [0] >= [0] = o() activate(n__u()) = [0] >= [0] = u() e() = [1] >= [1] = n__e() i() = [1] >= [1] = n__i() isList(V) = [4] >= [2] = U11(isNeList(activate(V))) isList(n____(V1,V2)) = [4] >= [3] = U21(isList(activate(V1)),activate(V2)) isList(n__nil()) = [4] >= [1] = tt() nil() = [0] >= [0] = n__nil() o() = [0] >= [0] = n__o() u() = [0] >= [0] = n__u() ** Step 7.a:4: 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))) U71#(tt(),P) -> c_10(isPal#(activate(P))) isList#(V) -> c_28(isNeList#(activate(V))) isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isPal#(V) -> c_36(isNePal#(activate(V))) - Weak DPs: U21#(tt(),V2) -> c_2(isList#(activate(V2))) isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P))) - 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() __(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)) -> __(activate(X1),activate(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/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/0 ,c_19/2,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/2,c_30/0,c_31/1,c_32/2,c_33/2 ,c_34/1,c_35/1,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/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 any 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_10) = {1}, uargs(c_28) = {1}, uargs(c_29) = {1,2}, uargs(c_32) = {1,2}, uargs(c_33) = {1,2}, uargs(c_35) = {1}, uargs(c_36) = {1} Following symbols are considered usable: {__,a,activate,e,i,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) = [2] p(U22) = [1] x1 + [4] p(U31) = [4] p(U41) = [2] x1 + [1] x2 + [6] p(U42) = [0] p(U51) = [0] p(U52) = [0] p(U61) = [1] p(U71) = [0] p(U72) = [0] p(U81) = [0] p(__) = [1] x1 + [1] x2 + [2] p(a) = [0] p(activate) = [1] x1 + [0] p(e) = [0] p(i) = [3] p(isList) = [4] p(isNeList) = [0] p(isNePal) = [1] x1 + [2] p(isPal) = [4] x1 + [0] p(isQid) = [4] x1 + [0] p(n____) = [1] x1 + [1] x2 + [2] p(n__a) = [0] p(n__e) = [0] p(n__i) = [3] 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#) = [1] x1 + [2] p(U21#) = [0] p(U22#) = [1] x1 + [0] p(U31#) = [1] x1 + [4] p(U41#) = [0] p(U42#) = [4] x1 + [0] p(U51#) = [0] p(U52#) = [1] x1 + [4] p(U61#) = [1] x1 + [4] p(U71#) = [1] x2 + [3] p(U72#) = [0] p(U81#) = [0] p(__#) = [2] x1 + [2] x2 + [0] p(a#) = [4] p(activate#) = [1] p(e#) = [4] p(i#) = [0] p(isList#) = [0] p(isNeList#) = [0] p(isNePal#) = [1] x1 + [2] p(isPal#) = [1] x1 + [2] p(isQid#) = [1] p(nil#) = [4] p(o#) = [4] p(u#) = [0] p(c_1) = [1] p(c_2) = [2] x1 + [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [2] x1 + [0] p(c_8) = [0] p(c_9) = [1] p(c_10) = [1] x1 + [0] p(c_11) = [1] p(c_12) = [4] p(c_13) = [0] p(c_14) = [0] p(c_15) = [1] x2 + [1] p(c_16) = [1] p(c_17) = [4] p(c_18) = [1] p(c_19) = [1] x1 + [0] p(c_20) = [2] x1 + [2] p(c_21) = [0] p(c_22) = [2] p(c_23) = [2] x1 + [1] p(c_24) = [1] x1 + [1] p(c_25) = [1] x1 + [1] p(c_26) = [0] p(c_27) = [1] p(c_28) = [1] x1 + [0] p(c_29) = [4] x1 + [1] x2 + [0] p(c_30) = [4] p(c_31) = [0] p(c_32) = [2] x1 + [4] x2 + [0] p(c_33) = [4] x1 + [4] x2 + [0] p(c_34) = [1] p(c_35) = [1] x1 + [3] p(c_36) = [1] x1 + [0] p(c_37) = [0] p(c_38) = [1] p(c_39) = [1] p(c_40) = [2] p(c_41) = [4] p(c_42) = [2] p(c_43) = [1] p(c_44) = [4] p(c_45) = [4] Following rules are strictly oriented: U71#(tt(),P) = [1] P + [3] > [1] P + [2] = c_10(isPal#(activate(P))) Following rules are (at-least) weakly oriented: U21#(tt(),V2) = [0] >= [0] = c_2(isList#(activate(V2))) U41#(tt(),V2) = [0] >= [0] = c_5(isNeList#(activate(V2))) U51#(tt(),V2) = [0] >= [0] = c_7(isList#(activate(V2))) isList#(V) = [0] >= [0] = c_28(isNeList#(activate(V))) isList#(n____(V1,V2)) = [0] >= [0] = c_29(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) = [0] >= [0] = c_32(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) = [0] >= [0] = c_33(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) isNePal#(n____(I,n____(P,I))) = [2] I + [1] P + [6] >= [1] P + [6] = c_35(U71#(isQid(activate(I)),activate(P))) isPal#(V) = [1] V + [2] >= [1] V + [2] = c_36(isNePal#(activate(V))) __(X,nil()) = [1] X + [2] >= [1] X + [0] = X __(X1,X2) = [1] X1 + [1] X2 + [2] >= [1] X1 + [1] X2 + [2] = n____(X1,X2) __(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [4] >= [1] X + [1] Y + [1] Z + [4] = __(X,__(Y,Z)) __(nil(),X) = [1] X + [2] >= [1] X + [0] = X a() = [0] >= [0] = n__a() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n____(X1,X2)) = [1] X1 + [1] X2 + [2] >= [1] X1 + [1] X2 + [2] = __(activate(X1),activate(X2)) activate(n__a()) = [0] >= [0] = a() activate(n__e()) = [0] >= [0] = e() activate(n__i()) = [3] >= [3] = 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() = [3] >= [3] = n__i() nil() = [0] >= [0] = n__nil() o() = [0] >= [0] = n__o() u() = [0] >= [0] = n__u() ** Step 7.a:5: 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_28(isNeList#(activate(V))) isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isPal#(V) -> c_36(isNePal#(activate(V))) - Weak DPs: U21#(tt(),V2) -> c_2(isList#(activate(V2))) U71#(tt(),P) -> c_10(isPal#(activate(P))) isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P))) - 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() __(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)) -> __(activate(X1),activate(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/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/0 ,c_19/2,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/2,c_30/0,c_31/1,c_32/2,c_33/2 ,c_34/1,c_35/1,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/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 any 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_10) = {1}, uargs(c_28) = {1}, uargs(c_29) = {1,2}, uargs(c_32) = {1,2}, uargs(c_33) = {1,2}, uargs(c_35) = {1}, uargs(c_36) = {1} Following symbols are considered usable: {__,a,activate,e,i,isQid,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 + [4] p(U21) = [4] x1 + [4] x2 + [2] p(U22) = [3] x1 + [3] p(U31) = [7] p(U41) = [3] x1 + [5] p(U42) = [3] p(U51) = [5] x1 + [4] x2 + [4] p(U52) = [1] x1 + [4] p(U61) = [0] p(U71) = [1] x1 + [1] x2 + [2] p(U72) = [1] x1 + [4] p(U81) = [1] p(__) = [1] x1 + [1] x2 + [1] p(a) = [0] p(activate) = [1] x1 + [0] p(e) = [0] p(i) = [0] p(isList) = [0] p(isNeList) = [3] x1 + [0] p(isNePal) = [1] x1 + [0] p(isPal) = [1] x1 + [2] p(isQid) = [2] x1 + [2] 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) = [0] p(nil) = [0] p(o) = [0] p(tt) = [2] p(u) = [0] p(U11#) = [1] x1 + [1] p(U21#) = [0] p(U22#) = [0] p(U31#) = [0] p(U41#) = [0] p(U42#) = [1] x1 + [1] p(U51#) = [0] p(U52#) = [0] p(U61#) = [2] x1 + [1] p(U71#) = [6] x1 + [6] x2 + [2] p(U72#) = [1] x1 + [0] p(U81#) = [4] x1 + [1] p(__#) = [1] p(a#) = [2] p(activate#) = [2] p(e#) = [1] p(i#) = [1] p(isList#) = [0] p(isNeList#) = [0] p(isNePal#) = [6] x1 + [2] p(isPal#) = [6] x1 + [4] p(isQid#) = [1] p(nil#) = [1] p(o#) = [0] p(u#) = [0] p(c_1) = [2] p(c_2) = [1] x1 + [0] p(c_3) = [4] p(c_4) = [1] p(c_5) = [2] x1 + [0] p(c_6) = [0] p(c_7) = [4] x1 + [0] p(c_8) = [1] p(c_9) = [0] p(c_10) = [1] x1 + [5] p(c_11) = [0] p(c_12) = [1] p(c_13) = [0] p(c_14) = [0] p(c_15) = [1] x1 + [0] p(c_16) = [1] p(c_17) = [2] p(c_18) = [2] p(c_19) = [1] x2 + [0] p(c_20) = [1] x1 + [4] p(c_21) = [1] x1 + [0] p(c_22) = [4] p(c_23) = [1] x1 + [1] p(c_24) = [1] p(c_25) = [1] x1 + [1] p(c_26) = [2] p(c_27) = [2] p(c_28) = [4] x1 + [0] p(c_29) = [1] x1 + [1] x2 + [0] p(c_30) = [0] p(c_31) = [2] p(c_32) = [2] x1 + [1] x2 + [0] p(c_33) = [1] x1 + [1] x2 + [0] p(c_34) = [1] p(c_35) = [1] x1 + [0] p(c_36) = [1] x1 + [0] p(c_37) = [4] p(c_38) = [1] p(c_39) = [1] p(c_40) = [1] p(c_41) = [2] p(c_42) = [4] p(c_43) = [1] p(c_44) = [1] p(c_45) = [1] Following rules are strictly oriented: isPal#(V) = [6] V + [4] > [6] V + [2] = c_36(isNePal#(activate(V))) Following rules are (at-least) weakly oriented: U21#(tt(),V2) = [0] >= [0] = c_2(isList#(activate(V2))) U41#(tt(),V2) = [0] >= [0] = c_5(isNeList#(activate(V2))) U51#(tt(),V2) = [0] >= [0] = c_7(isList#(activate(V2))) U71#(tt(),P) = [6] P + [14] >= [6] P + [9] = c_10(isPal#(activate(P))) isList#(V) = [0] >= [0] = c_28(isNeList#(activate(V))) isList#(n____(V1,V2)) = [0] >= [0] = c_29(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) = [0] >= [0] = c_32(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) = [0] >= [0] = c_33(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) isNePal#(n____(I,n____(P,I))) = [12] I + [6] P + [14] >= [12] I + [6] P + [14] = c_35(U71#(isQid(activate(I)),activate(P))) __(X,nil()) = [1] X + [1] >= [1] X + [0] = X __(X1,X2) = [1] X1 + [1] X2 + [1] >= [1] X1 + [1] X2 + [1] = n____(X1,X2) __(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [2] >= [1] X + [1] Y + [1] Z + [2] = __(X,__(Y,Z)) __(nil(),X) = [1] X + [1] >= [1] X + [0] = X 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] = __(activate(X1),activate(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()) = [0] >= [0] = u() e() = [0] >= [0] = n__e() i() = [0] >= [0] = n__i() isQid(n__a()) = [2] >= [2] = tt() isQid(n__e()) = [2] >= [2] = tt() isQid(n__i()) = [2] >= [2] = tt() isQid(n__o()) = [2] >= [2] = tt() isQid(n__u()) = [2] >= [2] = tt() nil() = [0] >= [0] = n__nil() o() = [0] >= [0] = n__o() u() = [0] >= [0] = n__u() ** Step 7.a:6: 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_28(isNeList#(activate(V))) isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) - Weak DPs: U21#(tt(),V2) -> c_2(isList#(activate(V2))) U71#(tt(),P) -> c_10(isPal#(activate(P))) isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P))) isPal#(V) -> c_36(isNePal#(activate(V))) - 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() __(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)) -> __(activate(X1),activate(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/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/0 ,c_19/2,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/2,c_30/0,c_31/1,c_32/2,c_33/2 ,c_34/1,c_35/1,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/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 any 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_10) = {1}, uargs(c_28) = {1}, uargs(c_29) = {1,2}, uargs(c_32) = {1,2}, uargs(c_33) = {1,2}, uargs(c_35) = {1}, uargs(c_36) = {1} Following symbols are considered usable: {__,a,activate,e,i,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 + [1] p(U21) = [4] x2 + [4] p(U22) = [4] x1 + [0] p(U31) = [2] x1 + [1] p(U41) = [2] x1 + [4] p(U42) = [4] x1 + [6] p(U51) = [1] x2 + [2] p(U52) = [2] x1 + [0] p(U61) = [0] p(U71) = [2] x1 + [1] p(U72) = [0] p(U81) = [4] p(__) = [1] x1 + [1] x2 + [4] p(a) = [0] p(activate) = [1] x1 + [0] p(e) = [0] p(i) = [4] p(isList) = [1] p(isNeList) = [0] p(isNePal) = [0] p(isPal) = [1] x1 + [4] p(isQid) = [7] p(n____) = [1] x1 + [1] x2 + [4] p(n__a) = [0] p(n__e) = [0] p(n__i) = [4] p(n__nil) = [1] p(n__o) = [0] p(n__u) = [0] p(nil) = [1] p(o) = [0] p(tt) = [0] p(u) = [0] p(U11#) = [1] p(U21#) = [2] x2 + [2] p(U22#) = [2] p(U31#) = [1] x1 + [4] p(U41#) = [2] x2 + [0] p(U42#) = [1] p(U51#) = [2] x2 + [0] p(U52#) = [0] p(U61#) = [1] x1 + [0] p(U71#) = [0] p(U72#) = [0] p(U81#) = [1] p(__#) = [1] x2 + [1] p(a#) = [2] p(activate#) = [2] p(e#) = [0] p(i#) = [1] p(isList#) = [2] x1 + [0] p(isNeList#) = [2] x1 + [0] p(isNePal#) = [0] p(isPal#) = [0] p(isQid#) = [4] x1 + [1] p(nil#) = [0] p(o#) = [1] p(u#) = [1] p(c_1) = [0] p(c_2) = [1] x1 + [1] 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) = [0] p(c_9) = [0] p(c_10) = [1] x1 + [0] p(c_11) = [0] p(c_12) = [2] p(c_13) = [1] p(c_14) = [1] p(c_15) = [1] x1 + [1] x2 + [0] p(c_16) = [2] p(c_17) = [2] p(c_18) = [1] p(c_19) = [2] p(c_20) = [2] p(c_21) = [0] p(c_22) = [0] p(c_23) = [1] p(c_24) = [1] p(c_25) = [2] p(c_26) = [1] p(c_27) = [1] p(c_28) = [1] x1 + [0] p(c_29) = [1] x1 + [1] x2 + [3] p(c_30) = [0] p(c_31) = [2] x1 + [0] p(c_32) = [1] x1 + [1] x2 + [7] p(c_33) = [1] x1 + [1] x2 + [5] p(c_34) = [0] p(c_35) = [4] x1 + [0] p(c_36) = [1] x1 + [0] p(c_37) = [2] p(c_38) = [4] p(c_39) = [1] p(c_40) = [0] p(c_41) = [0] p(c_42) = [0] p(c_43) = [2] p(c_44) = [0] p(c_45) = [0] Following rules are strictly oriented: isList#(n____(V1,V2)) = [2] V1 + [2] V2 + [8] > [2] V1 + [2] V2 + [5] = c_29(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) = [2] V1 + [2] V2 + [8] > [2] V1 + [2] V2 + [7] = c_32(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) Following rules are (at-least) weakly oriented: U21#(tt(),V2) = [2] V2 + [2] >= [2] V2 + [1] = c_2(isList#(activate(V2))) U41#(tt(),V2) = [2] V2 + [0] >= [2] V2 + [0] = c_5(isNeList#(activate(V2))) U51#(tt(),V2) = [2] V2 + [0] >= [2] V2 + [0] = c_7(isList#(activate(V2))) U71#(tt(),P) = [0] >= [0] = c_10(isPal#(activate(P))) isList#(V) = [2] V + [0] >= [2] V + [0] = c_28(isNeList#(activate(V))) isNeList#(n____(V1,V2)) = [2] V1 + [2] V2 + [8] >= [2] V1 + [2] V2 + [5] = c_33(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) isNePal#(n____(I,n____(P,I))) = [0] >= [0] = c_35(U71#(isQid(activate(I)),activate(P))) isPal#(V) = [0] >= [0] = c_36(isNePal#(activate(V))) __(X,nil()) = [1] X + [5] >= [1] X + [0] = X __(X1,X2) = [1] X1 + [1] X2 + [4] >= [1] X1 + [1] X2 + [4] = n____(X1,X2) __(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [8] >= [1] X + [1] Y + [1] Z + [8] = __(X,__(Y,Z)) __(nil(),X) = [1] X + [5] >= [1] X + [0] = X a() = [0] >= [0] = n__a() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n____(X1,X2)) = [1] X1 + [1] X2 + [4] >= [1] X1 + [1] X2 + [4] = __(activate(X1),activate(X2)) activate(n__a()) = [0] >= [0] = a() activate(n__e()) = [0] >= [0] = e() activate(n__i()) = [4] >= [4] = i() activate(n__nil()) = [1] >= [1] = nil() activate(n__o()) = [0] >= [0] = o() activate(n__u()) = [0] >= [0] = u() e() = [0] >= [0] = n__e() i() = [4] >= [4] = n__i() nil() = [1] >= [1] = n__nil() o() = [0] >= [0] = n__o() u() = [0] >= [0] = n__u() ** Step 7.a:7: 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_28(isNeList#(activate(V))) - Weak DPs: U21#(tt(),V2) -> c_2(isList#(activate(V2))) U71#(tt(),P) -> c_10(isPal#(activate(P))) isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P))) isPal#(V) -> c_36(isNePal#(activate(V))) - 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() __(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)) -> __(activate(X1),activate(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/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/0 ,c_19/2,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/2,c_30/0,c_31/1,c_32/2,c_33/2 ,c_34/1,c_35/1,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/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 any 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_10) = {1}, uargs(c_28) = {1}, uargs(c_29) = {1,2}, uargs(c_32) = {1,2}, uargs(c_33) = {1,2}, uargs(c_35) = {1}, uargs(c_36) = {1} Following symbols are considered usable: {__,a,activate,e,i,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] p(U21) = [3] x2 + [0] p(U22) = [7] p(U31) = [1] x1 + [5] p(U41) = [4] x1 + [2] x2 + [5] p(U42) = [6] p(U51) = [1] x1 + [5] x2 + [6] p(U52) = [4] p(U61) = [4] p(U71) = [2] p(U72) = [2] x1 + [1] p(U81) = [0] p(__) = [1] x1 + [1] x2 + [2] p(a) = [0] p(activate) = [1] x1 + [0] p(e) = [0] p(i) = [0] p(isList) = [0] p(isNeList) = [0] p(isNePal) = [1] p(isPal) = [0] p(isQid) = [4] x1 + [2] p(n____) = [1] x1 + [1] x2 + [2] p(n__a) = [0] p(n__e) = [0] p(n__i) = [0] p(n__nil) = [1] p(n__o) = [0] p(n__u) = [0] p(nil) = [1] p(o) = [0] p(tt) = [0] p(u) = [0] p(U11#) = [1] p(U21#) = [4] x2 + [6] p(U22#) = [0] p(U31#) = [1] p(U41#) = [4] x2 + [5] p(U42#) = [0] p(U51#) = [4] x2 + [6] p(U52#) = [0] p(U61#) = [2] p(U71#) = [0] p(U72#) = [1] x1 + [0] p(U81#) = [1] p(__#) = [4] x1 + [1] x2 + [4] p(a#) = [1] p(activate#) = [2] x1 + [4] p(e#) = [0] p(i#) = [4] p(isList#) = [4] x1 + [6] p(isNeList#) = [4] x1 + [4] p(isNePal#) = [0] p(isPal#) = [0] p(isQid#) = [0] p(nil#) = [0] p(o#) = [1] p(u#) = [0] p(c_1) = [1] p(c_2) = [1] x1 + [0] p(c_3) = [2] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [1] x1 + [0] p(c_8) = [1] p(c_9) = [1] p(c_10) = [4] x1 + [0] p(c_11) = [4] p(c_12) = [0] p(c_13) = [1] p(c_14) = [0] p(c_15) = [2] x1 + [1] x2 + [1] p(c_16) = [1] p(c_17) = [2] p(c_18) = [0] p(c_19) = [4] x1 + [1] x2 + [2] p(c_20) = [4] p(c_21) = [1] p(c_22) = [4] x1 + [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [1] x1 + [4] p(c_26) = [4] p(c_27) = [0] p(c_28) = [1] x1 + [2] p(c_29) = [1] x1 + [1] x2 + [0] p(c_30) = [1] p(c_31) = [1] x1 + [0] p(c_32) = [1] x1 + [1] x2 + [1] p(c_33) = [1] x1 + [1] x2 + [2] p(c_34) = [1] p(c_35) = [2] x1 + [0] p(c_36) = [2] x1 + [0] p(c_37) = [0] p(c_38) = [1] p(c_39) = [1] p(c_40) = [1] p(c_41) = [1] p(c_42) = [1] p(c_43) = [0] p(c_44) = [0] p(c_45) = [0] Following rules are strictly oriented: U41#(tt(),V2) = [4] V2 + [5] > [4] V2 + [4] = c_5(isNeList#(activate(V2))) Following rules are (at-least) weakly oriented: U21#(tt(),V2) = [4] V2 + [6] >= [4] V2 + [6] = c_2(isList#(activate(V2))) U51#(tt(),V2) = [4] V2 + [6] >= [4] V2 + [6] = c_7(isList#(activate(V2))) U71#(tt(),P) = [0] >= [0] = c_10(isPal#(activate(P))) isList#(V) = [4] V + [6] >= [4] V + [6] = c_28(isNeList#(activate(V))) isList#(n____(V1,V2)) = [4] V1 + [4] V2 + [14] >= [4] V1 + [4] V2 + [12] = c_29(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) = [4] V1 + [4] V2 + [12] >= [4] V1 + [4] V2 + [12] = c_32(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) = [4] V1 + [4] V2 + [12] >= [4] V1 + [4] V2 + [12] = c_33(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) isNePal#(n____(I,n____(P,I))) = [0] >= [0] = c_35(U71#(isQid(activate(I)),activate(P))) isPal#(V) = [0] >= [0] = c_36(isNePal#(activate(V))) __(X,nil()) = [1] X + [3] >= [1] X + [0] = X __(X1,X2) = [1] X1 + [1] X2 + [2] >= [1] X1 + [1] X2 + [2] = n____(X1,X2) __(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [4] >= [1] X + [1] Y + [1] Z + [4] = __(X,__(Y,Z)) __(nil(),X) = [1] X + [3] >= [1] X + [0] = X a() = [0] >= [0] = n__a() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n____(X1,X2)) = [1] X1 + [1] X2 + [2] >= [1] X1 + [1] X2 + [2] = __(activate(X1),activate(X2)) activate(n__a()) = [0] >= [0] = a() activate(n__e()) = [0] >= [0] = e() activate(n__i()) = [0] >= [0] = i() activate(n__nil()) = [1] >= [1] = nil() activate(n__o()) = [0] >= [0] = o() activate(n__u()) = [0] >= [0] = u() e() = [0] >= [0] = n__e() i() = [0] >= [0] = n__i() nil() = [1] >= [1] = n__nil() o() = [0] >= [0] = n__o() u() = [0] >= [0] = n__u() ** Step 7.a:8: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: U51#(tt(),V2) -> c_7(isList#(activate(V2))) isList#(V) -> c_28(isNeList#(activate(V))) - Weak DPs: U21#(tt(),V2) -> c_2(isList#(activate(V2))) U41#(tt(),V2) -> c_5(isNeList#(activate(V2))) U71#(tt(),P) -> c_10(isPal#(activate(P))) isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P))) isPal#(V) -> c_36(isNePal#(activate(V))) - 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() __(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)) -> __(activate(X1),activate(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/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/0 ,c_19/2,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/2,c_30/0,c_31/1,c_32/2,c_33/2 ,c_34/1,c_35/1,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/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 any 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_10) = {1}, uargs(c_28) = {1}, uargs(c_29) = {1,2}, uargs(c_32) = {1,2}, uargs(c_33) = {1,2}, uargs(c_35) = {1}, uargs(c_36) = {1} Following symbols are considered usable: {__,a,activate,e,i,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 + [6] p(U21) = [1] p(U22) = [1] x1 + [2] p(U31) = [6] p(U41) = [1] p(U42) = [6] p(U51) = [1] p(U52) = [1] x1 + [4] p(U61) = [0] p(U71) = [1] x1 + [2] p(U72) = [0] p(U81) = [4] x1 + [1] p(__) = [1] x1 + [1] x2 + [1] p(a) = [0] p(activate) = [1] x1 + [0] p(e) = [0] p(i) = [2] p(isList) = [2] p(isNeList) = [4] p(isNePal) = [4] x1 + [1] p(isPal) = [1] p(isQid) = [4] p(n____) = [1] x1 + [1] x2 + [1] p(n__a) = [0] p(n__e) = [0] p(n__i) = [2] 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#) = [4] x1 + [1] p(U21#) = [2] x2 + [0] p(U22#) = [4] x1 + [0] p(U31#) = [1] x1 + [0] p(U41#) = [2] x2 + [1] p(U42#) = [1] p(U51#) = [2] x2 + [1] p(U52#) = [4] x1 + [0] p(U61#) = [0] p(U71#) = [0] p(U72#) = [1] x1 + [1] p(U81#) = [1] x1 + [1] p(__#) = [2] x1 + [1] p(a#) = [4] p(activate#) = [1] x1 + [1] p(e#) = [1] p(i#) = [1] p(isList#) = [2] x1 + [0] p(isNeList#) = [2] x1 + [0] p(isNePal#) = [0] p(isPal#) = [0] p(isQid#) = [0] p(nil#) = [0] p(o#) = [0] p(u#) = [1] p(c_1) = [2] p(c_2) = [1] x1 + [0] 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) = [0] p(c_9) = [0] p(c_10) = [4] x1 + [0] p(c_11) = [1] p(c_12) = [0] p(c_13) = [1] p(c_14) = [1] p(c_15) = [2] x2 + [4] p(c_16) = [0] p(c_17) = [1] p(c_18) = [0] p(c_19) = [1] x1 + [1] x2 + [1] p(c_20) = [4] x1 + [0] p(c_21) = [4] x1 + [1] p(c_22) = [1] x1 + [2] p(c_23) = [0] p(c_24) = [1] x1 + [0] p(c_25) = [1] p(c_26) = [1] p(c_27) = [1] p(c_28) = [1] x1 + [0] p(c_29) = [1] x1 + [1] x2 + [2] p(c_30) = [2] p(c_31) = [0] p(c_32) = [1] x1 + [1] x2 + [1] p(c_33) = [1] x1 + [1] x2 + [0] p(c_34) = [1] p(c_35) = [2] x1 + [0] p(c_36) = [2] x1 + [0] p(c_37) = [0] p(c_38) = [1] p(c_39) = [1] p(c_40) = [1] p(c_41) = [4] p(c_42) = [4] p(c_43) = [0] p(c_44) = [1] p(c_45) = [2] Following rules are strictly oriented: U51#(tt(),V2) = [2] V2 + [1] > [2] V2 + [0] = c_7(isList#(activate(V2))) 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 + [1] >= [2] V2 + [0] = c_5(isNeList#(activate(V2))) U71#(tt(),P) = [0] >= [0] = c_10(isPal#(activate(P))) isList#(V) = [2] V + [0] >= [2] V + [0] = c_28(isNeList#(activate(V))) isList#(n____(V1,V2)) = [2] V1 + [2] V2 + [2] >= [2] V1 + [2] V2 + [2] = c_29(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) = [2] V1 + [2] V2 + [2] >= [2] V1 + [2] V2 + [2] = c_32(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) = [2] V1 + [2] V2 + [2] >= [2] V1 + [2] V2 + [1] = c_33(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) isNePal#(n____(I,n____(P,I))) = [0] >= [0] = c_35(U71#(isQid(activate(I)),activate(P))) isPal#(V) = [0] >= [0] = c_36(isNePal#(activate(V))) __(X,nil()) = [1] X + [1] >= [1] X + [0] = X __(X1,X2) = [1] X1 + [1] X2 + [1] >= [1] X1 + [1] X2 + [1] = n____(X1,X2) __(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [2] >= [1] X + [1] Y + [1] Z + [2] = __(X,__(Y,Z)) __(nil(),X) = [1] X + [1] >= [1] X + [0] = X 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] = __(activate(X1),activate(X2)) activate(n__a()) = [0] >= [0] = a() activate(n__e()) = [0] >= [0] = e() activate(n__i()) = [2] >= [2] = 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() = [2] >= [2] = n__i() nil() = [0] >= [0] = n__nil() o() = [0] >= [0] = n__o() u() = [0] >= [0] = n__u() ** Step 7.a:9: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: isList#(V) -> c_28(isNeList#(activate(V))) - 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))) U71#(tt(),P) -> c_10(isPal#(activate(P))) isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P))) isPal#(V) -> c_36(isNePal#(activate(V))) - 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() __(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)) -> __(activate(X1),activate(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/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/0 ,c_19/2,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/2,c_30/0,c_31/1,c_32/2,c_33/2 ,c_34/1,c_35/1,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/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 any 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_10) = {1}, uargs(c_28) = {1}, uargs(c_29) = {1,2}, uargs(c_32) = {1,2}, uargs(c_33) = {1,2}, uargs(c_35) = {1}, uargs(c_36) = {1} Following symbols are considered usable: {__,a,activate,e,i,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) = [2] p(U21) = [1] x1 + [5] p(U22) = [0] p(U31) = [2] p(U41) = [2] x1 + [2] p(U42) = [1] x1 + [4] p(U51) = [1] x1 + [1] x2 + [1] p(U52) = [1] x1 + [0] p(U61) = [0] p(U71) = [0] p(U72) = [2] p(U81) = [1] x1 + [2] p(__) = [1] x1 + [1] x2 + [2] p(a) = [0] p(activate) = [1] x1 + [0] p(e) = [4] p(i) = [0] p(isList) = [0] p(isNeList) = [1] x1 + [1] p(isNePal) = [2] x1 + [1] p(isPal) = [1] x1 + [0] p(isQid) = [0] p(n____) = [1] x1 + [1] x2 + [2] p(n__a) = [0] p(n__e) = [4] p(n__i) = [0] p(n__nil) = [0] p(n__o) = [0] p(n__u) = [0] p(nil) = [0] p(o) = [0] p(tt) = [4] p(u) = [0] p(U11#) = [0] p(U21#) = [1] x2 + [1] p(U22#) = [2] p(U31#) = [2] x1 + [0] p(U41#) = [1] x2 + [0] p(U42#) = [4] x1 + [0] p(U51#) = [1] x2 + [1] p(U52#) = [1] p(U61#) = [2] x1 + [1] p(U71#) = [0] p(U72#) = [1] x1 + [1] p(U81#) = [0] p(__#) = [1] p(a#) = [1] p(activate#) = [2] x1 + [2] p(e#) = [4] p(i#) = [1] p(isList#) = [1] x1 + [1] p(isNeList#) = [1] x1 + [0] p(isNePal#) = [0] p(isPal#) = [0] p(isQid#) = [0] p(nil#) = [1] p(o#) = [0] p(u#) = [1] 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) = [2] p(c_7) = [1] x1 + [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [1] x1 + [0] p(c_11) = [1] p(c_12) = [1] p(c_13) = [0] p(c_14) = [1] p(c_15) = [2] p(c_16) = [1] p(c_17) = [2] p(c_18) = [1] p(c_19) = [1] x1 + [1] p(c_20) = [2] x1 + [2] p(c_21) = [0] p(c_22) = [2] x1 + [2] p(c_23) = [0] p(c_24) = [2] p(c_25) = [0] p(c_26) = [4] p(c_27) = [0] p(c_28) = [1] x1 + [0] p(c_29) = [1] x1 + [1] x2 + [1] p(c_30) = [4] p(c_31) = [2] x1 + [0] p(c_32) = [1] x1 + [1] x2 + [0] p(c_33) = [1] x1 + [1] x2 + [1] p(c_34) = [1] x1 + [0] p(c_35) = [4] x1 + [0] p(c_36) = [4] x1 + [0] p(c_37) = [0] p(c_38) = [0] p(c_39) = [0] p(c_40) = [0] p(c_41) = [0] p(c_42) = [1] p(c_43) = [2] p(c_44) = [1] p(c_45) = [0] Following rules are strictly oriented: isList#(V) = [1] V + [1] > [1] V + [0] = c_28(isNeList#(activate(V))) Following rules are (at-least) weakly oriented: U21#(tt(),V2) = [1] V2 + [1] >= [1] V2 + [1] = c_2(isList#(activate(V2))) U41#(tt(),V2) = [1] V2 + [0] >= [1] V2 + [0] = c_5(isNeList#(activate(V2))) U51#(tt(),V2) = [1] V2 + [1] >= [1] V2 + [1] = c_7(isList#(activate(V2))) U71#(tt(),P) = [0] >= [0] = c_10(isPal#(activate(P))) isList#(n____(V1,V2)) = [1] V1 + [1] V2 + [3] >= [1] V1 + [1] V2 + [3] = c_29(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) = [1] V1 + [1] V2 + [2] >= [1] V1 + [1] V2 + [1] = c_32(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) = [1] V1 + [1] V2 + [2] >= [1] V1 + [1] V2 + [2] = c_33(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) isNePal#(n____(I,n____(P,I))) = [0] >= [0] = c_35(U71#(isQid(activate(I)),activate(P))) isPal#(V) = [0] >= [0] = c_36(isNePal#(activate(V))) __(X,nil()) = [1] X + [2] >= [1] X + [0] = X __(X1,X2) = [1] X1 + [1] X2 + [2] >= [1] X1 + [1] X2 + [2] = n____(X1,X2) __(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [4] >= [1] X + [1] Y + [1] Z + [4] = __(X,__(Y,Z)) __(nil(),X) = [1] X + [2] >= [1] X + [0] = X a() = [0] >= [0] = n__a() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n____(X1,X2)) = [1] X1 + [1] X2 + [2] >= [1] X1 + [1] X2 + [2] = __(activate(X1),activate(X2)) activate(n__a()) = [0] >= [0] = a() activate(n__e()) = [4] >= [4] = 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() = [4] >= [4] = n__e() i() = [0] >= [0] = n__i() nil() = [0] >= [0] = n__nil() o() = [0] >= [0] = n__o() u() = [0] >= [0] = n__u() ** Step 7.a:10: EmptyProcessor 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))) U71#(tt(),P) -> c_10(isPal#(activate(P))) isList#(V) -> c_28(isNeList#(activate(V))) isList#(n____(V1,V2)) -> c_29(U21#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_32(U41#(isList(activate(V1)),activate(V2)),isList#(activate(V1))) isNeList#(n____(V1,V2)) -> c_33(U51#(isNeList(activate(V1)),activate(V2)),isNeList#(activate(V1))) isNePal#(n____(I,n____(P,I))) -> c_35(U71#(isQid(activate(I)),activate(P))) isPal#(V) -> c_36(isNePal#(activate(V))) - 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() __(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)) -> __(activate(X1),activate(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/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/0 ,c_19/2,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/1,c_29/2,c_30/0,c_31/1,c_32/2,c_33/2 ,c_34/1,c_35/1,c_36/1,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/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). ** Step 7.b:1: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: activate#(n____(X1,X2)) -> c_19(activate#(X1),activate#(X2)) isNeList#(V) -> c_31(activate#(V)) isNePal#(V) -> c_34(activate#(V)) - Weak DPs: U21#(tt(),V2) -> activate#(V2) U21#(tt(),V2) -> isList#(activate(V2)) U41#(tt(),V2) -> activate#(V2) U41#(tt(),V2) -> isNeList#(activate(V2)) U51#(tt(),V2) -> activate#(V2) U51#(tt(),V2) -> isList#(activate(V2)) U71#(tt(),P) -> activate#(P) U71#(tt(),P) -> isPal#(activate(P)) isList#(V) -> activate#(V) isList#(V) -> isNeList#(activate(V)) isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2)) isList#(n____(V1,V2)) -> activate#(V1) isList#(n____(V1,V2)) -> activate#(V2) isList#(n____(V1,V2)) -> isList#(activate(V1)) isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2)) isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2)) isNeList#(n____(V1,V2)) -> activate#(V1) isNeList#(n____(V1,V2)) -> activate#(V2) isNeList#(n____(V1,V2)) -> isList#(activate(V1)) isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) isNePal#(n____(I,n____(P,I))) -> U71#(isQid(activate(I)),activate(P)) isNePal#(n____(I,n____(P,I))) -> activate#(I) isNePal#(n____(I,n____(P,I))) -> activate#(P) isPal#(V) -> activate#(V) isPal#(V) -> isNePal#(activate(V)) - 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() __(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)) -> __(activate(X1),activate(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/2 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/2,c_8/0,c_9/0,c_10/2,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/0 ,c_19/2,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/4,c_30/0,c_31/1,c_32/4,c_33/4 ,c_34/1,c_35/3,c_36/2,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(U11) = {1}, uargs(U21) = {1,2}, uargs(U22) = {1}, uargs(U31) = {1}, uargs(U41) = {1,2}, uargs(U42) = {1}, uargs(U51) = {1,2}, uargs(U52) = {1}, uargs(__) = {1,2}, uargs(isList) = {1}, uargs(isNeList) = {1}, uargs(isQid) = {1}, uargs(U21#) = {1,2}, uargs(U41#) = {1,2}, uargs(U51#) = {1,2}, uargs(U71#) = {1,2}, uargs(isList#) = {1}, uargs(isNeList#) = {1}, uargs(isNePal#) = {1}, uargs(isPal#) = {1}, uargs(c_19) = {1,2}, uargs(c_31) = {1}, uargs(c_34) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(U11) = [1] x1 + [2] p(U21) = [1] x1 + [1] x2 + [2] p(U22) = [1] x1 + [0] p(U31) = [1] x1 + [0] p(U41) = [1] x1 + [1] x2 + [0] p(U42) = [1] x1 + [0] p(U51) = [1] x1 + [1] x2 + [2] p(U52) = [1] x1 + [0] p(U61) = [0] p(U71) = [0] p(U72) = [0] p(U81) = [0] p(__) = [1] x1 + [1] x2 + [2] p(a) = [0] p(activate) = [1] x1 + [0] p(e) = [4] p(i) = [0] p(isList) = [1] x1 + [2] p(isNeList) = [1] x1 + [0] p(isNePal) = [0] p(isPal) = [0] p(isQid) = [1] x1 + [0] p(n____) = [1] x1 + [1] x2 + [2] p(n__a) = [0] p(n__e) = [4] p(n__i) = [0] p(n__nil) = [0] p(n__o) = [1] p(n__u) = [1] p(nil) = [0] p(o) = [1] p(tt) = [0] p(u) = [1] p(U11#) = [0] p(U21#) = [1] x1 + [1] x2 + [0] p(U22#) = [0] p(U31#) = [0] p(U41#) = [1] x1 + [1] x2 + [0] p(U42#) = [0] p(U51#) = [1] x1 + [1] x2 + [1] p(U52#) = [0] p(U61#) = [0] p(U71#) = [1] x1 + [1] x2 + [4] p(U72#) = [0] p(U81#) = [0] p(__#) = [0] p(a#) = [0] p(activate#) = [1] x1 + [0] p(e#) = [0] p(i#) = [0] p(isList#) = [1] x1 + [0] p(isNeList#) = [1] x1 + [0] p(isNePal#) = [1] x1 + [4] p(isPal#) = [1] x1 + [4] p(isQid#) = [0] p(nil#) = [0] p(o#) = [0] p(u#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [1] x1 + [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [1] x1 + [1] x2 + [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [2] p(c_28) = [2] x2 + [0] p(c_29) = [2] x1 + [2] x2 + [2] x4 + [0] p(c_30) = [0] p(c_31) = [1] x1 + [5] p(c_32) = [1] x1 + [1] x2 + [4] p(c_33) = [1] x2 + [0] p(c_34) = [1] x1 + [1] p(c_35) = [1] x3 + [2] p(c_36) = [4] p(c_37) = [1] p(c_38) = [2] p(c_39) = [0] p(c_40) = [0] p(c_41) = [4] p(c_42) = [1] p(c_43) = [1] p(c_44) = [2] p(c_45) = [4] Following rules are strictly oriented: activate#(n____(X1,X2)) = [1] X1 + [1] X2 + [2] > [1] X1 + [1] X2 + [0] = c_19(activate#(X1),activate#(X2)) isNePal#(V) = [1] V + [4] > [1] V + [1] = c_34(activate#(V)) Following rules are (at-least) weakly oriented: U21#(tt(),V2) = [1] V2 + [0] >= [1] V2 + [0] = activate#(V2) U21#(tt(),V2) = [1] V2 + [0] >= [1] V2 + [0] = isList#(activate(V2)) U41#(tt(),V2) = [1] V2 + [0] >= [1] V2 + [0] = activate#(V2) U41#(tt(),V2) = [1] V2 + [0] >= [1] V2 + [0] = isNeList#(activate(V2)) U51#(tt(),V2) = [1] V2 + [1] >= [1] V2 + [0] = activate#(V2) U51#(tt(),V2) = [1] V2 + [1] >= [1] V2 + [0] = isList#(activate(V2)) U71#(tt(),P) = [1] P + [4] >= [1] P + [0] = activate#(P) U71#(tt(),P) = [1] P + [4] >= [1] P + [4] = isPal#(activate(P)) isList#(V) = [1] V + [0] >= [1] V + [0] = activate#(V) isList#(V) = [1] V + [0] >= [1] V + [0] = isNeList#(activate(V)) isList#(n____(V1,V2)) = [1] V1 + [1] V2 + [2] >= [1] V1 + [1] V2 + [2] = U21#(isList(activate(V1)),activate(V2)) isList#(n____(V1,V2)) = [1] V1 + [1] V2 + [2] >= [1] V1 + [0] = activate#(V1) isList#(n____(V1,V2)) = [1] V1 + [1] V2 + [2] >= [1] V2 + [0] = activate#(V2) isList#(n____(V1,V2)) = [1] V1 + [1] V2 + [2] >= [1] V1 + [0] = isList#(activate(V1)) isNeList#(V) = [1] V + [0] >= [1] V + [5] = c_31(activate#(V)) isNeList#(n____(V1,V2)) = [1] V1 + [1] V2 + [2] >= [1] V1 + [1] V2 + [2] = U41#(isList(activate(V1)),activate(V2)) isNeList#(n____(V1,V2)) = [1] V1 + [1] V2 + [2] >= [1] V1 + [1] V2 + [1] = U51#(isNeList(activate(V1)),activate(V2)) isNeList#(n____(V1,V2)) = [1] V1 + [1] V2 + [2] >= [1] V1 + [0] = activate#(V1) isNeList#(n____(V1,V2)) = [1] V1 + [1] V2 + [2] >= [1] V2 + [0] = activate#(V2) isNeList#(n____(V1,V2)) = [1] V1 + [1] V2 + [2] >= [1] V1 + [0] = isList#(activate(V1)) isNeList#(n____(V1,V2)) = [1] V1 + [1] V2 + [2] >= [1] V1 + [0] = isNeList#(activate(V1)) isNePal#(n____(I,n____(P,I))) = [2] I + [1] P + [8] >= [1] I + [1] P + [4] = U71#(isQid(activate(I)),activate(P)) isNePal#(n____(I,n____(P,I))) = [2] I + [1] P + [8] >= [1] I + [0] = activate#(I) isNePal#(n____(I,n____(P,I))) = [2] I + [1] P + [8] >= [1] P + [0] = activate#(P) isPal#(V) = [1] V + [4] >= [1] V + [0] = activate#(V) isPal#(V) = [1] V + [4] >= [1] V + [4] = isNePal#(activate(V)) U11(tt()) = [2] >= [0] = tt() U21(tt(),V2) = [1] V2 + [2] >= [1] V2 + [2] = U22(isList(activate(V2))) U22(tt()) = [0] >= [0] = tt() U31(tt()) = [0] >= [0] = tt() U41(tt(),V2) = [1] V2 + [0] >= [1] V2 + [0] = U42(isNeList(activate(V2))) U42(tt()) = [0] >= [0] = tt() U51(tt(),V2) = [1] V2 + [2] >= [1] V2 + [2] = U52(isList(activate(V2))) U52(tt()) = [0] >= [0] = tt() __(X,nil()) = [1] X + [2] >= [1] X + [0] = X __(X1,X2) = [1] X1 + [1] X2 + [2] >= [1] X1 + [1] X2 + [2] = n____(X1,X2) __(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [4] >= [1] X + [1] Y + [1] Z + [4] = __(X,__(Y,Z)) __(nil(),X) = [1] X + [2] >= [1] X + [0] = X a() = [0] >= [0] = n__a() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n____(X1,X2)) = [1] X1 + [1] X2 + [2] >= [1] X1 + [1] X2 + [2] = __(activate(X1),activate(X2)) activate(n__a()) = [0] >= [0] = a() activate(n__e()) = [4] >= [4] = e() activate(n__i()) = [0] >= [0] = i() activate(n__nil()) = [0] >= [0] = nil() activate(n__o()) = [1] >= [1] = o() activate(n__u()) = [1] >= [1] = u() e() = [4] >= [4] = n__e() i() = [0] >= [0] = n__i() isList(V) = [1] V + [2] >= [1] V + [2] = U11(isNeList(activate(V))) isList(n____(V1,V2)) = [1] V1 + [1] V2 + [4] >= [1] V1 + [1] V2 + [4] = U21(isList(activate(V1)),activate(V2)) isList(n__nil()) = [2] >= [0] = tt() isNeList(V) = [1] V + [0] >= [1] V + [0] = U31(isQid(activate(V))) isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [2] >= [1] V1 + [1] V2 + [2] = U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [2] >= [1] V1 + [1] V2 + [2] = U51(isNeList(activate(V1)),activate(V2)) isQid(n__a()) = [0] >= [0] = tt() isQid(n__e()) = [4] >= [0] = tt() isQid(n__i()) = [0] >= [0] = tt() isQid(n__o()) = [1] >= [0] = tt() isQid(n__u()) = [1] >= [0] = tt() nil() = [0] >= [0] = n__nil() o() = [1] >= [1] = n__o() u() = [1] >= [1] = n__u() Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.b:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: isNeList#(V) -> c_31(activate#(V)) - Weak DPs: U21#(tt(),V2) -> activate#(V2) U21#(tt(),V2) -> isList#(activate(V2)) U41#(tt(),V2) -> activate#(V2) U41#(tt(),V2) -> isNeList#(activate(V2)) U51#(tt(),V2) -> activate#(V2) U51#(tt(),V2) -> isList#(activate(V2)) U71#(tt(),P) -> activate#(P) U71#(tt(),P) -> isPal#(activate(P)) activate#(n____(X1,X2)) -> c_19(activate#(X1),activate#(X2)) isList#(V) -> activate#(V) isList#(V) -> isNeList#(activate(V)) isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2)) isList#(n____(V1,V2)) -> activate#(V1) isList#(n____(V1,V2)) -> activate#(V2) isList#(n____(V1,V2)) -> isList#(activate(V1)) isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2)) isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2)) isNeList#(n____(V1,V2)) -> activate#(V1) isNeList#(n____(V1,V2)) -> activate#(V2) isNeList#(n____(V1,V2)) -> isList#(activate(V1)) isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) isNePal#(V) -> c_34(activate#(V)) isNePal#(n____(I,n____(P,I))) -> U71#(isQid(activate(I)),activate(P)) isNePal#(n____(I,n____(P,I))) -> activate#(I) isNePal#(n____(I,n____(P,I))) -> activate#(P) isPal#(V) -> activate#(V) isPal#(V) -> isNePal#(activate(V)) - 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() __(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)) -> __(activate(X1),activate(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/2 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/2,c_8/0,c_9/0,c_10/2,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/0 ,c_19/2,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/4,c_30/0,c_31/1,c_32/4,c_33/4 ,c_34/1,c_35/3,c_36/2,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(U11) = {1}, uargs(U21) = {1,2}, uargs(U22) = {1}, uargs(U31) = {1}, uargs(U41) = {1,2}, uargs(U42) = {1}, uargs(U51) = {1,2}, uargs(U52) = {1}, uargs(__) = {1,2}, uargs(isList) = {1}, uargs(isNeList) = {1}, uargs(isQid) = {1}, uargs(U21#) = {1,2}, uargs(U41#) = {1,2}, uargs(U51#) = {1,2}, uargs(U71#) = {1,2}, uargs(isList#) = {1}, uargs(isNeList#) = {1}, uargs(isNePal#) = {1}, uargs(isPal#) = {1}, uargs(c_19) = {1,2}, uargs(c_31) = {1}, uargs(c_34) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(U11) = [1] x1 + [0] p(U21) = [1] x1 + [1] x2 + [1] p(U22) = [1] x1 + [0] p(U31) = [1] x1 + [0] p(U41) = [1] x1 + [1] x2 + [0] p(U42) = [1] x1 + [0] p(U51) = [1] x1 + [1] x2 + [1] p(U52) = [1] x1 + [0] p(U61) = [0] p(U71) = [0] p(U72) = [0] p(U81) = [0] p(__) = [1] x1 + [1] x2 + [1] p(a) = [2] p(activate) = [1] x1 + [0] p(e) = [0] p(i) = [5] p(isList) = [1] x1 + [1] p(isNeList) = [1] x1 + [0] p(isNePal) = [0] p(isPal) = [1] x1 + [0] p(isQid) = [1] x1 + [0] p(n____) = [1] x1 + [1] x2 + [1] p(n__a) = [2] p(n__e) = [0] p(n__i) = [5] 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#) = [1] x1 + [1] x2 + [7] p(U22#) = [0] p(U31#) = [0] p(U41#) = [1] x1 + [1] x2 + [7] p(U42#) = [0] p(U51#) = [1] x1 + [1] x2 + [7] p(U52#) = [0] p(U61#) = [0] p(U71#) = [1] x1 + [1] x2 + [1] p(U72#) = [0] p(U81#) = [0] p(__#) = [0] p(a#) = [0] p(activate#) = [1] x1 + [0] p(e#) = [0] p(i#) = [0] p(isList#) = [1] x1 + [7] p(isNeList#) = [1] x1 + [7] p(isNePal#) = [1] x1 + [1] p(isPal#) = [1] x1 + [1] p(isQid#) = [0] p(nil#) = [0] p(o#) = [0] p(u#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [1] x1 + [1] x2 + [1] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [0] p(c_29) = [0] p(c_30) = [0] p(c_31) = [1] x1 + [0] p(c_32) = [0] p(c_33) = [0] p(c_34) = [1] x1 + [1] p(c_35) = [0] p(c_36) = [0] p(c_37) = [0] p(c_38) = [0] p(c_39) = [0] p(c_40) = [0] p(c_41) = [0] p(c_42) = [0] p(c_43) = [0] p(c_44) = [0] p(c_45) = [0] Following rules are strictly oriented: isNeList#(V) = [1] V + [7] > [1] V + [0] = c_31(activate#(V)) Following rules are (at-least) weakly oriented: U21#(tt(),V2) = [1] V2 + [7] >= [1] V2 + [0] = activate#(V2) U21#(tt(),V2) = [1] V2 + [7] >= [1] V2 + [7] = isList#(activate(V2)) U41#(tt(),V2) = [1] V2 + [7] >= [1] V2 + [0] = activate#(V2) U41#(tt(),V2) = [1] V2 + [7] >= [1] V2 + [7] = isNeList#(activate(V2)) U51#(tt(),V2) = [1] V2 + [7] >= [1] V2 + [0] = activate#(V2) U51#(tt(),V2) = [1] V2 + [7] >= [1] V2 + [7] = isList#(activate(V2)) U71#(tt(),P) = [1] P + [1] >= [1] P + [0] = activate#(P) U71#(tt(),P) = [1] P + [1] >= [1] P + [1] = isPal#(activate(P)) activate#(n____(X1,X2)) = [1] X1 + [1] X2 + [1] >= [1] X1 + [1] X2 + [1] = c_19(activate#(X1),activate#(X2)) isList#(V) = [1] V + [7] >= [1] V + [0] = activate#(V) isList#(V) = [1] V + [7] >= [1] V + [7] = isNeList#(activate(V)) isList#(n____(V1,V2)) = [1] V1 + [1] V2 + [8] >= [1] V1 + [1] V2 + [8] = U21#(isList(activate(V1)),activate(V2)) isList#(n____(V1,V2)) = [1] V1 + [1] V2 + [8] >= [1] V1 + [0] = activate#(V1) isList#(n____(V1,V2)) = [1] V1 + [1] V2 + [8] >= [1] V2 + [0] = activate#(V2) isList#(n____(V1,V2)) = [1] V1 + [1] V2 + [8] >= [1] V1 + [7] = isList#(activate(V1)) isNeList#(n____(V1,V2)) = [1] V1 + [1] V2 + [8] >= [1] V1 + [1] V2 + [8] = U41#(isList(activate(V1)),activate(V2)) isNeList#(n____(V1,V2)) = [1] V1 + [1] V2 + [8] >= [1] V1 + [1] V2 + [7] = U51#(isNeList(activate(V1)),activate(V2)) isNeList#(n____(V1,V2)) = [1] V1 + [1] V2 + [8] >= [1] V1 + [0] = activate#(V1) isNeList#(n____(V1,V2)) = [1] V1 + [1] V2 + [8] >= [1] V2 + [0] = activate#(V2) isNeList#(n____(V1,V2)) = [1] V1 + [1] V2 + [8] >= [1] V1 + [7] = isList#(activate(V1)) isNeList#(n____(V1,V2)) = [1] V1 + [1] V2 + [8] >= [1] V1 + [7] = isNeList#(activate(V1)) isNePal#(V) = [1] V + [1] >= [1] V + [1] = c_34(activate#(V)) isNePal#(n____(I,n____(P,I))) = [2] I + [1] P + [3] >= [1] I + [1] P + [1] = U71#(isQid(activate(I)),activate(P)) isNePal#(n____(I,n____(P,I))) = [2] I + [1] P + [3] >= [1] I + [0] = activate#(I) isNePal#(n____(I,n____(P,I))) = [2] I + [1] P + [3] >= [1] P + [0] = activate#(P) isPal#(V) = [1] V + [1] >= [1] V + [0] = activate#(V) isPal#(V) = [1] V + [1] >= [1] V + [1] = isNePal#(activate(V)) U11(tt()) = [0] >= [0] = tt() U21(tt(),V2) = [1] V2 + [1] >= [1] V2 + [1] = U22(isList(activate(V2))) U22(tt()) = [0] >= [0] = tt() U31(tt()) = [0] >= [0] = tt() U41(tt(),V2) = [1] V2 + [0] >= [1] V2 + [0] = U42(isNeList(activate(V2))) U42(tt()) = [0] >= [0] = tt() U51(tt(),V2) = [1] V2 + [1] >= [1] V2 + [1] = U52(isList(activate(V2))) U52(tt()) = [0] >= [0] = tt() __(X,nil()) = [1] X + [1] >= [1] X + [0] = X __(X1,X2) = [1] X1 + [1] X2 + [1] >= [1] X1 + [1] X2 + [1] = n____(X1,X2) __(__(X,Y),Z) = [1] X + [1] Y + [1] Z + [2] >= [1] X + [1] Y + [1] Z + [2] = __(X,__(Y,Z)) __(nil(),X) = [1] X + [1] >= [1] X + [0] = X a() = [2] >= [2] = 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] = __(activate(X1),activate(X2)) activate(n__a()) = [2] >= [2] = a() activate(n__e()) = [0] >= [0] = e() activate(n__i()) = [5] >= [5] = 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() = [5] >= [5] = n__i() isList(V) = [1] V + [1] >= [1] V + [0] = U11(isNeList(activate(V))) isList(n____(V1,V2)) = [1] V1 + [1] V2 + [2] >= [1] V1 + [1] V2 + [2] = U21(isList(activate(V1)),activate(V2)) isList(n__nil()) = [1] >= [0] = tt() isNeList(V) = [1] V + [0] >= [1] V + [0] = U31(isQid(activate(V))) isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [1] >= [1] V1 + [1] V2 + [1] = U41(isList(activate(V1)),activate(V2)) isNeList(n____(V1,V2)) = [1] V1 + [1] V2 + [1] >= [1] V1 + [1] V2 + [1] = U51(isNeList(activate(V1)),activate(V2)) isQid(n__a()) = [2] >= [0] = tt() isQid(n__e()) = [0] >= [0] = tt() isQid(n__i()) = [5] >= [0] = tt() isQid(n__o()) = [0] >= [0] = tt() isQid(n__u()) = [0] >= [0] = tt() nil() = [0] >= [0] = n__nil() o() = [0] >= [0] = n__o() u() = [0] >= [0] = n__u() Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.b:3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: U21#(tt(),V2) -> activate#(V2) U21#(tt(),V2) -> isList#(activate(V2)) U41#(tt(),V2) -> activate#(V2) U41#(tt(),V2) -> isNeList#(activate(V2)) U51#(tt(),V2) -> activate#(V2) U51#(tt(),V2) -> isList#(activate(V2)) U71#(tt(),P) -> activate#(P) U71#(tt(),P) -> isPal#(activate(P)) activate#(n____(X1,X2)) -> c_19(activate#(X1),activate#(X2)) isList#(V) -> activate#(V) isList#(V) -> isNeList#(activate(V)) isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2)) isList#(n____(V1,V2)) -> activate#(V1) isList#(n____(V1,V2)) -> activate#(V2) isList#(n____(V1,V2)) -> isList#(activate(V1)) isNeList#(V) -> c_31(activate#(V)) isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2)) isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2)) isNeList#(n____(V1,V2)) -> activate#(V1) isNeList#(n____(V1,V2)) -> activate#(V2) isNeList#(n____(V1,V2)) -> isList#(activate(V1)) isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) isNePal#(V) -> c_34(activate#(V)) isNePal#(n____(I,n____(P,I))) -> U71#(isQid(activate(I)),activate(P)) isNePal#(n____(I,n____(P,I))) -> activate#(I) isNePal#(n____(I,n____(P,I))) -> activate#(P) isPal#(V) -> activate#(V) isPal#(V) -> isNePal#(activate(V)) - 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() __(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)) -> __(activate(X1),activate(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/2 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/2,c_8/0,c_9/0,c_10/2,c_11/0,c_12/0,c_13/0,c_14/0,c_15/2,c_16/0,c_17/0,c_18/0 ,c_19/2,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/0,c_27/0,c_28/2,c_29/4,c_30/0,c_31/1,c_32/4,c_33/4 ,c_34/1,c_35/3,c_36/2,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0,c_45/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^2))