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