YES(O(1),O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { __(X1, X2) -> n____(X1, X2) , __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , nil() -> n__nil() , U11(tt()) -> tt() , U21(tt(), V2) -> U22(isList(activate(V2))) , U22(tt()) -> tt() , isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U31(tt()) -> tt() , U41(tt(), V2) -> U42(isNeList(activate(V2))) , U42(tt()) -> 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)) , U51(tt(), V2) -> U52(isList(activate(V2))) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt(), P) -> U72(isPal(activate(P))) , U72(tt()) -> tt() , isPal(V) -> U81(isNePal(activate(V))) , isPal(n__nil()) -> tt() , U81(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> U61(isQid(activate(V))) , isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(P)) , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Arguments of following rules are not normal-forms: { __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , isNePal(n____(I, __(P, I))) -> U71(isQid(activate(I)), activate(P)) } All above mentioned rules can be savely removed. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , U11(tt()) -> tt() , U21(tt(), V2) -> U22(isList(activate(V2))) , U22(tt()) -> tt() , isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U31(tt()) -> tt() , U41(tt(), V2) -> U42(isNeList(activate(V2))) , U42(tt()) -> 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)) , U51(tt(), V2) -> U52(isList(activate(V2))) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt(), P) -> U72(isPal(activate(P))) , U72(tt()) -> tt() , isPal(V) -> U81(isNePal(activate(V))) , isPal(n__nil()) -> tt() , U81(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> U61(isQid(activate(V))) , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We add the following dependency tuples: Strict DPs: { __^#(X1, X2) -> c_1() , nil^#() -> c_2() , U11^#(tt()) -> c_3() , U21^#(tt(), V2) -> c_4(U22^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , U22^#(tt()) -> c_5() , isList^#(V) -> c_6(U11^#(isNeList(activate(V))), isNeList^#(activate(V)), activate^#(V)) , isList^#(n__nil()) -> c_7() , isList^#(n____(V1, V2)) -> c_8(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , activate^#(X) -> c_9() , activate^#(n__nil()) -> c_10(nil^#()) , activate^#(n____(X1, X2)) -> c_11(__^#(X1, X2)) , activate^#(n__a()) -> c_12(a^#()) , activate^#(n__e()) -> c_13(e^#()) , activate^#(n__i()) -> c_14(i^#()) , activate^#(n__o()) -> c_15(o^#()) , activate^#(n__u()) -> c_16(u^#()) , isNeList^#(V) -> c_20(U31^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) , isNeList^#(n____(V1, V2)) -> c_21(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_22(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , a^#() -> c_37() , e^#() -> c_38() , i^#() -> c_39() , o^#() -> c_40() , u^#() -> c_41() , U31^#(tt()) -> c_17() , U41^#(tt(), V2) -> c_18(U42^#(isNeList(activate(V2))), isNeList^#(activate(V2)), activate^#(V2)) , U42^#(tt()) -> c_19() , isQid^#(n__a()) -> c_31() , isQid^#(n__e()) -> c_32() , isQid^#(n__i()) -> c_33() , isQid^#(n__o()) -> c_34() , isQid^#(n__u()) -> c_35() , U51^#(tt(), V2) -> c_23(U52^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , U52^#(tt()) -> c_24() , U61^#(tt()) -> c_25() , U71^#(tt(), P) -> c_26(U72^#(isPal(activate(P))), isPal^#(activate(P)), activate^#(P)) , U72^#(tt()) -> c_27() , isPal^#(V) -> c_28(U81^#(isNePal(activate(V))), isNePal^#(activate(V)), activate^#(V)) , isPal^#(n__nil()) -> c_29() , U81^#(tt()) -> c_30() , isNePal^#(V) -> c_36(U61^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { __^#(X1, X2) -> c_1() , nil^#() -> c_2() , U11^#(tt()) -> c_3() , U21^#(tt(), V2) -> c_4(U22^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , U22^#(tt()) -> c_5() , isList^#(V) -> c_6(U11^#(isNeList(activate(V))), isNeList^#(activate(V)), activate^#(V)) , isList^#(n__nil()) -> c_7() , isList^#(n____(V1, V2)) -> c_8(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , activate^#(X) -> c_9() , activate^#(n__nil()) -> c_10(nil^#()) , activate^#(n____(X1, X2)) -> c_11(__^#(X1, X2)) , activate^#(n__a()) -> c_12(a^#()) , activate^#(n__e()) -> c_13(e^#()) , activate^#(n__i()) -> c_14(i^#()) , activate^#(n__o()) -> c_15(o^#()) , activate^#(n__u()) -> c_16(u^#()) , isNeList^#(V) -> c_20(U31^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) , isNeList^#(n____(V1, V2)) -> c_21(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_22(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , a^#() -> c_37() , e^#() -> c_38() , i^#() -> c_39() , o^#() -> c_40() , u^#() -> c_41() , U31^#(tt()) -> c_17() , U41^#(tt(), V2) -> c_18(U42^#(isNeList(activate(V2))), isNeList^#(activate(V2)), activate^#(V2)) , U42^#(tt()) -> c_19() , isQid^#(n__a()) -> c_31() , isQid^#(n__e()) -> c_32() , isQid^#(n__i()) -> c_33() , isQid^#(n__o()) -> c_34() , isQid^#(n__u()) -> c_35() , U51^#(tt(), V2) -> c_23(U52^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , U52^#(tt()) -> c_24() , U61^#(tt()) -> c_25() , U71^#(tt(), P) -> c_26(U72^#(isPal(activate(P))), isPal^#(activate(P)), activate^#(P)) , U72^#(tt()) -> c_27() , isPal^#(V) -> c_28(U81^#(isNePal(activate(V))), isNePal^#(activate(V)), activate^#(V)) , isPal^#(n__nil()) -> c_29() , U81^#(tt()) -> c_30() , isNePal^#(V) -> c_36(U61^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) } Weak Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , U11(tt()) -> tt() , U21(tt(), V2) -> U22(isList(activate(V2))) , U22(tt()) -> tt() , isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U31(tt()) -> tt() , U41(tt(), V2) -> U42(isNeList(activate(V2))) , U42(tt()) -> 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)) , U51(tt(), V2) -> U52(isList(activate(V2))) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt(), P) -> U72(isPal(activate(P))) , U72(tt()) -> tt() , isPal(V) -> U81(isNePal(activate(V))) , isPal(n__nil()) -> tt() , U81(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> U61(isQid(activate(V))) , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {1,2,3,5,7,9,20,21,22,23,24,25,27,28,29,30,31,32,34,35,37,39,40} by applications of Pre({1,2,3,5,7,9,20,21,22,23,24,25,27,28,29,30,31,32,34,35,37,39,40}) = {4,6,8,10,11,12,13,14,15,16,17,18,19,26,33,36,38,41}. Here rules are labeled as follows: DPs: { 1: __^#(X1, X2) -> c_1() , 2: nil^#() -> c_2() , 3: U11^#(tt()) -> c_3() , 4: U21^#(tt(), V2) -> c_4(U22^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , 5: U22^#(tt()) -> c_5() , 6: isList^#(V) -> c_6(U11^#(isNeList(activate(V))), isNeList^#(activate(V)), activate^#(V)) , 7: isList^#(n__nil()) -> c_7() , 8: isList^#(n____(V1, V2)) -> c_8(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , 9: activate^#(X) -> c_9() , 10: activate^#(n__nil()) -> c_10(nil^#()) , 11: activate^#(n____(X1, X2)) -> c_11(__^#(X1, X2)) , 12: activate^#(n__a()) -> c_12(a^#()) , 13: activate^#(n__e()) -> c_13(e^#()) , 14: activate^#(n__i()) -> c_14(i^#()) , 15: activate^#(n__o()) -> c_15(o^#()) , 16: activate^#(n__u()) -> c_16(u^#()) , 17: isNeList^#(V) -> c_20(U31^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) , 18: isNeList^#(n____(V1, V2)) -> c_21(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , 19: isNeList^#(n____(V1, V2)) -> c_22(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , 20: a^#() -> c_37() , 21: e^#() -> c_38() , 22: i^#() -> c_39() , 23: o^#() -> c_40() , 24: u^#() -> c_41() , 25: U31^#(tt()) -> c_17() , 26: U41^#(tt(), V2) -> c_18(U42^#(isNeList(activate(V2))), isNeList^#(activate(V2)), activate^#(V2)) , 27: U42^#(tt()) -> c_19() , 28: isQid^#(n__a()) -> c_31() , 29: isQid^#(n__e()) -> c_32() , 30: isQid^#(n__i()) -> c_33() , 31: isQid^#(n__o()) -> c_34() , 32: isQid^#(n__u()) -> c_35() , 33: U51^#(tt(), V2) -> c_23(U52^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , 34: U52^#(tt()) -> c_24() , 35: U61^#(tt()) -> c_25() , 36: U71^#(tt(), P) -> c_26(U72^#(isPal(activate(P))), isPal^#(activate(P)), activate^#(P)) , 37: U72^#(tt()) -> c_27() , 38: isPal^#(V) -> c_28(U81^#(isNePal(activate(V))), isNePal^#(activate(V)), activate^#(V)) , 39: isPal^#(n__nil()) -> c_29() , 40: U81^#(tt()) -> c_30() , 41: isNePal^#(V) -> c_36(U61^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { U21^#(tt(), V2) -> c_4(U22^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , isList^#(V) -> c_6(U11^#(isNeList(activate(V))), isNeList^#(activate(V)), activate^#(V)) , isList^#(n____(V1, V2)) -> c_8(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , activate^#(n__nil()) -> c_10(nil^#()) , activate^#(n____(X1, X2)) -> c_11(__^#(X1, X2)) , activate^#(n__a()) -> c_12(a^#()) , activate^#(n__e()) -> c_13(e^#()) , activate^#(n__i()) -> c_14(i^#()) , activate^#(n__o()) -> c_15(o^#()) , activate^#(n__u()) -> c_16(u^#()) , isNeList^#(V) -> c_20(U31^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) , isNeList^#(n____(V1, V2)) -> c_21(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_22(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , U41^#(tt(), V2) -> c_18(U42^#(isNeList(activate(V2))), isNeList^#(activate(V2)), activate^#(V2)) , U51^#(tt(), V2) -> c_23(U52^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , U71^#(tt(), P) -> c_26(U72^#(isPal(activate(P))), isPal^#(activate(P)), activate^#(P)) , isPal^#(V) -> c_28(U81^#(isNePal(activate(V))), isNePal^#(activate(V)), activate^#(V)) , isNePal^#(V) -> c_36(U61^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) } Weak DPs: { __^#(X1, X2) -> c_1() , nil^#() -> c_2() , U11^#(tt()) -> c_3() , U22^#(tt()) -> c_5() , isList^#(n__nil()) -> c_7() , activate^#(X) -> c_9() , a^#() -> c_37() , e^#() -> c_38() , i^#() -> c_39() , o^#() -> c_40() , u^#() -> c_41() , U31^#(tt()) -> c_17() , U42^#(tt()) -> c_19() , isQid^#(n__a()) -> c_31() , isQid^#(n__e()) -> c_32() , isQid^#(n__i()) -> c_33() , isQid^#(n__o()) -> c_34() , isQid^#(n__u()) -> c_35() , U52^#(tt()) -> c_24() , U61^#(tt()) -> c_25() , U72^#(tt()) -> c_27() , isPal^#(n__nil()) -> c_29() , U81^#(tt()) -> c_30() } Weak Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , U11(tt()) -> tt() , U21(tt(), V2) -> U22(isList(activate(V2))) , U22(tt()) -> tt() , isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U31(tt()) -> tt() , U41(tt(), V2) -> U42(isNeList(activate(V2))) , U42(tt()) -> 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)) , U51(tt(), V2) -> U52(isList(activate(V2))) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt(), P) -> U72(isPal(activate(P))) , U72(tt()) -> tt() , isPal(V) -> U81(isNePal(activate(V))) , isPal(n__nil()) -> tt() , U81(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> U61(isQid(activate(V))) , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {4,5,6,7,8,9,10} by applications of Pre({4,5,6,7,8,9,10}) = {1,2,3,11,12,13,14,15,16,17,18}. Here rules are labeled as follows: DPs: { 1: U21^#(tt(), V2) -> c_4(U22^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , 2: isList^#(V) -> c_6(U11^#(isNeList(activate(V))), isNeList^#(activate(V)), activate^#(V)) , 3: isList^#(n____(V1, V2)) -> c_8(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , 4: activate^#(n__nil()) -> c_10(nil^#()) , 5: activate^#(n____(X1, X2)) -> c_11(__^#(X1, X2)) , 6: activate^#(n__a()) -> c_12(a^#()) , 7: activate^#(n__e()) -> c_13(e^#()) , 8: activate^#(n__i()) -> c_14(i^#()) , 9: activate^#(n__o()) -> c_15(o^#()) , 10: activate^#(n__u()) -> c_16(u^#()) , 11: isNeList^#(V) -> c_20(U31^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) , 12: isNeList^#(n____(V1, V2)) -> c_21(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , 13: isNeList^#(n____(V1, V2)) -> c_22(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , 14: U41^#(tt(), V2) -> c_18(U42^#(isNeList(activate(V2))), isNeList^#(activate(V2)), activate^#(V2)) , 15: U51^#(tt(), V2) -> c_23(U52^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , 16: U71^#(tt(), P) -> c_26(U72^#(isPal(activate(P))), isPal^#(activate(P)), activate^#(P)) , 17: isPal^#(V) -> c_28(U81^#(isNePal(activate(V))), isNePal^#(activate(V)), activate^#(V)) , 18: isNePal^#(V) -> c_36(U61^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) , 19: __^#(X1, X2) -> c_1() , 20: nil^#() -> c_2() , 21: U11^#(tt()) -> c_3() , 22: U22^#(tt()) -> c_5() , 23: isList^#(n__nil()) -> c_7() , 24: activate^#(X) -> c_9() , 25: a^#() -> c_37() , 26: e^#() -> c_38() , 27: i^#() -> c_39() , 28: o^#() -> c_40() , 29: u^#() -> c_41() , 30: U31^#(tt()) -> c_17() , 31: U42^#(tt()) -> c_19() , 32: isQid^#(n__a()) -> c_31() , 33: isQid^#(n__e()) -> c_32() , 34: isQid^#(n__i()) -> c_33() , 35: isQid^#(n__o()) -> c_34() , 36: isQid^#(n__u()) -> c_35() , 37: U52^#(tt()) -> c_24() , 38: U61^#(tt()) -> c_25() , 39: U72^#(tt()) -> c_27() , 40: isPal^#(n__nil()) -> c_29() , 41: U81^#(tt()) -> c_30() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { U21^#(tt(), V2) -> c_4(U22^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , isList^#(V) -> c_6(U11^#(isNeList(activate(V))), isNeList^#(activate(V)), activate^#(V)) , isList^#(n____(V1, V2)) -> c_8(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(V) -> c_20(U31^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) , isNeList^#(n____(V1, V2)) -> c_21(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_22(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , U41^#(tt(), V2) -> c_18(U42^#(isNeList(activate(V2))), isNeList^#(activate(V2)), activate^#(V2)) , U51^#(tt(), V2) -> c_23(U52^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , U71^#(tt(), P) -> c_26(U72^#(isPal(activate(P))), isPal^#(activate(P)), activate^#(P)) , isPal^#(V) -> c_28(U81^#(isNePal(activate(V))), isNePal^#(activate(V)), activate^#(V)) , isNePal^#(V) -> c_36(U61^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) } Weak DPs: { __^#(X1, X2) -> c_1() , nil^#() -> c_2() , U11^#(tt()) -> c_3() , U22^#(tt()) -> c_5() , isList^#(n__nil()) -> c_7() , activate^#(X) -> c_9() , activate^#(n__nil()) -> c_10(nil^#()) , activate^#(n____(X1, X2)) -> c_11(__^#(X1, X2)) , activate^#(n__a()) -> c_12(a^#()) , activate^#(n__e()) -> c_13(e^#()) , activate^#(n__i()) -> c_14(i^#()) , activate^#(n__o()) -> c_15(o^#()) , activate^#(n__u()) -> c_16(u^#()) , a^#() -> c_37() , e^#() -> c_38() , i^#() -> c_39() , o^#() -> c_40() , u^#() -> c_41() , U31^#(tt()) -> c_17() , U42^#(tt()) -> c_19() , isQid^#(n__a()) -> c_31() , isQid^#(n__e()) -> c_32() , isQid^#(n__i()) -> c_33() , isQid^#(n__o()) -> c_34() , isQid^#(n__u()) -> c_35() , U52^#(tt()) -> c_24() , U61^#(tt()) -> c_25() , U72^#(tt()) -> c_27() , isPal^#(n__nil()) -> c_29() , U81^#(tt()) -> c_30() } Weak Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , U11(tt()) -> tt() , U21(tt(), V2) -> U22(isList(activate(V2))) , U22(tt()) -> tt() , isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U31(tt()) -> tt() , U41(tt(), V2) -> U42(isNeList(activate(V2))) , U42(tt()) -> 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)) , U51(tt(), V2) -> U52(isList(activate(V2))) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt(), P) -> U72(isPal(activate(P))) , U72(tt()) -> tt() , isPal(V) -> U81(isNePal(activate(V))) , isPal(n__nil()) -> tt() , U81(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> U61(isQid(activate(V))) , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {4,11} by applications of Pre({4,11}) = {2,6,7,10}. Here rules are labeled as follows: DPs: { 1: U21^#(tt(), V2) -> c_4(U22^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , 2: isList^#(V) -> c_6(U11^#(isNeList(activate(V))), isNeList^#(activate(V)), activate^#(V)) , 3: isList^#(n____(V1, V2)) -> c_8(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , 4: isNeList^#(V) -> c_20(U31^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) , 5: isNeList^#(n____(V1, V2)) -> c_21(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , 6: isNeList^#(n____(V1, V2)) -> c_22(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , 7: U41^#(tt(), V2) -> c_18(U42^#(isNeList(activate(V2))), isNeList^#(activate(V2)), activate^#(V2)) , 8: U51^#(tt(), V2) -> c_23(U52^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , 9: U71^#(tt(), P) -> c_26(U72^#(isPal(activate(P))), isPal^#(activate(P)), activate^#(P)) , 10: isPal^#(V) -> c_28(U81^#(isNePal(activate(V))), isNePal^#(activate(V)), activate^#(V)) , 11: isNePal^#(V) -> c_36(U61^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) , 12: __^#(X1, X2) -> c_1() , 13: nil^#() -> c_2() , 14: U11^#(tt()) -> c_3() , 15: U22^#(tt()) -> c_5() , 16: isList^#(n__nil()) -> c_7() , 17: activate^#(X) -> c_9() , 18: activate^#(n__nil()) -> c_10(nil^#()) , 19: activate^#(n____(X1, X2)) -> c_11(__^#(X1, X2)) , 20: activate^#(n__a()) -> c_12(a^#()) , 21: activate^#(n__e()) -> c_13(e^#()) , 22: activate^#(n__i()) -> c_14(i^#()) , 23: activate^#(n__o()) -> c_15(o^#()) , 24: activate^#(n__u()) -> c_16(u^#()) , 25: a^#() -> c_37() , 26: e^#() -> c_38() , 27: i^#() -> c_39() , 28: o^#() -> c_40() , 29: u^#() -> c_41() , 30: U31^#(tt()) -> c_17() , 31: U42^#(tt()) -> c_19() , 32: isQid^#(n__a()) -> c_31() , 33: isQid^#(n__e()) -> c_32() , 34: isQid^#(n__i()) -> c_33() , 35: isQid^#(n__o()) -> c_34() , 36: isQid^#(n__u()) -> c_35() , 37: U52^#(tt()) -> c_24() , 38: U61^#(tt()) -> c_25() , 39: U72^#(tt()) -> c_27() , 40: isPal^#(n__nil()) -> c_29() , 41: U81^#(tt()) -> c_30() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { U21^#(tt(), V2) -> c_4(U22^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , isList^#(V) -> c_6(U11^#(isNeList(activate(V))), isNeList^#(activate(V)), activate^#(V)) , isList^#(n____(V1, V2)) -> c_8(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_21(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_22(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , U41^#(tt(), V2) -> c_18(U42^#(isNeList(activate(V2))), isNeList^#(activate(V2)), activate^#(V2)) , U51^#(tt(), V2) -> c_23(U52^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , U71^#(tt(), P) -> c_26(U72^#(isPal(activate(P))), isPal^#(activate(P)), activate^#(P)) , isPal^#(V) -> c_28(U81^#(isNePal(activate(V))), isNePal^#(activate(V)), activate^#(V)) } Weak DPs: { __^#(X1, X2) -> c_1() , nil^#() -> c_2() , U11^#(tt()) -> c_3() , U22^#(tt()) -> c_5() , isList^#(n__nil()) -> c_7() , activate^#(X) -> c_9() , activate^#(n__nil()) -> c_10(nil^#()) , activate^#(n____(X1, X2)) -> c_11(__^#(X1, X2)) , activate^#(n__a()) -> c_12(a^#()) , activate^#(n__e()) -> c_13(e^#()) , activate^#(n__i()) -> c_14(i^#()) , activate^#(n__o()) -> c_15(o^#()) , activate^#(n__u()) -> c_16(u^#()) , isNeList^#(V) -> c_20(U31^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) , a^#() -> c_37() , e^#() -> c_38() , i^#() -> c_39() , o^#() -> c_40() , u^#() -> c_41() , U31^#(tt()) -> c_17() , U42^#(tt()) -> c_19() , isQid^#(n__a()) -> c_31() , isQid^#(n__e()) -> c_32() , isQid^#(n__i()) -> c_33() , isQid^#(n__o()) -> c_34() , isQid^#(n__u()) -> c_35() , U52^#(tt()) -> c_24() , U61^#(tt()) -> c_25() , U72^#(tt()) -> c_27() , isPal^#(n__nil()) -> c_29() , U81^#(tt()) -> c_30() , isNePal^#(V) -> c_36(U61^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) } Weak Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , U11(tt()) -> tt() , U21(tt(), V2) -> U22(isList(activate(V2))) , U22(tt()) -> tt() , isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U31(tt()) -> tt() , U41(tt(), V2) -> U42(isNeList(activate(V2))) , U42(tt()) -> 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)) , U51(tt(), V2) -> U52(isList(activate(V2))) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt(), P) -> U72(isPal(activate(P))) , U72(tt()) -> tt() , isPal(V) -> U81(isNePal(activate(V))) , isPal(n__nil()) -> tt() , U81(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> U61(isQid(activate(V))) , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {9} by applications of Pre({9}) = {8}. Here rules are labeled as follows: DPs: { 1: U21^#(tt(), V2) -> c_4(U22^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , 2: isList^#(V) -> c_6(U11^#(isNeList(activate(V))), isNeList^#(activate(V)), activate^#(V)) , 3: isList^#(n____(V1, V2)) -> c_8(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , 4: isNeList^#(n____(V1, V2)) -> c_21(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , 5: isNeList^#(n____(V1, V2)) -> c_22(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , 6: U41^#(tt(), V2) -> c_18(U42^#(isNeList(activate(V2))), isNeList^#(activate(V2)), activate^#(V2)) , 7: U51^#(tt(), V2) -> c_23(U52^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , 8: U71^#(tt(), P) -> c_26(U72^#(isPal(activate(P))), isPal^#(activate(P)), activate^#(P)) , 9: isPal^#(V) -> c_28(U81^#(isNePal(activate(V))), isNePal^#(activate(V)), activate^#(V)) , 10: __^#(X1, X2) -> c_1() , 11: nil^#() -> c_2() , 12: U11^#(tt()) -> c_3() , 13: U22^#(tt()) -> c_5() , 14: isList^#(n__nil()) -> c_7() , 15: activate^#(X) -> c_9() , 16: activate^#(n__nil()) -> c_10(nil^#()) , 17: activate^#(n____(X1, X2)) -> c_11(__^#(X1, X2)) , 18: activate^#(n__a()) -> c_12(a^#()) , 19: activate^#(n__e()) -> c_13(e^#()) , 20: activate^#(n__i()) -> c_14(i^#()) , 21: activate^#(n__o()) -> c_15(o^#()) , 22: activate^#(n__u()) -> c_16(u^#()) , 23: isNeList^#(V) -> c_20(U31^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) , 24: a^#() -> c_37() , 25: e^#() -> c_38() , 26: i^#() -> c_39() , 27: o^#() -> c_40() , 28: u^#() -> c_41() , 29: U31^#(tt()) -> c_17() , 30: U42^#(tt()) -> c_19() , 31: isQid^#(n__a()) -> c_31() , 32: isQid^#(n__e()) -> c_32() , 33: isQid^#(n__i()) -> c_33() , 34: isQid^#(n__o()) -> c_34() , 35: isQid^#(n__u()) -> c_35() , 36: U52^#(tt()) -> c_24() , 37: U61^#(tt()) -> c_25() , 38: U72^#(tt()) -> c_27() , 39: isPal^#(n__nil()) -> c_29() , 40: U81^#(tt()) -> c_30() , 41: isNePal^#(V) -> c_36(U61^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { U21^#(tt(), V2) -> c_4(U22^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , isList^#(V) -> c_6(U11^#(isNeList(activate(V))), isNeList^#(activate(V)), activate^#(V)) , isList^#(n____(V1, V2)) -> c_8(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_21(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_22(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , U41^#(tt(), V2) -> c_18(U42^#(isNeList(activate(V2))), isNeList^#(activate(V2)), activate^#(V2)) , U51^#(tt(), V2) -> c_23(U52^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , U71^#(tt(), P) -> c_26(U72^#(isPal(activate(P))), isPal^#(activate(P)), activate^#(P)) } Weak DPs: { __^#(X1, X2) -> c_1() , nil^#() -> c_2() , U11^#(tt()) -> c_3() , U22^#(tt()) -> c_5() , isList^#(n__nil()) -> c_7() , activate^#(X) -> c_9() , activate^#(n__nil()) -> c_10(nil^#()) , activate^#(n____(X1, X2)) -> c_11(__^#(X1, X2)) , activate^#(n__a()) -> c_12(a^#()) , activate^#(n__e()) -> c_13(e^#()) , activate^#(n__i()) -> c_14(i^#()) , activate^#(n__o()) -> c_15(o^#()) , activate^#(n__u()) -> c_16(u^#()) , isNeList^#(V) -> c_20(U31^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) , a^#() -> c_37() , e^#() -> c_38() , i^#() -> c_39() , o^#() -> c_40() , u^#() -> c_41() , U31^#(tt()) -> c_17() , U42^#(tt()) -> c_19() , isQid^#(n__a()) -> c_31() , isQid^#(n__e()) -> c_32() , isQid^#(n__i()) -> c_33() , isQid^#(n__o()) -> c_34() , isQid^#(n__u()) -> c_35() , U52^#(tt()) -> c_24() , U61^#(tt()) -> c_25() , U72^#(tt()) -> c_27() , isPal^#(V) -> c_28(U81^#(isNePal(activate(V))), isNePal^#(activate(V)), activate^#(V)) , isPal^#(n__nil()) -> c_29() , U81^#(tt()) -> c_30() , isNePal^#(V) -> c_36(U61^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) } Weak Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , U11(tt()) -> tt() , U21(tt(), V2) -> U22(isList(activate(V2))) , U22(tt()) -> tt() , isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U31(tt()) -> tt() , U41(tt(), V2) -> U42(isNeList(activate(V2))) , U42(tt()) -> 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)) , U51(tt(), V2) -> U52(isList(activate(V2))) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt(), P) -> U72(isPal(activate(P))) , U72(tt()) -> tt() , isPal(V) -> U81(isNePal(activate(V))) , isPal(n__nil()) -> tt() , U81(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> U61(isQid(activate(V))) , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We estimate the number of application of {8} by applications of Pre({8}) = {}. Here rules are labeled as follows: DPs: { 1: U21^#(tt(), V2) -> c_4(U22^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , 2: isList^#(V) -> c_6(U11^#(isNeList(activate(V))), isNeList^#(activate(V)), activate^#(V)) , 3: isList^#(n____(V1, V2)) -> c_8(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , 4: isNeList^#(n____(V1, V2)) -> c_21(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , 5: isNeList^#(n____(V1, V2)) -> c_22(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , 6: U41^#(tt(), V2) -> c_18(U42^#(isNeList(activate(V2))), isNeList^#(activate(V2)), activate^#(V2)) , 7: U51^#(tt(), V2) -> c_23(U52^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , 8: U71^#(tt(), P) -> c_26(U72^#(isPal(activate(P))), isPal^#(activate(P)), activate^#(P)) , 9: __^#(X1, X2) -> c_1() , 10: nil^#() -> c_2() , 11: U11^#(tt()) -> c_3() , 12: U22^#(tt()) -> c_5() , 13: isList^#(n__nil()) -> c_7() , 14: activate^#(X) -> c_9() , 15: activate^#(n__nil()) -> c_10(nil^#()) , 16: activate^#(n____(X1, X2)) -> c_11(__^#(X1, X2)) , 17: activate^#(n__a()) -> c_12(a^#()) , 18: activate^#(n__e()) -> c_13(e^#()) , 19: activate^#(n__i()) -> c_14(i^#()) , 20: activate^#(n__o()) -> c_15(o^#()) , 21: activate^#(n__u()) -> c_16(u^#()) , 22: isNeList^#(V) -> c_20(U31^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) , 23: a^#() -> c_37() , 24: e^#() -> c_38() , 25: i^#() -> c_39() , 26: o^#() -> c_40() , 27: u^#() -> c_41() , 28: U31^#(tt()) -> c_17() , 29: U42^#(tt()) -> c_19() , 30: isQid^#(n__a()) -> c_31() , 31: isQid^#(n__e()) -> c_32() , 32: isQid^#(n__i()) -> c_33() , 33: isQid^#(n__o()) -> c_34() , 34: isQid^#(n__u()) -> c_35() , 35: U52^#(tt()) -> c_24() , 36: U61^#(tt()) -> c_25() , 37: U72^#(tt()) -> c_27() , 38: isPal^#(V) -> c_28(U81^#(isNePal(activate(V))), isNePal^#(activate(V)), activate^#(V)) , 39: isPal^#(n__nil()) -> c_29() , 40: U81^#(tt()) -> c_30() , 41: isNePal^#(V) -> c_36(U61^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { U21^#(tt(), V2) -> c_4(U22^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , isList^#(V) -> c_6(U11^#(isNeList(activate(V))), isNeList^#(activate(V)), activate^#(V)) , isList^#(n____(V1, V2)) -> c_8(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_21(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_22(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , U41^#(tt(), V2) -> c_18(U42^#(isNeList(activate(V2))), isNeList^#(activate(V2)), activate^#(V2)) , U51^#(tt(), V2) -> c_23(U52^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) } Weak DPs: { __^#(X1, X2) -> c_1() , nil^#() -> c_2() , U11^#(tt()) -> c_3() , U22^#(tt()) -> c_5() , isList^#(n__nil()) -> c_7() , activate^#(X) -> c_9() , activate^#(n__nil()) -> c_10(nil^#()) , activate^#(n____(X1, X2)) -> c_11(__^#(X1, X2)) , activate^#(n__a()) -> c_12(a^#()) , activate^#(n__e()) -> c_13(e^#()) , activate^#(n__i()) -> c_14(i^#()) , activate^#(n__o()) -> c_15(o^#()) , activate^#(n__u()) -> c_16(u^#()) , isNeList^#(V) -> c_20(U31^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) , a^#() -> c_37() , e^#() -> c_38() , i^#() -> c_39() , o^#() -> c_40() , u^#() -> c_41() , U31^#(tt()) -> c_17() , U42^#(tt()) -> c_19() , isQid^#(n__a()) -> c_31() , isQid^#(n__e()) -> c_32() , isQid^#(n__i()) -> c_33() , isQid^#(n__o()) -> c_34() , isQid^#(n__u()) -> c_35() , U52^#(tt()) -> c_24() , U61^#(tt()) -> c_25() , U71^#(tt(), P) -> c_26(U72^#(isPal(activate(P))), isPal^#(activate(P)), activate^#(P)) , U72^#(tt()) -> c_27() , isPal^#(V) -> c_28(U81^#(isNePal(activate(V))), isNePal^#(activate(V)), activate^#(V)) , isPal^#(n__nil()) -> c_29() , U81^#(tt()) -> c_30() , isNePal^#(V) -> c_36(U61^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) } Weak Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , U11(tt()) -> tt() , U21(tt(), V2) -> U22(isList(activate(V2))) , U22(tt()) -> tt() , isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U31(tt()) -> tt() , U41(tt(), V2) -> U42(isNeList(activate(V2))) , U42(tt()) -> 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)) , U51(tt(), V2) -> U52(isList(activate(V2))) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt(), P) -> U72(isPal(activate(P))) , U72(tt()) -> tt() , isPal(V) -> U81(isNePal(activate(V))) , isPal(n__nil()) -> tt() , U81(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> U61(isQid(activate(V))) , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { __^#(X1, X2) -> c_1() , nil^#() -> c_2() , U11^#(tt()) -> c_3() , U22^#(tt()) -> c_5() , isList^#(n__nil()) -> c_7() , activate^#(X) -> c_9() , activate^#(n__nil()) -> c_10(nil^#()) , activate^#(n____(X1, X2)) -> c_11(__^#(X1, X2)) , activate^#(n__a()) -> c_12(a^#()) , activate^#(n__e()) -> c_13(e^#()) , activate^#(n__i()) -> c_14(i^#()) , activate^#(n__o()) -> c_15(o^#()) , activate^#(n__u()) -> c_16(u^#()) , isNeList^#(V) -> c_20(U31^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) , a^#() -> c_37() , e^#() -> c_38() , i^#() -> c_39() , o^#() -> c_40() , u^#() -> c_41() , U31^#(tt()) -> c_17() , U42^#(tt()) -> c_19() , isQid^#(n__a()) -> c_31() , isQid^#(n__e()) -> c_32() , isQid^#(n__i()) -> c_33() , isQid^#(n__o()) -> c_34() , isQid^#(n__u()) -> c_35() , U52^#(tt()) -> c_24() , U61^#(tt()) -> c_25() , U71^#(tt(), P) -> c_26(U72^#(isPal(activate(P))), isPal^#(activate(P)), activate^#(P)) , U72^#(tt()) -> c_27() , isPal^#(V) -> c_28(U81^#(isNePal(activate(V))), isNePal^#(activate(V)), activate^#(V)) , isPal^#(n__nil()) -> c_29() , U81^#(tt()) -> c_30() , isNePal^#(V) -> c_36(U61^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { U21^#(tt(), V2) -> c_4(U22^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , isList^#(V) -> c_6(U11^#(isNeList(activate(V))), isNeList^#(activate(V)), activate^#(V)) , isList^#(n____(V1, V2)) -> c_8(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_21(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_22(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , U41^#(tt(), V2) -> c_18(U42^#(isNeList(activate(V2))), isNeList^#(activate(V2)), activate^#(V2)) , U51^#(tt(), V2) -> c_23(U52^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) } Weak Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , U11(tt()) -> tt() , U21(tt(), V2) -> U22(isList(activate(V2))) , U22(tt()) -> tt() , isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U31(tt()) -> tt() , U41(tt(), V2) -> U42(isNeList(activate(V2))) , U42(tt()) -> 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)) , U51(tt(), V2) -> U52(isList(activate(V2))) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt(), P) -> U72(isPal(activate(P))) , U72(tt()) -> tt() , isPal(V) -> U81(isNePal(activate(V))) , isPal(n__nil()) -> tt() , U81(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> U61(isQid(activate(V))) , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { U21^#(tt(), V2) -> c_4(U22^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) , isList^#(V) -> c_6(U11^#(isNeList(activate(V))), isNeList^#(activate(V)), activate^#(V)) , isList^#(n____(V1, V2)) -> c_8(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_21(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_22(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , U41^#(tt(), V2) -> c_18(U42^#(isNeList(activate(V2))), isNeList^#(activate(V2)), activate^#(V2)) , U51^#(tt(), V2) -> c_23(U52^#(isList(activate(V2))), isList^#(activate(V2)), activate^#(V2)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { U21^#(tt(), V2) -> c_1(isList^#(activate(V2))) , isList^#(V) -> c_2(isNeList^#(activate(V))) , isList^#(n____(V1, V2)) -> c_3(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1))) , isNeList^#(n____(V1, V2)) -> c_4(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1))) , isNeList^#(n____(V1, V2)) -> c_5(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1))) , U41^#(tt(), V2) -> c_6(isNeList^#(activate(V2))) , U51^#(tt(), V2) -> c_7(isList^#(activate(V2))) } Weak Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , U11(tt()) -> tt() , U21(tt(), V2) -> U22(isList(activate(V2))) , U22(tt()) -> tt() , isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U31(tt()) -> tt() , U41(tt(), V2) -> U42(isNeList(activate(V2))) , U42(tt()) -> 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)) , U51(tt(), V2) -> U52(isList(activate(V2))) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt(), P) -> U72(isPal(activate(P))) , U72(tt()) -> tt() , isPal(V) -> U81(isNePal(activate(V))) , isPal(n__nil()) -> tt() , U81(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , isNePal(V) -> U61(isQid(activate(V))) , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We replace rewrite rules by usable rules: Weak Usable Rules: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , U11(tt()) -> tt() , U21(tt(), V2) -> U22(isList(activate(V2))) , U22(tt()) -> tt() , isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U31(tt()) -> tt() , U41(tt(), V2) -> U42(isNeList(activate(V2))) , U42(tt()) -> 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)) , U51(tt(), V2) -> U52(isList(activate(V2))) , U52(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { U21^#(tt(), V2) -> c_1(isList^#(activate(V2))) , isList^#(V) -> c_2(isNeList^#(activate(V))) , isList^#(n____(V1, V2)) -> c_3(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1))) , isNeList^#(n____(V1, V2)) -> c_4(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1))) , isNeList^#(n____(V1, V2)) -> c_5(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1))) , U41^#(tt(), V2) -> c_6(isNeList^#(activate(V2))) , U51^#(tt(), V2) -> c_7(isList^#(activate(V2))) } Weak Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , U11(tt()) -> tt() , U21(tt(), V2) -> U22(isList(activate(V2))) , U22(tt()) -> tt() , isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U31(tt()) -> tt() , U41(tt(), V2) -> U42(isNeList(activate(V2))) , U42(tt()) -> 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)) , U51(tt(), V2) -> U52(isList(activate(V2))) , U52(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 3: isList^#(n____(V1, V2)) -> c_3(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1))) , 4: isNeList^#(n____(V1, V2)) -> c_4(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1))) , 5: isNeList^#(n____(V1, V2)) -> c_5(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1))) , 7: U51^#(tt(), V2) -> c_7(isList^#(activate(V2))) } Trs: { U22(tt()) -> tt() , isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2}, Uargs(c_4) = {1, 2}, Uargs(c_5) = {1, 2}, Uargs(c_6) = {1}, Uargs(c_7) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [__](x1, x2) = [1] x1 + [1] x2 + [7] [nil] = [0] [U11](x1) = [1] [tt] = [1] [U21](x1, x2) = [2] [U22](x1) = [2] [isList](x1) = [2] [activate](x1) = [1] x1 + [0] [U31](x1) = [1] [U41](x1, x2) = [1] [U42](x1) = [1] [isNeList](x1) = [1] [U51](x1, x2) = [1] [U52](x1) = [1] [U61](x1) = [7] x1 + [0] [U71](x1, x2) = [7] x1 + [7] x2 + [0] [U72](x1) = [7] x1 + [0] [isPal](x1) = [7] x1 + [0] [U81](x1) = [7] x1 + [0] [n__nil] = [0] [n____](x1, x2) = [1] x1 + [1] x2 + [7] [isQid](x1) = [1] [isNePal](x1) = [7] x1 + [0] [n__a] = [0] [n__e] = [0] [n__i] = [0] [n__o] = [0] [n__u] = [0] [a] = [0] [e] = [0] [i] = [0] [o] = [0] [u] = [0] [__^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_1] = [0] [nil^#] = [0] [c_2] = [0] [U11^#](x1) = [7] x1 + [0] [c_3] = [0] [U21^#](x1, x2) = [1] x2 + [2] [c_4](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U22^#](x1) = [7] x1 + [0] [isList^#](x1) = [1] x1 + [1] [activate^#](x1) = [7] x1 + [0] [c_5] = [0] [c_6](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [isNeList^#](x1) = [1] x1 + [1] [c_7] = [0] [c_8](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [c_9] = [0] [c_10](x1) = [7] x1 + [0] [c_11](x1) = [7] x1 + [0] [c_12](x1) = [7] x1 + [0] [a^#] = [0] [c_13](x1) = [7] x1 + [0] [e^#] = [0] [c_14](x1) = [7] x1 + [0] [i^#] = [0] [c_15](x1) = [7] x1 + [0] [o^#] = [0] [c_16](x1) = [7] x1 + [0] [u^#] = [0] [U31^#](x1) = [7] x1 + [0] [c_17] = [0] [U41^#](x1, x2) = [1] x1 + [1] x2 + [0] [c_18](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U42^#](x1) = [7] x1 + [0] [c_19] = [0] [c_20](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [isQid^#](x1) = [7] x1 + [0] [c_21](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [c_22](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [U51^#](x1, x2) = [6] x1 + [1] x2 + [0] [c_23](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U52^#](x1) = [7] x1 + [0] [c_24] = [0] [U61^#](x1) = [7] x1 + [0] [c_25] = [0] [U71^#](x1, x2) = [7] x1 + [7] x2 + [0] [c_26](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U72^#](x1) = [7] x1 + [0] [isPal^#](x1) = [7] x1 + [0] [c_27] = [0] [c_28](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U81^#](x1) = [7] x1 + [0] [isNePal^#](x1) = [7] x1 + [0] [c_29] = [0] [c_30] = [0] [c_31] = [0] [c_32] = [0] [c_33] = [0] [c_34] = [0] [c_35] = [0] [c_36](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c_37] = [0] [c_38] = [0] [c_39] = [0] [c_40] = [0] [c_41] = [0] [c] = [0] [c_1](x1) = [1] x1 + [1] [c_2](x1) = [1] x1 + [0] [c_3](x1, x2) = [1] x1 + [1] x2 + [0] [c_4](x1, x2) = [1] x1 + [1] x2 + [4] [c_5](x1, x2) = [1] x1 + [1] x2 + [0] [c_6](x1) = [1] x1 + [0] [c_7](x1) = [1] x1 + [1] The following symbols are considered usable {__, nil, U11, U21, U22, isList, activate, U31, U41, U42, isNeList, U51, U52, isQid, a, e, i, o, u, U21^#, isList^#, isNeList^#, U41^#, U51^#} The order satisfies the following ordering constraints: [__(X1, X2)] = [1] X1 + [1] X2 + [7] >= [1] X1 + [1] X2 + [7] = [n____(X1, X2)] [nil()] = [0] >= [0] = [n__nil()] [U11(tt())] = [1] >= [1] = [tt()] [U21(tt(), V2)] = [2] >= [2] = [U22(isList(activate(V2)))] [U22(tt())] = [2] > [1] = [tt()] [isList(V)] = [2] > [1] = [U11(isNeList(activate(V)))] [isList(n__nil())] = [2] > [1] = [tt()] [isList(n____(V1, V2))] = [2] >= [2] = [U21(isList(activate(V1)), activate(V2))] [activate(X)] = [1] X + [0] >= [1] X + [0] = [X] [activate(n__nil())] = [0] >= [0] = [nil()] [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [7] >= [1] X1 + [1] X2 + [7] = [__(X1, X2)] [activate(n__a())] = [0] >= [0] = [a()] [activate(n__e())] = [0] >= [0] = [e()] [activate(n__i())] = [0] >= [0] = [i()] [activate(n__o())] = [0] >= [0] = [o()] [activate(n__u())] = [0] >= [0] = [u()] [U31(tt())] = [1] >= [1] = [tt()] [U41(tt(), V2)] = [1] >= [1] = [U42(isNeList(activate(V2)))] [U42(tt())] = [1] >= [1] = [tt()] [isNeList(V)] = [1] >= [1] = [U31(isQid(activate(V)))] [isNeList(n____(V1, V2))] = [1] >= [1] = [U41(isList(activate(V1)), activate(V2))] [isNeList(n____(V1, V2))] = [1] >= [1] = [U51(isNeList(activate(V1)), activate(V2))] [U51(tt(), V2)] = [1] >= [1] = [U52(isList(activate(V2)))] [U52(tt())] = [1] >= [1] = [tt()] [isQid(n__a())] = [1] >= [1] = [tt()] [isQid(n__e())] = [1] >= [1] = [tt()] [isQid(n__i())] = [1] >= [1] = [tt()] [isQid(n__o())] = [1] >= [1] = [tt()] [isQid(n__u())] = [1] >= [1] = [tt()] [a()] = [0] >= [0] = [n__a()] [e()] = [0] >= [0] = [n__e()] [i()] = [0] >= [0] = [n__i()] [o()] = [0] >= [0] = [n__o()] [u()] = [0] >= [0] = [n__u()] [U21^#(tt(), V2)] = [1] V2 + [2] >= [1] V2 + [2] = [c_1(isList^#(activate(V2)))] [isList^#(V)] = [1] V + [1] >= [1] V + [1] = [c_2(isNeList^#(activate(V)))] [isList^#(n____(V1, V2))] = [1] V2 + [1] V1 + [8] > [1] V2 + [1] V1 + [3] = [c_3(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)))] [isNeList^#(n____(V1, V2))] = [1] V2 + [1] V1 + [8] > [1] V2 + [1] V1 + [7] = [c_4(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)))] [isNeList^#(n____(V1, V2))] = [1] V2 + [1] V1 + [8] > [1] V2 + [1] V1 + [7] = [c_5(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)))] [U41^#(tt(), V2)] = [1] V2 + [1] >= [1] V2 + [1] = [c_6(isNeList^#(activate(V2)))] [U51^#(tt(), V2)] = [1] V2 + [6] > [1] V2 + [2] = [c_7(isList^#(activate(V2)))] We return to the main proof. Consider the set of all dependency pairs : { 1: U21^#(tt(), V2) -> c_1(isList^#(activate(V2))) , 2: isList^#(V) -> c_2(isNeList^#(activate(V))) , 3: isList^#(n____(V1, V2)) -> c_3(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1))) , 4: isNeList^#(n____(V1, V2)) -> c_4(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1))) , 5: isNeList^#(n____(V1, V2)) -> c_5(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1))) , 6: U41^#(tt(), V2) -> c_6(isNeList^#(activate(V2))) , 7: U51^#(tt(), V2) -> c_7(isList^#(activate(V2))) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {3,4,5,7}. These cover all (indirect) predecessors of dependency pairs {1,2,3,4,5,6,7}, their number of application is equally bounded. The dependency pairs are shifted into the weak component. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { U21^#(tt(), V2) -> c_1(isList^#(activate(V2))) , isList^#(V) -> c_2(isNeList^#(activate(V))) , isList^#(n____(V1, V2)) -> c_3(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1))) , isNeList^#(n____(V1, V2)) -> c_4(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1))) , isNeList^#(n____(V1, V2)) -> c_5(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1))) , U41^#(tt(), V2) -> c_6(isNeList^#(activate(V2))) , U51^#(tt(), V2) -> c_7(isList^#(activate(V2))) } Weak Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , U11(tt()) -> tt() , U21(tt(), V2) -> U22(isList(activate(V2))) , U22(tt()) -> tt() , isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U31(tt()) -> tt() , U41(tt(), V2) -> U42(isNeList(activate(V2))) , U42(tt()) -> 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)) , U51(tt(), V2) -> U52(isList(activate(V2))) , U52(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { U21^#(tt(), V2) -> c_1(isList^#(activate(V2))) , isList^#(V) -> c_2(isNeList^#(activate(V))) , isList^#(n____(V1, V2)) -> c_3(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1))) , isNeList^#(n____(V1, V2)) -> c_4(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1))) , isNeList^#(n____(V1, V2)) -> c_5(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1))) , U41^#(tt(), V2) -> c_6(isNeList^#(activate(V2))) , U51^#(tt(), V2) -> c_7(isList^#(activate(V2))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , U11(tt()) -> tt() , U21(tt(), V2) -> U22(isList(activate(V2))) , U22(tt()) -> tt() , isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(X1, X2) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , U31(tt()) -> tt() , U41(tt(), V2) -> U42(isNeList(activate(V2))) , U42(tt()) -> 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)) , U51(tt(), V2) -> U52(isList(activate(V2))) , U52(tt()) -> tt() , isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() , a() -> n__a() , e() -> n__e() , i() -> n__i() , o() -> n__o() , u() -> n__u() } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^1))