YES(O(1),O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). 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)) -> __(activate(X1), activate(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, n____(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^2)) Arguments of following rules are not normal-forms: { __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X } 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^2)). 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)) -> __(activate(X1), activate(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, n____(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^2)) 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(__^#(activate(X1), activate(X2)), activate^#(X1), activate^#(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_38() , e^#() -> c_39() , i^#() -> c_40() , o^#() -> c_41() , u^#() -> c_42() , 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)) , isNePal^#(n____(I, n____(P, I))) -> c_37(U71^#(isQid(activate(I)), activate(P)), isQid^#(activate(I)), activate^#(I), activate^#(P)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). 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(__^#(activate(X1), activate(X2)), activate^#(X1), activate^#(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_38() , e^#() -> c_39() , i^#() -> c_40() , o^#() -> c_41() , u^#() -> c_42() , 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)) , isNePal^#(n____(I, n____(P, I))) -> c_37(U71^#(isQid(activate(I)), activate(P)), isQid^#(activate(I)), activate^#(I), activate^#(P)) } 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)) -> __(activate(X1), activate(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, n____(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^2)) 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,42}. 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(__^#(activate(X1), activate(X2)), activate^#(X1), activate^#(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_38() , 21: e^#() -> c_39() , 22: i^#() -> c_40() , 23: o^#() -> c_41() , 24: u^#() -> c_42() , 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)) , 42: isNePal^#(n____(I, n____(P, I))) -> c_37(U71^#(isQid(activate(I)), activate(P)), isQid^#(activate(I)), activate^#(I), activate^#(P)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). 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(__^#(activate(X1), activate(X2)), activate^#(X1), activate^#(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)) , isNePal^#(n____(I, n____(P, I))) -> c_37(U71^#(isQid(activate(I)), activate(P)), isQid^#(activate(I)), activate^#(I), 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() , a^#() -> c_38() , e^#() -> c_39() , i^#() -> c_40() , o^#() -> c_41() , u^#() -> c_42() , 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)) -> __(activate(X1), activate(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, n____(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^2)) We estimate the number of application of {4,6,7,8,9,10} by applications of Pre({4,6,7,8,9,10}) = {1,2,3,5,11,12,13,14,15,16,17,18,19}. 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(__^#(activate(X1), activate(X2)), activate^#(X1), activate^#(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: isNePal^#(n____(I, n____(P, I))) -> c_37(U71^#(isQid(activate(I)), activate(P)), isQid^#(activate(I)), activate^#(I), activate^#(P)) , 20: __^#(X1, X2) -> c_1() , 21: nil^#() -> c_2() , 22: U11^#(tt()) -> c_3() , 23: U22^#(tt()) -> c_5() , 24: isList^#(n__nil()) -> c_7() , 25: activate^#(X) -> c_9() , 26: a^#() -> c_38() , 27: e^#() -> c_39() , 28: i^#() -> c_40() , 29: o^#() -> c_41() , 30: u^#() -> c_42() , 31: U31^#(tt()) -> c_17() , 32: U42^#(tt()) -> c_19() , 33: isQid^#(n__a()) -> c_31() , 34: isQid^#(n__e()) -> c_32() , 35: isQid^#(n__i()) -> c_33() , 36: isQid^#(n__o()) -> c_34() , 37: isQid^#(n__u()) -> c_35() , 38: U52^#(tt()) -> c_24() , 39: U61^#(tt()) -> c_25() , 40: U72^#(tt()) -> c_27() , 41: isPal^#(n__nil()) -> c_29() , 42: U81^#(tt()) -> c_30() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). 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____(X1, X2)) -> c_11(__^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , 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)) , isNePal^#(n____(I, n____(P, I))) -> c_37(U71^#(isQid(activate(I)), activate(P)), isQid^#(activate(I)), activate^#(I), 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__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_38() , e^#() -> c_39() , i^#() -> c_40() , o^#() -> c_41() , u^#() -> c_42() , 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)) -> __(activate(X1), activate(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, n____(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^2)) 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__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_38() , e^#() -> c_39() , i^#() -> c_40() , o^#() -> c_41() , u^#() -> c_42() , 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() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). 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____(X1, X2)) -> c_11(__^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , 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)) , isNePal^#(n____(I, n____(P, I))) -> c_37(U71^#(isQid(activate(I)), activate(P)), isQid^#(activate(I)), activate^#(I), activate^#(P)) } 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)) -> __(activate(X1), activate(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, n____(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^2)) 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)) , activate^#(n____(X1, X2)) -> c_11(__^#(activate(X1), activate(X2)), activate^#(X1), activate^#(X2)) , isNeList^#(V) -> c_20(U31^#(isQid(activate(V))), isQid^#(activate(V)), activate^#(V)) , 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)) , isNePal^#(n____(I, n____(P, I))) -> c_37(U71^#(isQid(activate(I)), activate(P)), isQid^#(activate(I)), activate^#(I), activate^#(P)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { U21^#(tt(), V2) -> c_1(isList^#(activate(V2)), activate^#(V2)) , isList^#(V) -> c_2(isNeList^#(activate(V)), activate^#(V)) , isList^#(n____(V1, V2)) -> c_3(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , activate^#(n____(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) , isNeList^#(V) -> c_5(activate^#(V)) , isNeList^#(n____(V1, V2)) -> c_6(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_7(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , U41^#(tt(), V2) -> c_8(isNeList^#(activate(V2)), activate^#(V2)) , U51^#(tt(), V2) -> c_9(isList^#(activate(V2)), activate^#(V2)) , U71^#(tt(), P) -> c_10(isPal^#(activate(P)), activate^#(P)) , isPal^#(V) -> c_11(isNePal^#(activate(V)), activate^#(V)) , isNePal^#(V) -> c_12(activate^#(V)) , isNePal^#(n____(I, n____(P, I))) -> c_13(U71^#(isQid(activate(I)), activate(P)), activate^#(I), activate^#(P)) } 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)) -> __(activate(X1), activate(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, n____(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^2)) 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)) -> __(activate(X1), activate(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^2)). Strict DPs: { U21^#(tt(), V2) -> c_1(isList^#(activate(V2)), activate^#(V2)) , isList^#(V) -> c_2(isNeList^#(activate(V)), activate^#(V)) , isList^#(n____(V1, V2)) -> c_3(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , activate^#(n____(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) , isNeList^#(V) -> c_5(activate^#(V)) , isNeList^#(n____(V1, V2)) -> c_6(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_7(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , U41^#(tt(), V2) -> c_8(isNeList^#(activate(V2)), activate^#(V2)) , U51^#(tt(), V2) -> c_9(isList^#(activate(V2)), activate^#(V2)) , U71^#(tt(), P) -> c_10(isPal^#(activate(P)), activate^#(P)) , isPal^#(V) -> c_11(isNePal^#(activate(V)), activate^#(V)) , isNePal^#(V) -> c_12(activate^#(V)) , isNePal^#(n____(I, n____(P, I))) -> c_13(U71^#(isQid(activate(I)), activate(P)), activate^#(I), activate^#(P)) } 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)) -> __(activate(X1), activate(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^2)) We decompose the input problem according to the dependency graph into the upper component { U21^#(tt(), V2) -> c_1(isList^#(activate(V2)), activate^#(V2)) , isList^#(V) -> c_2(isNeList^#(activate(V)), activate^#(V)) , isList^#(n____(V1, V2)) -> c_3(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_6(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_7(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , U41^#(tt(), V2) -> c_8(isNeList^#(activate(V2)), activate^#(V2)) , U51^#(tt(), V2) -> c_9(isList^#(activate(V2)), activate^#(V2)) , U71^#(tt(), P) -> c_10(isPal^#(activate(P)), activate^#(P)) , isPal^#(V) -> c_11(isNePal^#(activate(V)), activate^#(V)) , isNePal^#(n____(I, n____(P, I))) -> c_13(U71^#(isQid(activate(I)), activate(P)), activate^#(I), activate^#(P)) } and lower component { activate^#(n____(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) , isNeList^#(V) -> c_5(activate^#(V)) , isNePal^#(V) -> c_12(activate^#(V)) } Further, following extension rules are added to the lower component. { U21^#(tt(), V2) -> isList^#(activate(V2)) , U21^#(tt(), V2) -> activate^#(V2) , isList^#(V) -> activate^#(V) , isList^#(V) -> isNeList^#(activate(V)) , isList^#(n____(V1, V2)) -> U21^#(isList(activate(V1)), activate(V2)) , isList^#(n____(V1, V2)) -> isList^#(activate(V1)) , isList^#(n____(V1, V2)) -> activate^#(V1) , isList^#(n____(V1, V2)) -> activate^#(V2) , isNeList^#(n____(V1, V2)) -> isList^#(activate(V1)) , isNeList^#(n____(V1, V2)) -> activate^#(V1) , isNeList^#(n____(V1, V2)) -> activate^#(V2) , isNeList^#(n____(V1, V2)) -> isNeList^#(activate(V1)) , isNeList^#(n____(V1, V2)) -> U41^#(isList(activate(V1)), activate(V2)) , isNeList^#(n____(V1, V2)) -> U51^#(isNeList(activate(V1)), activate(V2)) , U41^#(tt(), V2) -> activate^#(V2) , U41^#(tt(), V2) -> isNeList^#(activate(V2)) , U51^#(tt(), V2) -> isList^#(activate(V2)) , U51^#(tt(), V2) -> activate^#(V2) , U71^#(tt(), P) -> activate^#(P) , U71^#(tt(), P) -> isPal^#(activate(P)) , isPal^#(V) -> activate^#(V) , isPal^#(V) -> isNePal^#(activate(V)) , isNePal^#(n____(I, n____(P, I))) -> activate^#(I) , isNePal^#(n____(I, n____(P, I))) -> activate^#(P) , isNePal^#(n____(I, n____(P, I))) -> U71^#(isQid(activate(I)), activate(P)) } TcT solves the upper component with certificate YES(O(1),O(n^1)). Sub-proof: ---------- 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)), activate^#(V2)) , isList^#(V) -> c_2(isNeList^#(activate(V)), activate^#(V)) , isList^#(n____(V1, V2)) -> c_3(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_6(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_7(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , U41^#(tt(), V2) -> c_8(isNeList^#(activate(V2)), activate^#(V2)) , U51^#(tt(), V2) -> c_9(isList^#(activate(V2)), activate^#(V2)) , U71^#(tt(), P) -> c_10(isPal^#(activate(P)), activate^#(P)) , isPal^#(V) -> c_11(isNePal^#(activate(V)), activate^#(V)) , isNePal^#(n____(I, n____(P, I))) -> c_13(U71^#(isQid(activate(I)), activate(P)), activate^#(I), activate^#(P)) } 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)) -> __(activate(X1), activate(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)), activate^#(V1), activate^#(V2)) , 4: isNeList^#(n____(V1, V2)) -> c_6(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , 5: isNeList^#(n____(V1, V2)) -> c_7(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) } Trs: { U11(tt()) -> tt() , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , 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)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2}, Uargs(c_6) = {1, 2}, Uargs(c_7) = {1, 2}, Uargs(c_8) = {1}, Uargs(c_9) = {1}, Uargs(c_10) = {1}, Uargs(c_11) = {1}, Uargs(c_13) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [__](x1, x2) = [1] x1 + [1] x2 + [4] [nil] = [0] [U11](x1) = [4] [tt] = [0] [U21](x1, x2) = [0] [U22](x1) = [0] [isList](x1) = [4] [activate](x1) = [1] x1 + [0] [U31](x1) = [0] [U41](x1, x2) = [0] [U42](x1) = [0] [isNeList](x1) = [1] [U51](x1, x2) = [0] [U52](x1) = [0] [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 + [4] [isQid](x1) = [0] [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) = [2] x2 + [0] [c_4](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U22^#](x1) = [7] x1 + [0] [isList^#](x1) = [2] x1 + [0] [activate^#](x1) = [0] [c_5] = [0] [c_6](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [isNeList^#](x1) = [2] x1 + [0] [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, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [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) = [2] 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) = [3] x1 + [2] 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) = [0] [c_26](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U72^#](x1) = [7] x1 + [0] [isPal^#](x1) = [0] [c_27] = [0] [c_28](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U81^#](x1) = [7] x1 + [0] [isNePal^#](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](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [c_38] = [0] [c_39] = [0] [c_40] = [0] [c_41] = [0] [c_42] = [0] [c] = [0] [c_1](x1, x2) = [1] x1 + [0] [c_2](x1, x2) = [1] x1 + [0] [c_3](x1, x2, x3, x4) = [1] x1 + [1] x2 + [7] [c_4](x1, x2) = [7] x1 + [7] x2 + [0] [c_5](x1) = [7] x1 + [0] [c_6](x1, x2, x3, x4) = [1] x1 + [1] x2 + [7] [c_7](x1, x2, x3, x4) = [1] x1 + [1] x2 + [3] [c_8](x1, x2) = [1] x1 + [0] [c_9](x1, x2) = [1] x1 + [0] [c_10](x1, x2) = [2] x1 + [0] [c_11](x1, x2) = [4] x1 + [0] [c_12](x1) = [7] x1 + [0] [c_13](x1, x2, x3) = [2] x1 + [0] 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^#, U71^#, isPal^#, isNePal^#} The order satisfies the following ordering constraints: [__(X1, X2)] = [1] X1 + [1] X2 + [4] >= [1] X1 + [1] X2 + [4] = [n____(X1, X2)] [nil()] = [0] >= [0] = [n__nil()] [U11(tt())] = [4] > [0] = [tt()] [U21(tt(), V2)] = [0] >= [0] = [U22(isList(activate(V2)))] [U22(tt())] = [0] >= [0] = [tt()] [isList(V)] = [4] >= [4] = [U11(isNeList(activate(V)))] [isList(n__nil())] = [4] > [0] = [tt()] [isList(n____(V1, V2))] = [4] > [0] = [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 + [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())] = [0] >= [0] = [i()] [activate(n__o())] = [0] >= [0] = [o()] [activate(n__u())] = [0] >= [0] = [u()] [U31(tt())] = [0] >= [0] = [tt()] [U41(tt(), V2)] = [0] >= [0] = [U42(isNeList(activate(V2)))] [U42(tt())] = [0] >= [0] = [tt()] [isNeList(V)] = [1] > [0] = [U31(isQid(activate(V)))] [isNeList(n____(V1, V2))] = [1] > [0] = [U41(isList(activate(V1)), activate(V2))] [isNeList(n____(V1, V2))] = [1] > [0] = [U51(isNeList(activate(V1)), activate(V2))] [U51(tt(), V2)] = [0] >= [0] = [U52(isList(activate(V2)))] [U52(tt())] = [0] >= [0] = [tt()] [isQid(n__a())] = [0] >= [0] = [tt()] [isQid(n__e())] = [0] >= [0] = [tt()] [isQid(n__i())] = [0] >= [0] = [tt()] [isQid(n__o())] = [0] >= [0] = [tt()] [isQid(n__u())] = [0] >= [0] = [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)] = [2] V2 + [0] >= [2] V2 + [0] = [c_1(isList^#(activate(V2)), activate^#(V2))] [isList^#(V)] = [2] V + [0] >= [2] V + [0] = [c_2(isNeList^#(activate(V)), activate^#(V))] [isList^#(n____(V1, V2))] = [2] V2 + [2] V1 + [8] > [2] V2 + [2] V1 + [7] = [c_3(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2))] [isNeList^#(n____(V1, V2))] = [2] V2 + [2] V1 + [8] > [2] V2 + [2] V1 + [7] = [c_6(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2))] [isNeList^#(n____(V1, V2))] = [2] V2 + [2] V1 + [8] > [2] V2 + [2] V1 + [6] = [c_7(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2))] [U41^#(tt(), V2)] = [2] V2 + [0] >= [2] V2 + [0] = [c_8(isNeList^#(activate(V2)), activate^#(V2))] [U51^#(tt(), V2)] = [2] V2 + [0] >= [2] V2 + [0] = [c_9(isList^#(activate(V2)), activate^#(V2))] [U71^#(tt(), P)] = [0] >= [0] = [c_10(isPal^#(activate(P)), activate^#(P))] [isPal^#(V)] = [0] >= [0] = [c_11(isNePal^#(activate(V)), activate^#(V))] [isNePal^#(n____(I, n____(P, I)))] = [0] >= [0] = [c_13(U71^#(isQid(activate(I)), activate(P)), activate^#(I), activate^#(P))] We return to the main proof. Consider the set of all dependency pairs : { 1: U21^#(tt(), V2) -> c_1(isList^#(activate(V2)), activate^#(V2)) , 2: isList^#(V) -> c_2(isNeList^#(activate(V)), activate^#(V)) , 3: isList^#(n____(V1, V2)) -> c_3(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , 4: isNeList^#(n____(V1, V2)) -> c_6(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , 5: isNeList^#(n____(V1, V2)) -> c_7(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , 6: U41^#(tt(), V2) -> c_8(isNeList^#(activate(V2)), activate^#(V2)) , 7: U51^#(tt(), V2) -> c_9(isList^#(activate(V2)), activate^#(V2)) , 8: U71^#(tt(), P) -> c_10(isPal^#(activate(P)), activate^#(P)) , 9: isPal^#(V) -> c_11(isNePal^#(activate(V)), activate^#(V)) , 10: isNePal^#(n____(I, n____(P, I))) -> c_13(U71^#(isQid(activate(I)), activate(P)), activate^#(I), activate^#(P)) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {3,4,5}. 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(n^1)). Strict DPs: { U71^#(tt(), P) -> c_10(isPal^#(activate(P)), activate^#(P)) , isPal^#(V) -> c_11(isNePal^#(activate(V)), activate^#(V)) , isNePal^#(n____(I, n____(P, I))) -> c_13(U71^#(isQid(activate(I)), activate(P)), activate^#(I), activate^#(P)) } Weak DPs: { U21^#(tt(), V2) -> c_1(isList^#(activate(V2)), activate^#(V2)) , isList^#(V) -> c_2(isNeList^#(activate(V)), activate^#(V)) , isList^#(n____(V1, V2)) -> c_3(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_6(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_7(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , U41^#(tt(), V2) -> c_8(isNeList^#(activate(V2)), activate^#(V2)) , U51^#(tt(), V2) -> c_9(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)) -> __(activate(X1), activate(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)) 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)), activate^#(V2)) , isList^#(V) -> c_2(isNeList^#(activate(V)), activate^#(V)) , isList^#(n____(V1, V2)) -> c_3(U21^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_6(U41^#(isList(activate(V1)), activate(V2)), isList^#(activate(V1)), activate^#(V1), activate^#(V2)) , isNeList^#(n____(V1, V2)) -> c_7(U51^#(isNeList(activate(V1)), activate(V2)), isNeList^#(activate(V1)), activate^#(V1), activate^#(V2)) , U41^#(tt(), V2) -> c_8(isNeList^#(activate(V2)), activate^#(V2)) , U51^#(tt(), V2) -> c_9(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: { U71^#(tt(), P) -> c_10(isPal^#(activate(P)), activate^#(P)) , isPal^#(V) -> c_11(isNePal^#(activate(V)), activate^#(V)) , isNePal^#(n____(I, n____(P, I))) -> c_13(U71^#(isQid(activate(I)), activate(P)), activate^#(I), activate^#(P)) } 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)) -> __(activate(X1), activate(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)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { U71^#(tt(), P) -> c_10(isPal^#(activate(P)), activate^#(P)) , isPal^#(V) -> c_11(isNePal^#(activate(V)), activate^#(V)) , isNePal^#(n____(I, n____(P, I))) -> c_13(U71^#(isQid(activate(I)), activate(P)), activate^#(I), activate^#(P)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { U71^#(tt(), P) -> c_1(isPal^#(activate(P))) , isPal^#(V) -> c_2(isNePal^#(activate(V))) , isNePal^#(n____(I, n____(P, I))) -> c_3(U71^#(isQid(activate(I)), activate(P))) } 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)) -> __(activate(X1), activate(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 replace rewrite rules by usable rules: Weak Usable Rules: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , 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: { U71^#(tt(), P) -> c_1(isPal^#(activate(P))) , isPal^#(V) -> c_2(isNePal^#(activate(V))) , isNePal^#(n____(I, n____(P, I))) -> c_3(U71^#(isQid(activate(I)), activate(P))) } Weak Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , 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: isNePal^#(n____(I, n____(P, I))) -> c_3(U71^#(isQid(activate(I)), activate(P))) } Trs: { isQid(n__a()) -> tt() , isQid(n__e()) -> tt() , isQid(n__i()) -> tt() , isQid(n__o()) -> tt() , isQid(n__u()) -> tt() } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [__](x1, x2) = [1] x1 + [1] x2 + [1] [nil] = [0] [U11](x1) = [7] x1 + [0] [tt] = [0] [U21](x1, x2) = [7] x1 + [7] x2 + [0] [U22](x1) = [7] x1 + [0] [isList](x1) = [7] x1 + [0] [activate](x1) = [1] x1 + [0] [U31](x1) = [7] x1 + [0] [U41](x1, x2) = [7] x1 + [7] x2 + [0] [U42](x1) = [7] x1 + [0] [isNeList](x1) = [7] x1 + [0] [U51](x1, x2) = [7] x1 + [7] x2 + [0] [U52](x1) = [7] x1 + [0] [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 + [1] [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) = [7] x1 + [7] x2 + [0] [c_4](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U22^#](x1) = [7] x1 + [0] [isList^#](x1) = [7] x1 + [0] [activate^#](x1) = [7] x1 + [0] [c_5] = [0] [c_6](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [isNeList^#](x1) = [7] x1 + [0] [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, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [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) = [7] x1 + [7] 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) = [7] x1 + [7] 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 + [4] x2 + [0] [c_26](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U72^#](x1) = [7] x1 + [0] [isPal^#](x1) = [4] x1 + [0] [c_27] = [0] [c_28](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U81^#](x1) = [7] x1 + [0] [isNePal^#](x1) = [4] 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](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [c_38] = [0] [c_39] = [0] [c_40] = [0] [c_41] = [0] [c_42] = [0] [c] = [0] [c_1](x1, x2) = [7] x1 + [7] x2 + [0] [c_2](x1, x2) = [7] x1 + [7] x2 + [0] [c_3](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [c_4](x1, x2) = [7] x1 + [7] x2 + [0] [c_5](x1) = [7] x1 + [0] [c_6](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [c_7](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [c_8](x1, x2) = [7] x1 + [7] x2 + [0] [c_9](x1, x2) = [7] x1 + [7] x2 + [0] [c_10](x1, x2) = [7] x1 + [7] x2 + [0] [c_11](x1, x2) = [7] x1 + [7] x2 + [0] [c_12](x1) = [7] x1 + [0] [c_13](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [c] = [0] [c_1](x1) = [1] x1 + [0] [c_2](x1) = [1] x1 + [0] [c_3](x1) = [1] x1 + [0] The following symbols are considered usable {__, nil, activate, isQid, a, e, i, o, u, U71^#, isPal^#, isNePal^#} The order satisfies the following ordering constraints: [__(X1, X2)] = [1] X1 + [1] X2 + [1] >= [1] X1 + [1] X2 + [1] = [n____(X1, X2)] [nil()] = [0] >= [0] = [n__nil()] [activate(X)] = [1] X + [0] >= [1] X + [0] = [X] [activate(n__nil())] = [0] >= [0] = [nil()] [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__o())] = [0] >= [0] = [o()] [activate(n__u())] = [0] >= [0] = [u()] [isQid(n__a())] = [1] > [0] = [tt()] [isQid(n__e())] = [1] > [0] = [tt()] [isQid(n__i())] = [1] > [0] = [tt()] [isQid(n__o())] = [1] > [0] = [tt()] [isQid(n__u())] = [1] > [0] = [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()] [U71^#(tt(), P)] = [4] P + [0] >= [4] P + [0] = [c_1(isPal^#(activate(P)))] [isPal^#(V)] = [4] V + [0] >= [4] V + [0] = [c_2(isNePal^#(activate(V)))] [isNePal^#(n____(I, n____(P, I)))] = [4] P + [8] I + [8] > [4] P + [7] = [c_3(U71^#(isQid(activate(I)), activate(P)))] We return to the main proof. Consider the set of all dependency pairs : { 1: U71^#(tt(), P) -> c_1(isPal^#(activate(P))) , 2: isPal^#(V) -> c_2(isNePal^#(activate(V))) , 3: isNePal^#(n____(I, n____(P, I))) -> c_3(U71^#(isQid(activate(I)), activate(P))) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {3}. These cover all (indirect) predecessors of dependency pairs {1,2,3}, 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: { U71^#(tt(), P) -> c_1(isPal^#(activate(P))) , isPal^#(V) -> c_2(isNePal^#(activate(V))) , isNePal^#(n____(I, n____(P, I))) -> c_3(U71^#(isQid(activate(I)), activate(P))) } Weak Trs: { __(X1, X2) -> n____(X1, X2) , nil() -> n__nil() , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , 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. { U71^#(tt(), P) -> c_1(isPal^#(activate(P))) , isPal^#(V) -> c_2(isNePal^#(activate(V))) , isNePal^#(n____(I, n____(P, I))) -> c_3(U71^#(isQid(activate(I)), activate(P))) } 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() , activate(X) -> X , activate(n__nil()) -> nil() , activate(n____(X1, X2)) -> __(activate(X1), activate(X2)) , activate(n__a()) -> a() , activate(n__e()) -> e() , activate(n__i()) -> i() , activate(n__o()) -> o() , activate(n__u()) -> u() , 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 We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { activate^#(n____(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) , isNeList^#(V) -> c_5(activate^#(V)) , isNePal^#(V) -> c_12(activate^#(V)) } Weak DPs: { U21^#(tt(), V2) -> isList^#(activate(V2)) , U21^#(tt(), V2) -> activate^#(V2) , isList^#(V) -> activate^#(V) , isList^#(V) -> isNeList^#(activate(V)) , isList^#(n____(V1, V2)) -> U21^#(isList(activate(V1)), activate(V2)) , isList^#(n____(V1, V2)) -> isList^#(activate(V1)) , isList^#(n____(V1, V2)) -> activate^#(V1) , isList^#(n____(V1, V2)) -> activate^#(V2) , isNeList^#(n____(V1, V2)) -> isList^#(activate(V1)) , isNeList^#(n____(V1, V2)) -> activate^#(V1) , isNeList^#(n____(V1, V2)) -> activate^#(V2) , isNeList^#(n____(V1, V2)) -> isNeList^#(activate(V1)) , isNeList^#(n____(V1, V2)) -> U41^#(isList(activate(V1)), activate(V2)) , isNeList^#(n____(V1, V2)) -> U51^#(isNeList(activate(V1)), activate(V2)) , U41^#(tt(), V2) -> activate^#(V2) , U41^#(tt(), V2) -> isNeList^#(activate(V2)) , U51^#(tt(), V2) -> isList^#(activate(V2)) , U51^#(tt(), V2) -> activate^#(V2) , U71^#(tt(), P) -> activate^#(P) , U71^#(tt(), P) -> isPal^#(activate(P)) , isPal^#(V) -> activate^#(V) , isPal^#(V) -> isNePal^#(activate(V)) , isNePal^#(n____(I, n____(P, I))) -> activate^#(I) , isNePal^#(n____(I, n____(P, I))) -> activate^#(P) , isNePal^#(n____(I, n____(P, I))) -> U71^#(isQid(activate(I)), activate(P)) } 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)) -> __(activate(X1), activate(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: { 1: activate^#(n____(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) , 8: isList^#(n____(V1, V2)) -> U21^#(isList(activate(V1)), activate(V2)) , 9: isList^#(n____(V1, V2)) -> isList^#(activate(V1)) , 10: isList^#(n____(V1, V2)) -> activate^#(V1) , 11: isList^#(n____(V1, V2)) -> activate^#(V2) , 12: isNeList^#(n____(V1, V2)) -> isList^#(activate(V1)) , 13: isNeList^#(n____(V1, V2)) -> activate^#(V1) , 14: isNeList^#(n____(V1, V2)) -> activate^#(V2) , 15: isNeList^#(n____(V1, V2)) -> isNeList^#(activate(V1)) , 16: isNeList^#(n____(V1, V2)) -> U41^#(isList(activate(V1)), activate(V2)) , 17: isNeList^#(n____(V1, V2)) -> U51^#(isNeList(activate(V1)), activate(V2)) , 26: isNePal^#(n____(I, n____(P, I))) -> activate^#(I) , 27: isNePal^#(n____(I, n____(P, I))) -> activate^#(P) , 28: isNePal^#(n____(I, n____(P, I))) -> U71^#(isQid(activate(I)), activate(P)) } Trs: { isList(V) -> U11(isNeList(activate(V))) , isList(n__nil()) -> tt() , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) , 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)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}, Uargs(c_12) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [__](x1, x2) = [1] x1 + [1] x2 + [1] [nil] = [0] [U11](x1) = [0] [tt] = [0] [U21](x1, x2) = [0] [U22](x1) = [0] [isList](x1) = [7] x1 + [1] [activate](x1) = [1] x1 + [0] [U31](x1) = [0] [U41](x1, x2) = [0] [U42](x1) = [0] [isNeList](x1) = [4] x1 + [4] [U51](x1, x2) = [4] x2 + [0] [U52](x1) = [0] [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 + [1] [isQid](x1) = [0] [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) = [2] x2 + [0] [c_4](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U22^#](x1) = [7] x1 + [0] [isList^#](x1) = [2] x1 + [0] [activate^#](x1) = [1] x1 + [0] [c_5] = [0] [c_6](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [isNeList^#](x1) = [2] x1 + [0] [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, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [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) = [2] 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) = [2] 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) = [4] x2 + [0] [c_26](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U72^#](x1) = [7] x1 + [0] [isPal^#](x1) = [4] x1 + [0] [c_27] = [0] [c_28](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] [U81^#](x1) = [7] x1 + [0] [isNePal^#](x1) = [4] 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](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [c_38] = [0] [c_39] = [0] [c_40] = [0] [c_41] = [0] [c_42] = [0] [c] = [0] [c_1](x1, x2) = [7] x1 + [7] x2 + [0] [c_2](x1, x2) = [7] x1 + [7] x2 + [0] [c_3](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [c_4](x1, x2) = [1] x1 + [1] x2 + [0] [c_5](x1) = [2] x1 + [0] [c_6](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [c_7](x1, x2, x3, x4) = [7] x1 + [7] x2 + [7] x3 + [7] x4 + [0] [c_8](x1, x2) = [7] x1 + [7] x2 + [0] [c_9](x1, x2) = [7] x1 + [7] x2 + [0] [c_10](x1, x2) = [7] x1 + [7] x2 + [0] [c_11](x1, x2) = [7] x1 + [7] x2 + [0] [c_12](x1) = [4] x1 + [0] [c_13](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0] 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^#, activate^#, isNeList^#, U41^#, U51^#, U71^#, isPal^#, isNePal^#} The order satisfies the following ordering constraints: [__(X1, X2)] = [1] X1 + [1] X2 + [1] >= [1] X1 + [1] X2 + [1] = [n____(X1, X2)] [nil()] = [0] >= [0] = [n__nil()] [U11(tt())] = [0] >= [0] = [tt()] [U21(tt(), V2)] = [0] >= [0] = [U22(isList(activate(V2)))] [U22(tt())] = [0] >= [0] = [tt()] [isList(V)] = [7] V + [1] > [0] = [U11(isNeList(activate(V)))] [isList(n__nil())] = [1] > [0] = [tt()] [isList(n____(V1, V2))] = [7] V2 + [7] V1 + [8] > [0] = [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 + [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__o())] = [0] >= [0] = [o()] [activate(n__u())] = [0] >= [0] = [u()] [U31(tt())] = [0] >= [0] = [tt()] [U41(tt(), V2)] = [0] >= [0] = [U42(isNeList(activate(V2)))] [U42(tt())] = [0] >= [0] = [tt()] [isNeList(V)] = [4] V + [4] > [0] = [U31(isQid(activate(V)))] [isNeList(n____(V1, V2))] = [4] V2 + [4] V1 + [8] > [0] = [U41(isList(activate(V1)), activate(V2))] [isNeList(n____(V1, V2))] = [4] V2 + [4] V1 + [8] > [4] V2 + [0] = [U51(isNeList(activate(V1)), activate(V2))] [U51(tt(), V2)] = [4] V2 + [0] >= [0] = [U52(isList(activate(V2)))] [U52(tt())] = [0] >= [0] = [tt()] [isQid(n__a())] = [0] >= [0] = [tt()] [isQid(n__e())] = [0] >= [0] = [tt()] [isQid(n__i())] = [0] >= [0] = [tt()] [isQid(n__o())] = [0] >= [0] = [tt()] [isQid(n__u())] = [0] >= [0] = [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)] = [2] V2 + [0] >= [2] V2 + [0] = [isList^#(activate(V2))] [U21^#(tt(), V2)] = [2] V2 + [0] >= [1] V2 + [0] = [activate^#(V2)] [isList^#(V)] = [2] V + [0] >= [1] V + [0] = [activate^#(V)] [isList^#(V)] = [2] V + [0] >= [2] V + [0] = [isNeList^#(activate(V))] [isList^#(n____(V1, V2))] = [2] V2 + [2] V1 + [2] > [2] V2 + [0] = [U21^#(isList(activate(V1)), activate(V2))] [isList^#(n____(V1, V2))] = [2] V2 + [2] V1 + [2] > [2] V1 + [0] = [isList^#(activate(V1))] [isList^#(n____(V1, V2))] = [2] V2 + [2] V1 + [2] > [1] V1 + [0] = [activate^#(V1)] [isList^#(n____(V1, V2))] = [2] V2 + [2] V1 + [2] > [1] V2 + [0] = [activate^#(V2)] [activate^#(n____(X1, X2))] = [1] X1 + [1] X2 + [1] > [1] X1 + [1] X2 + [0] = [c_4(activate^#(X1), activate^#(X2))] [isNeList^#(V)] = [2] V + [0] >= [2] V + [0] = [c_5(activate^#(V))] [isNeList^#(n____(V1, V2))] = [2] V2 + [2] V1 + [2] > [2] V1 + [0] = [isList^#(activate(V1))] [isNeList^#(n____(V1, V2))] = [2] V2 + [2] V1 + [2] > [1] V1 + [0] = [activate^#(V1)] [isNeList^#(n____(V1, V2))] = [2] V2 + [2] V1 + [2] > [1] V2 + [0] = [activate^#(V2)] [isNeList^#(n____(V1, V2))] = [2] V2 + [2] V1 + [2] > [2] V1 + [0] = [isNeList^#(activate(V1))] [isNeList^#(n____(V1, V2))] = [2] V2 + [2] V1 + [2] > [2] V2 + [0] = [U41^#(isList(activate(V1)), activate(V2))] [isNeList^#(n____(V1, V2))] = [2] V2 + [2] V1 + [2] > [2] V2 + [0] = [U51^#(isNeList(activate(V1)), activate(V2))] [U41^#(tt(), V2)] = [2] V2 + [0] >= [1] V2 + [0] = [activate^#(V2)] [U41^#(tt(), V2)] = [2] V2 + [0] >= [2] V2 + [0] = [isNeList^#(activate(V2))] [U51^#(tt(), V2)] = [2] V2 + [0] >= [2] V2 + [0] = [isList^#(activate(V2))] [U51^#(tt(), V2)] = [2] V2 + [0] >= [1] V2 + [0] = [activate^#(V2)] [U71^#(tt(), P)] = [4] P + [0] >= [1] P + [0] = [activate^#(P)] [U71^#(tt(), P)] = [4] P + [0] >= [4] P + [0] = [isPal^#(activate(P))] [isPal^#(V)] = [4] V + [0] >= [1] V + [0] = [activate^#(V)] [isPal^#(V)] = [4] V + [0] >= [4] V + [0] = [isNePal^#(activate(V))] [isNePal^#(V)] = [4] V + [0] >= [4] V + [0] = [c_12(activate^#(V))] [isNePal^#(n____(I, n____(P, I)))] = [4] P + [8] I + [8] > [1] I + [0] = [activate^#(I)] [isNePal^#(n____(I, n____(P, I)))] = [4] P + [8] I + [8] > [1] P + [0] = [activate^#(P)] [isNePal^#(n____(I, n____(P, I)))] = [4] P + [8] I + [8] > [4] P + [0] = [U71^#(isQid(activate(I)), activate(P))] We return to the main proof. Consider the set of all dependency pairs : { 1: activate^#(n____(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) , 2: isNeList^#(V) -> c_5(activate^#(V)) , 3: isNePal^#(V) -> c_12(activate^#(V)) , 4: U21^#(tt(), V2) -> isList^#(activate(V2)) , 5: U21^#(tt(), V2) -> activate^#(V2) , 6: isList^#(V) -> activate^#(V) , 7: isList^#(V) -> isNeList^#(activate(V)) , 8: isList^#(n____(V1, V2)) -> U21^#(isList(activate(V1)), activate(V2)) , 9: isList^#(n____(V1, V2)) -> isList^#(activate(V1)) , 10: isList^#(n____(V1, V2)) -> activate^#(V1) , 11: isList^#(n____(V1, V2)) -> activate^#(V2) , 12: isNeList^#(n____(V1, V2)) -> isList^#(activate(V1)) , 13: isNeList^#(n____(V1, V2)) -> activate^#(V1) , 14: isNeList^#(n____(V1, V2)) -> activate^#(V2) , 15: isNeList^#(n____(V1, V2)) -> isNeList^#(activate(V1)) , 16: isNeList^#(n____(V1, V2)) -> U41^#(isList(activate(V1)), activate(V2)) , 17: isNeList^#(n____(V1, V2)) -> U51^#(isNeList(activate(V1)), activate(V2)) , 18: U41^#(tt(), V2) -> activate^#(V2) , 19: U41^#(tt(), V2) -> isNeList^#(activate(V2)) , 20: U51^#(tt(), V2) -> isList^#(activate(V2)) , 21: U51^#(tt(), V2) -> activate^#(V2) , 22: U71^#(tt(), P) -> activate^#(P) , 23: U71^#(tt(), P) -> isPal^#(activate(P)) , 24: isPal^#(V) -> activate^#(V) , 25: isPal^#(V) -> isNePal^#(activate(V)) , 26: isNePal^#(n____(I, n____(P, I))) -> activate^#(I) , 27: isNePal^#(n____(I, n____(P, I))) -> activate^#(P) , 28: isNePal^#(n____(I, n____(P, I))) -> U71^#(isQid(activate(I)), activate(P)) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {1,8,9,10,11,12,13,14,15,16,17,26,27,28}. These cover all (indirect) predecessors of dependency pairs {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28}, 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) -> isList^#(activate(V2)) , U21^#(tt(), V2) -> activate^#(V2) , isList^#(V) -> activate^#(V) , isList^#(V) -> isNeList^#(activate(V)) , isList^#(n____(V1, V2)) -> U21^#(isList(activate(V1)), activate(V2)) , isList^#(n____(V1, V2)) -> isList^#(activate(V1)) , isList^#(n____(V1, V2)) -> activate^#(V1) , isList^#(n____(V1, V2)) -> activate^#(V2) , activate^#(n____(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) , isNeList^#(V) -> c_5(activate^#(V)) , isNeList^#(n____(V1, V2)) -> isList^#(activate(V1)) , isNeList^#(n____(V1, V2)) -> activate^#(V1) , isNeList^#(n____(V1, V2)) -> activate^#(V2) , isNeList^#(n____(V1, V2)) -> isNeList^#(activate(V1)) , isNeList^#(n____(V1, V2)) -> U41^#(isList(activate(V1)), activate(V2)) , isNeList^#(n____(V1, V2)) -> U51^#(isNeList(activate(V1)), activate(V2)) , U41^#(tt(), V2) -> activate^#(V2) , U41^#(tt(), V2) -> isNeList^#(activate(V2)) , U51^#(tt(), V2) -> isList^#(activate(V2)) , U51^#(tt(), V2) -> activate^#(V2) , U71^#(tt(), P) -> activate^#(P) , U71^#(tt(), P) -> isPal^#(activate(P)) , isPal^#(V) -> activate^#(V) , isPal^#(V) -> isNePal^#(activate(V)) , isNePal^#(V) -> c_12(activate^#(V)) , isNePal^#(n____(I, n____(P, I))) -> activate^#(I) , isNePal^#(n____(I, n____(P, I))) -> activate^#(P) , isNePal^#(n____(I, n____(P, I))) -> U71^#(isQid(activate(I)), activate(P)) } 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)) -> __(activate(X1), activate(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) -> isList^#(activate(V2)) , U21^#(tt(), V2) -> activate^#(V2) , isList^#(V) -> activate^#(V) , isList^#(V) -> isNeList^#(activate(V)) , isList^#(n____(V1, V2)) -> U21^#(isList(activate(V1)), activate(V2)) , isList^#(n____(V1, V2)) -> isList^#(activate(V1)) , isList^#(n____(V1, V2)) -> activate^#(V1) , isList^#(n____(V1, V2)) -> activate^#(V2) , activate^#(n____(X1, X2)) -> c_4(activate^#(X1), activate^#(X2)) , isNeList^#(V) -> c_5(activate^#(V)) , isNeList^#(n____(V1, V2)) -> isList^#(activate(V1)) , isNeList^#(n____(V1, V2)) -> activate^#(V1) , isNeList^#(n____(V1, V2)) -> activate^#(V2) , isNeList^#(n____(V1, V2)) -> isNeList^#(activate(V1)) , isNeList^#(n____(V1, V2)) -> U41^#(isList(activate(V1)), activate(V2)) , isNeList^#(n____(V1, V2)) -> U51^#(isNeList(activate(V1)), activate(V2)) , U41^#(tt(), V2) -> activate^#(V2) , U41^#(tt(), V2) -> isNeList^#(activate(V2)) , U51^#(tt(), V2) -> isList^#(activate(V2)) , U51^#(tt(), V2) -> activate^#(V2) , U71^#(tt(), P) -> activate^#(P) , U71^#(tt(), P) -> isPal^#(activate(P)) , isPal^#(V) -> activate^#(V) , isPal^#(V) -> isNePal^#(activate(V)) , isNePal^#(V) -> c_12(activate^#(V)) , isNePal^#(n____(I, n____(P, I))) -> activate^#(I) , isNePal^#(n____(I, n____(P, I))) -> activate^#(P) , isNePal^#(n____(I, n____(P, I))) -> U71^#(isQid(activate(I)), activate(P)) } 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)) -> __(activate(X1), activate(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^2))