YES(O(1),O(n^1)) 70.71/24.07 YES(O(1),O(n^1)) 70.71/24.07 70.71/24.07 We are left with following problem, upon which TcT provides the 70.71/24.07 certificate YES(O(1),O(n^1)). 70.71/24.07 70.71/24.07 Strict Trs: 70.71/24.07 { __(X1, X2) -> n____(X1, X2) 70.71/24.07 , __(X, nil()) -> X 70.71/24.07 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 70.71/24.07 , __(nil(), X) -> X 70.71/24.07 , nil() -> n__nil() 70.71/24.07 , U11(tt()) -> tt() 70.71/24.07 , U21(tt(), V2) -> U22(isList(activate(V2))) 70.71/24.07 , U22(tt()) -> tt() 70.71/24.07 , isList(V) -> U11(isNeList(activate(V))) 70.71/24.07 , isList(n__nil()) -> tt() 70.71/24.07 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 70.71/24.07 , activate(X) -> X 70.71/24.07 , activate(n__nil()) -> nil() 70.71/24.07 , activate(n____(X1, X2)) -> __(X1, X2) 70.71/24.07 , activate(n__a()) -> a() 70.71/24.07 , activate(n__e()) -> e() 70.71/24.07 , activate(n__i()) -> i() 70.71/24.07 , activate(n__o()) -> o() 70.71/24.07 , activate(n__u()) -> u() 70.71/24.07 , U31(tt()) -> tt() 70.71/24.07 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 70.71/24.07 , U42(tt()) -> tt() 70.71/24.07 , isNeList(V) -> U31(isQid(activate(V))) 70.71/24.07 , isNeList(n____(V1, V2)) -> 70.71/24.07 U41(isList(activate(V1)), activate(V2)) 70.71/24.07 , isNeList(n____(V1, V2)) -> 70.71/24.07 U51(isNeList(activate(V1)), activate(V2)) 70.71/24.07 , U51(tt(), V2) -> U52(isList(activate(V2))) 70.71/24.07 , U52(tt()) -> tt() 70.71/24.07 , U61(tt()) -> tt() 70.71/24.07 , U71(tt(), P) -> U72(isPal(activate(P))) 70.71/24.07 , U72(tt()) -> tt() 70.71/24.07 , isPal(V) -> U81(isNePal(activate(V))) 70.71/24.07 , isPal(n__nil()) -> tt() 70.71/24.07 , U81(tt()) -> tt() 70.71/24.07 , isQid(n__a()) -> tt() 70.71/24.07 , isQid(n__e()) -> tt() 70.71/24.07 , isQid(n__i()) -> tt() 70.71/24.07 , isQid(n__o()) -> tt() 70.71/24.07 , isQid(n__u()) -> tt() 70.71/24.07 , isNePal(V) -> U61(isQid(activate(V))) 70.71/24.07 , isNePal(n____(I, __(P, I))) -> 70.71/24.07 U71(isQid(activate(I)), activate(P)) 70.71/24.07 , a() -> n__a() 70.71/24.07 , e() -> n__e() 70.71/24.07 , i() -> n__i() 70.71/24.07 , o() -> n__o() 70.71/24.07 , u() -> n__u() } 70.71/24.07 Obligation: 70.71/24.07 innermost runtime complexity 70.71/24.07 Answer: 70.71/24.07 YES(O(1),O(n^1)) 70.71/24.07 70.71/24.07 Arguments of following rules are not normal-forms: 70.71/24.07 70.71/24.07 { __(X, nil()) -> X 70.71/24.07 , __(__(X, Y), Z) -> __(X, __(Y, Z)) 70.71/24.07 , __(nil(), X) -> X 70.71/24.07 , isNePal(n____(I, __(P, I))) -> 70.71/24.07 U71(isQid(activate(I)), activate(P)) } 70.71/24.07 70.71/24.07 All above mentioned rules can be savely removed. 70.71/24.07 70.71/24.07 We are left with following problem, upon which TcT provides the 70.71/24.07 certificate YES(O(1),O(n^1)). 70.71/24.07 70.71/24.07 Strict Trs: 70.71/24.07 { __(X1, X2) -> n____(X1, X2) 70.71/24.07 , nil() -> n__nil() 70.71/24.07 , U11(tt()) -> tt() 70.71/24.07 , U21(tt(), V2) -> U22(isList(activate(V2))) 70.71/24.07 , U22(tt()) -> tt() 70.71/24.07 , isList(V) -> U11(isNeList(activate(V))) 70.71/24.07 , isList(n__nil()) -> tt() 70.71/24.07 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 70.71/24.07 , activate(X) -> X 70.71/24.07 , activate(n__nil()) -> nil() 70.71/24.07 , activate(n____(X1, X2)) -> __(X1, X2) 70.71/24.07 , activate(n__a()) -> a() 70.71/24.07 , activate(n__e()) -> e() 70.71/24.07 , activate(n__i()) -> i() 70.71/24.07 , activate(n__o()) -> o() 70.71/24.07 , activate(n__u()) -> u() 70.71/24.07 , U31(tt()) -> tt() 70.71/24.07 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 70.71/24.07 , U42(tt()) -> tt() 70.71/24.07 , isNeList(V) -> U31(isQid(activate(V))) 70.71/24.07 , isNeList(n____(V1, V2)) -> 70.71/24.07 U41(isList(activate(V1)), activate(V2)) 70.71/24.07 , isNeList(n____(V1, V2)) -> 70.71/24.07 U51(isNeList(activate(V1)), activate(V2)) 70.71/24.07 , U51(tt(), V2) -> U52(isList(activate(V2))) 70.71/24.07 , U52(tt()) -> tt() 70.71/24.07 , U61(tt()) -> tt() 70.71/24.07 , U71(tt(), P) -> U72(isPal(activate(P))) 70.71/24.07 , U72(tt()) -> tt() 70.71/24.07 , isPal(V) -> U81(isNePal(activate(V))) 70.71/24.07 , isPal(n__nil()) -> tt() 70.71/24.07 , U81(tt()) -> tt() 70.71/24.07 , isQid(n__a()) -> tt() 70.71/24.07 , isQid(n__e()) -> tt() 70.71/24.07 , isQid(n__i()) -> tt() 70.71/24.07 , isQid(n__o()) -> tt() 70.71/24.07 , isQid(n__u()) -> tt() 70.71/24.07 , isNePal(V) -> U61(isQid(activate(V))) 70.71/24.07 , a() -> n__a() 70.71/24.07 , e() -> n__e() 70.71/24.07 , i() -> n__i() 70.71/24.07 , o() -> n__o() 70.71/24.07 , u() -> n__u() } 70.71/24.07 Obligation: 70.71/24.07 innermost runtime complexity 70.71/24.07 Answer: 70.71/24.07 YES(O(1),O(n^1)) 70.71/24.07 70.71/24.07 The weightgap principle applies (using the following nonconstant 70.71/24.07 growth matrix-interpretation) 70.71/24.07 70.71/24.07 The following argument positions are usable: 70.71/24.07 Uargs(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1}, 70.71/24.07 Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2}, 70.71/24.07 Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2}, 70.71/24.07 Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1}, 70.71/24.07 Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {1}, 70.71/24.07 Uargs(isNePal) = {1} 70.71/24.07 70.71/24.07 TcT has computed the following matrix interpretation satisfying 70.71/24.07 not(EDA) and not(IDA(1)). 70.71/24.07 70.71/24.07 [__](x1, x2) = [1] x1 + [1] x2 + [7] 70.71/24.07 70.71/24.07 [nil] = [5] 70.71/24.07 70.71/24.07 [U11](x1) = [1] x1 + [7] 70.71/24.07 70.71/24.07 [tt] = [7] 70.71/24.07 70.71/24.07 [U21](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.07 70.71/24.07 [U22](x1) = [1] x1 + [7] 70.71/24.07 70.71/24.07 [isList](x1) = [1] x1 + [1] 70.71/24.07 70.71/24.07 [activate](x1) = [1] x1 + [7] 70.71/24.07 70.71/24.07 [U31](x1) = [1] x1 + [1] 70.71/24.07 70.71/24.07 [U41](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.07 70.71/24.07 [U42](x1) = [1] x1 + [7] 70.71/24.07 70.71/24.07 [isNeList](x1) = [1] x1 + [1] 70.71/24.07 70.71/24.07 [U51](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.07 70.71/24.07 [U52](x1) = [1] x1 + [7] 70.71/24.07 70.71/24.07 [U61](x1) = [1] x1 + [1] 70.71/24.07 70.71/24.07 [U71](x1, x2) = [1] x1 + [1] x2 + [7] 70.71/24.07 70.71/24.07 [U72](x1) = [1] x1 + [1] 70.71/24.07 70.71/24.07 [isPal](x1) = [1] x1 + [7] 70.71/24.07 70.71/24.07 [U81](x1) = [1] x1 + [1] 70.71/24.07 70.71/24.07 [n__nil] = [7] 70.71/24.07 70.71/24.07 [n____](x1, x2) = [1] x1 + [1] x2 + [5] 70.71/24.07 70.71/24.07 [isQid](x1) = [1] x1 + [7] 70.71/24.07 70.71/24.07 [isNePal](x1) = [1] x1 + [7] 70.71/24.07 70.71/24.07 [n__a] = [7] 70.71/24.07 70.71/24.07 [n__e] = [7] 70.71/24.07 70.71/24.07 [n__i] = [7] 70.71/24.07 70.71/24.07 [n__o] = [7] 70.71/24.07 70.71/24.07 [n__u] = [7] 70.71/24.07 70.71/24.07 [a] = [5] 70.71/24.07 70.71/24.07 [e] = [5] 70.71/24.07 70.71/24.07 [i] = [5] 70.71/24.07 70.71/24.07 [o] = [3] 70.71/24.07 70.71/24.07 [u] = [5] 70.71/24.07 70.71/24.07 The order satisfies the following ordering constraints: 70.71/24.07 70.71/24.07 [__(X1, X2)] = [1] X1 + [1] X2 + [7] 70.71/24.07 > [1] X1 + [1] X2 + [5] 70.71/24.07 = [n____(X1, X2)] 70.71/24.07 70.71/24.07 [nil()] = [5] 70.71/24.07 ? [7] 70.71/24.07 = [n__nil()] 70.71/24.07 70.71/24.07 [U11(tt())] = [14] 70.71/24.07 > [7] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [U21(tt(), V2)] = [1] V2 + [7] 70.71/24.07 ? [1] V2 + [15] 70.71/24.07 = [U22(isList(activate(V2)))] 70.71/24.07 70.71/24.07 [U22(tt())] = [14] 70.71/24.07 > [7] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [isList(V)] = [1] V + [1] 70.71/24.07 ? [1] V + [15] 70.71/24.07 = [U11(isNeList(activate(V)))] 70.71/24.07 70.71/24.07 [isList(n__nil())] = [8] 70.71/24.07 > [7] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [isList(n____(V1, V2))] = [1] V2 + [1] V1 + [6] 70.71/24.07 ? [1] V2 + [1] V1 + [15] 70.71/24.07 = [U21(isList(activate(V1)), activate(V2))] 70.71/24.07 70.71/24.07 [activate(X)] = [1] X + [7] 70.71/24.07 > [1] X + [0] 70.71/24.07 = [X] 70.71/24.07 70.71/24.07 [activate(n__nil())] = [14] 70.71/24.07 > [5] 70.71/24.07 = [nil()] 70.71/24.07 70.71/24.07 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [12] 70.71/24.07 > [1] X1 + [1] X2 + [7] 70.71/24.07 = [__(X1, X2)] 70.71/24.07 70.71/24.07 [activate(n__a())] = [14] 70.71/24.07 > [5] 70.71/24.07 = [a()] 70.71/24.07 70.71/24.07 [activate(n__e())] = [14] 70.71/24.07 > [5] 70.71/24.07 = [e()] 70.71/24.07 70.71/24.07 [activate(n__i())] = [14] 70.71/24.07 > [5] 70.71/24.07 = [i()] 70.71/24.07 70.71/24.07 [activate(n__o())] = [14] 70.71/24.07 > [3] 70.71/24.07 = [o()] 70.71/24.07 70.71/24.07 [activate(n__u())] = [14] 70.71/24.07 > [5] 70.71/24.07 = [u()] 70.71/24.07 70.71/24.07 [U31(tt())] = [8] 70.71/24.07 > [7] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [U41(tt(), V2)] = [1] V2 + [7] 70.71/24.07 ? [1] V2 + [15] 70.71/24.07 = [U42(isNeList(activate(V2)))] 70.71/24.07 70.71/24.07 [U42(tt())] = [14] 70.71/24.07 > [7] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [isNeList(V)] = [1] V + [1] 70.71/24.07 ? [1] V + [15] 70.71/24.07 = [U31(isQid(activate(V)))] 70.71/24.07 70.71/24.07 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [6] 70.71/24.07 ? [1] V2 + [1] V1 + [15] 70.71/24.07 = [U41(isList(activate(V1)), activate(V2))] 70.71/24.07 70.71/24.07 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [6] 70.71/24.07 ? [1] V2 + [1] V1 + [15] 70.71/24.07 = [U51(isNeList(activate(V1)), activate(V2))] 70.71/24.07 70.71/24.07 [U51(tt(), V2)] = [1] V2 + [7] 70.71/24.07 ? [1] V2 + [15] 70.71/24.07 = [U52(isList(activate(V2)))] 70.71/24.07 70.71/24.07 [U52(tt())] = [14] 70.71/24.07 > [7] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [U61(tt())] = [8] 70.71/24.07 > [7] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [U71(tt(), P)] = [1] P + [14] 70.71/24.07 ? [1] P + [15] 70.71/24.07 = [U72(isPal(activate(P)))] 70.71/24.07 70.71/24.07 [U72(tt())] = [8] 70.71/24.07 > [7] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [isPal(V)] = [1] V + [7] 70.71/24.07 ? [1] V + [15] 70.71/24.07 = [U81(isNePal(activate(V)))] 70.71/24.07 70.71/24.07 [isPal(n__nil())] = [14] 70.71/24.07 > [7] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [U81(tt())] = [8] 70.71/24.07 > [7] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [isQid(n__a())] = [14] 70.71/24.07 > [7] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [isQid(n__e())] = [14] 70.71/24.07 > [7] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [isQid(n__i())] = [14] 70.71/24.07 > [7] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [isQid(n__o())] = [14] 70.71/24.07 > [7] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [isQid(n__u())] = [14] 70.71/24.07 > [7] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [isNePal(V)] = [1] V + [7] 70.71/24.07 ? [1] V + [15] 70.71/24.07 = [U61(isQid(activate(V)))] 70.71/24.07 70.71/24.07 [a()] = [5] 70.71/24.07 ? [7] 70.71/24.07 = [n__a()] 70.71/24.07 70.71/24.07 [e()] = [5] 70.71/24.07 ? [7] 70.71/24.07 = [n__e()] 70.71/24.07 70.71/24.07 [i()] = [5] 70.71/24.07 ? [7] 70.71/24.07 = [n__i()] 70.71/24.07 70.71/24.07 [o()] = [3] 70.71/24.07 ? [7] 70.71/24.07 = [n__o()] 70.71/24.07 70.71/24.07 [u()] = [5] 70.71/24.07 ? [7] 70.71/24.07 = [n__u()] 70.71/24.07 70.71/24.07 70.71/24.07 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.71/24.07 70.71/24.07 We are left with following problem, upon which TcT provides the 70.71/24.07 certificate YES(O(1),O(n^1)). 70.71/24.07 70.71/24.07 Strict Trs: 70.71/24.07 { nil() -> n__nil() 70.71/24.07 , U21(tt(), V2) -> U22(isList(activate(V2))) 70.71/24.07 , isList(V) -> U11(isNeList(activate(V))) 70.71/24.07 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 70.71/24.07 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 70.71/24.07 , isNeList(V) -> U31(isQid(activate(V))) 70.71/24.07 , isNeList(n____(V1, V2)) -> 70.71/24.07 U41(isList(activate(V1)), activate(V2)) 70.71/24.07 , isNeList(n____(V1, V2)) -> 70.71/24.07 U51(isNeList(activate(V1)), activate(V2)) 70.71/24.07 , U51(tt(), V2) -> U52(isList(activate(V2))) 70.71/24.07 , U71(tt(), P) -> U72(isPal(activate(P))) 70.71/24.07 , isPal(V) -> U81(isNePal(activate(V))) 70.71/24.07 , isNePal(V) -> U61(isQid(activate(V))) 70.71/24.07 , a() -> n__a() 70.71/24.07 , e() -> n__e() 70.71/24.07 , i() -> n__i() 70.71/24.07 , o() -> n__o() 70.71/24.07 , u() -> n__u() } 70.71/24.07 Weak Trs: 70.71/24.07 { __(X1, X2) -> n____(X1, X2) 70.71/24.07 , U11(tt()) -> tt() 70.71/24.07 , U22(tt()) -> tt() 70.71/24.07 , isList(n__nil()) -> tt() 70.71/24.07 , activate(X) -> X 70.71/24.07 , activate(n__nil()) -> nil() 70.71/24.07 , activate(n____(X1, X2)) -> __(X1, X2) 70.71/24.07 , activate(n__a()) -> a() 70.71/24.07 , activate(n__e()) -> e() 70.71/24.07 , activate(n__i()) -> i() 70.71/24.07 , activate(n__o()) -> o() 70.71/24.07 , activate(n__u()) -> u() 70.71/24.07 , U31(tt()) -> tt() 70.71/24.07 , U42(tt()) -> tt() 70.71/24.07 , U52(tt()) -> tt() 70.71/24.07 , U61(tt()) -> tt() 70.71/24.07 , U72(tt()) -> tt() 70.71/24.07 , isPal(n__nil()) -> tt() 70.71/24.07 , U81(tt()) -> tt() 70.71/24.07 , isQid(n__a()) -> tt() 70.71/24.07 , isQid(n__e()) -> tt() 70.71/24.07 , isQid(n__i()) -> tt() 70.71/24.07 , isQid(n__o()) -> tt() 70.71/24.07 , isQid(n__u()) -> tt() } 70.71/24.07 Obligation: 70.71/24.07 innermost runtime complexity 70.71/24.07 Answer: 70.71/24.07 YES(O(1),O(n^1)) 70.71/24.07 70.71/24.07 The weightgap principle applies (using the following nonconstant 70.71/24.07 growth matrix-interpretation) 70.71/24.07 70.71/24.07 The following argument positions are usable: 70.71/24.07 Uargs(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1}, 70.71/24.07 Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2}, 70.71/24.07 Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2}, 70.71/24.07 Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1}, 70.71/24.07 Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {1}, 70.71/24.07 Uargs(isNePal) = {1} 70.71/24.07 70.71/24.07 TcT has computed the following matrix interpretation satisfying 70.71/24.07 not(EDA) and not(IDA(1)). 70.71/24.07 70.71/24.07 [__](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.07 70.71/24.07 [nil] = [0] 70.71/24.07 70.71/24.07 [U11](x1) = [1] x1 + [0] 70.71/24.07 70.71/24.07 [tt] = [0] 70.71/24.07 70.71/24.07 [U21](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.07 70.71/24.07 [U22](x1) = [1] x1 + [1] 70.71/24.07 70.71/24.07 [isList](x1) = [1] x1 + [1] 70.71/24.07 70.71/24.07 [activate](x1) = [1] x1 + [0] 70.71/24.07 70.71/24.07 [U31](x1) = [1] x1 + [7] 70.71/24.07 70.71/24.07 [U41](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.07 70.71/24.07 [U42](x1) = [1] x1 + [7] 70.71/24.07 70.71/24.07 [isNeList](x1) = [1] x1 + [0] 70.71/24.07 70.71/24.07 [U51](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.07 70.71/24.07 [U52](x1) = [1] x1 + [5] 70.71/24.07 70.71/24.07 [U61](x1) = [1] x1 + [7] 70.71/24.07 70.71/24.07 [U71](x1, x2) = [1] x1 + [1] x2 + [7] 70.71/24.07 70.71/24.07 [U72](x1) = [1] x1 + [3] 70.71/24.07 70.71/24.07 [isPal](x1) = [1] x1 + [4] 70.71/24.07 70.71/24.07 [U81](x1) = [1] x1 + [7] 70.71/24.07 70.71/24.07 [n__nil] = [0] 70.71/24.07 70.71/24.07 [n____](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.07 70.71/24.07 [isQid](x1) = [1] x1 + [0] 70.71/24.07 70.71/24.07 [isNePal](x1) = [1] x1 + [0] 70.71/24.07 70.71/24.07 [n__a] = [0] 70.71/24.07 70.71/24.07 [n__e] = [0] 70.71/24.07 70.71/24.07 [n__i] = [0] 70.71/24.07 70.71/24.07 [n__o] = [0] 70.71/24.07 70.71/24.07 [n__u] = [0] 70.71/24.07 70.71/24.07 [a] = [0] 70.71/24.07 70.71/24.07 [e] = [0] 70.71/24.07 70.71/24.07 [i] = [0] 70.71/24.07 70.71/24.07 [o] = [0] 70.71/24.07 70.71/24.07 [u] = [0] 70.71/24.07 70.71/24.07 The order satisfies the following ordering constraints: 70.71/24.07 70.71/24.07 [__(X1, X2)] = [1] X1 + [1] X2 + [0] 70.71/24.07 >= [1] X1 + [1] X2 + [0] 70.71/24.07 = [n____(X1, X2)] 70.71/24.07 70.71/24.07 [nil()] = [0] 70.71/24.07 >= [0] 70.71/24.07 = [n__nil()] 70.71/24.07 70.71/24.07 [U11(tt())] = [0] 70.71/24.07 >= [0] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [U21(tt(), V2)] = [1] V2 + [0] 70.71/24.07 ? [1] V2 + [2] 70.71/24.07 = [U22(isList(activate(V2)))] 70.71/24.07 70.71/24.07 [U22(tt())] = [1] 70.71/24.07 > [0] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [isList(V)] = [1] V + [1] 70.71/24.07 > [1] V + [0] 70.71/24.07 = [U11(isNeList(activate(V)))] 70.71/24.07 70.71/24.07 [isList(n__nil())] = [1] 70.71/24.07 > [0] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [isList(n____(V1, V2))] = [1] V2 + [1] V1 + [1] 70.71/24.07 >= [1] V2 + [1] V1 + [1] 70.71/24.07 = [U21(isList(activate(V1)), activate(V2))] 70.71/24.07 70.71/24.07 [activate(X)] = [1] X + [0] 70.71/24.07 >= [1] X + [0] 70.71/24.07 = [X] 70.71/24.07 70.71/24.07 [activate(n__nil())] = [0] 70.71/24.07 >= [0] 70.71/24.07 = [nil()] 70.71/24.07 70.71/24.07 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0] 70.71/24.07 >= [1] X1 + [1] X2 + [0] 70.71/24.07 = [__(X1, X2)] 70.71/24.07 70.71/24.07 [activate(n__a())] = [0] 70.71/24.07 >= [0] 70.71/24.07 = [a()] 70.71/24.07 70.71/24.07 [activate(n__e())] = [0] 70.71/24.07 >= [0] 70.71/24.07 = [e()] 70.71/24.07 70.71/24.07 [activate(n__i())] = [0] 70.71/24.07 >= [0] 70.71/24.07 = [i()] 70.71/24.07 70.71/24.07 [activate(n__o())] = [0] 70.71/24.07 >= [0] 70.71/24.07 = [o()] 70.71/24.07 70.71/24.07 [activate(n__u())] = [0] 70.71/24.07 >= [0] 70.71/24.07 = [u()] 70.71/24.07 70.71/24.07 [U31(tt())] = [7] 70.71/24.07 > [0] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [U41(tt(), V2)] = [1] V2 + [0] 70.71/24.07 ? [1] V2 + [7] 70.71/24.07 = [U42(isNeList(activate(V2)))] 70.71/24.07 70.71/24.07 [U42(tt())] = [7] 70.71/24.07 > [0] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [isNeList(V)] = [1] V + [0] 70.71/24.07 ? [1] V + [7] 70.71/24.07 = [U31(isQid(activate(V)))] 70.71/24.07 70.71/24.07 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0] 70.71/24.07 ? [1] V2 + [1] V1 + [1] 70.71/24.07 = [U41(isList(activate(V1)), activate(V2))] 70.71/24.07 70.71/24.07 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0] 70.71/24.07 >= [1] V2 + [1] V1 + [0] 70.71/24.07 = [U51(isNeList(activate(V1)), activate(V2))] 70.71/24.07 70.71/24.07 [U51(tt(), V2)] = [1] V2 + [0] 70.71/24.07 ? [1] V2 + [6] 70.71/24.07 = [U52(isList(activate(V2)))] 70.71/24.07 70.71/24.07 [U52(tt())] = [5] 70.71/24.07 > [0] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [U61(tt())] = [7] 70.71/24.07 > [0] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [U71(tt(), P)] = [1] P + [7] 70.71/24.07 >= [1] P + [7] 70.71/24.07 = [U72(isPal(activate(P)))] 70.71/24.07 70.71/24.07 [U72(tt())] = [3] 70.71/24.07 > [0] 70.71/24.07 = [tt()] 70.71/24.07 70.71/24.07 [isPal(V)] = [1] V + [4] 70.71/24.07 ? [1] V + [7] 70.71/24.07 = [U81(isNePal(activate(V)))] 70.71/24.07 70.71/24.07 [isPal(n__nil())] = [4] 70.71/24.07 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [U81(tt())] = [7] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isQid(n__a())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isQid(n__e())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isQid(n__i())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isQid(n__o())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isQid(n__u())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isNePal(V)] = [1] V + [0] 70.71/24.08 ? [1] V + [7] 70.71/24.08 = [U61(isQid(activate(V)))] 70.71/24.08 70.71/24.08 [a()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__a()] 70.71/24.08 70.71/24.08 [e()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__e()] 70.71/24.08 70.71/24.08 [i()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__i()] 70.71/24.08 70.71/24.08 [o()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__o()] 70.71/24.08 70.71/24.08 [u()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__u()] 70.71/24.08 70.71/24.08 70.71/24.08 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.71/24.08 70.71/24.08 We are left with following problem, upon which TcT provides the 70.71/24.08 certificate YES(O(1),O(n^1)). 70.71/24.08 70.71/24.08 Strict Trs: 70.71/24.08 { nil() -> n__nil() 70.71/24.08 , U21(tt(), V2) -> U22(isList(activate(V2))) 70.71/24.08 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 70.71/24.08 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 70.71/24.08 , isNeList(V) -> U31(isQid(activate(V))) 70.71/24.08 , isNeList(n____(V1, V2)) -> 70.71/24.08 U41(isList(activate(V1)), activate(V2)) 70.71/24.08 , isNeList(n____(V1, V2)) -> 70.71/24.08 U51(isNeList(activate(V1)), activate(V2)) 70.71/24.08 , U51(tt(), V2) -> U52(isList(activate(V2))) 70.71/24.08 , U71(tt(), P) -> U72(isPal(activate(P))) 70.71/24.08 , isPal(V) -> U81(isNePal(activate(V))) 70.71/24.08 , isNePal(V) -> U61(isQid(activate(V))) 70.71/24.08 , a() -> n__a() 70.71/24.08 , e() -> n__e() 70.71/24.08 , i() -> n__i() 70.71/24.08 , o() -> n__o() 70.71/24.08 , u() -> n__u() } 70.71/24.08 Weak Trs: 70.71/24.08 { __(X1, X2) -> n____(X1, X2) 70.71/24.08 , U11(tt()) -> tt() 70.71/24.08 , U22(tt()) -> tt() 70.71/24.08 , isList(V) -> U11(isNeList(activate(V))) 70.71/24.08 , isList(n__nil()) -> tt() 70.71/24.08 , activate(X) -> X 70.71/24.08 , activate(n__nil()) -> nil() 70.71/24.08 , activate(n____(X1, X2)) -> __(X1, X2) 70.71/24.08 , activate(n__a()) -> a() 70.71/24.08 , activate(n__e()) -> e() 70.71/24.08 , activate(n__i()) -> i() 70.71/24.08 , activate(n__o()) -> o() 70.71/24.08 , activate(n__u()) -> u() 70.71/24.08 , U31(tt()) -> tt() 70.71/24.08 , U42(tt()) -> tt() 70.71/24.08 , U52(tt()) -> tt() 70.71/24.08 , U61(tt()) -> tt() 70.71/24.08 , U72(tt()) -> tt() 70.71/24.08 , isPal(n__nil()) -> tt() 70.71/24.08 , U81(tt()) -> tt() 70.71/24.08 , isQid(n__a()) -> tt() 70.71/24.08 , isQid(n__e()) -> tt() 70.71/24.08 , isQid(n__i()) -> tt() 70.71/24.08 , isQid(n__o()) -> tt() 70.71/24.08 , isQid(n__u()) -> tt() } 70.71/24.08 Obligation: 70.71/24.08 innermost runtime complexity 70.71/24.08 Answer: 70.71/24.08 YES(O(1),O(n^1)) 70.71/24.08 70.71/24.08 The weightgap principle applies (using the following nonconstant 70.71/24.08 growth matrix-interpretation) 70.71/24.08 70.71/24.08 The following argument positions are usable: 70.71/24.08 Uargs(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1}, 70.71/24.08 Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2}, 70.71/24.08 Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2}, 70.71/24.08 Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1}, 70.71/24.08 Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {1}, 70.71/24.08 Uargs(isNePal) = {1} 70.71/24.08 70.71/24.08 TcT has computed the following matrix interpretation satisfying 70.71/24.08 not(EDA) and not(IDA(1)). 70.71/24.08 70.71/24.08 [__](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.08 70.71/24.08 [nil] = [0] 70.71/24.08 70.71/24.08 [U11](x1) = [1] x1 + [0] 70.71/24.08 70.71/24.08 [tt] = [0] 70.71/24.08 70.71/24.08 [U21](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.08 70.71/24.08 [U22](x1) = [1] x1 + [7] 70.71/24.08 70.71/24.08 [isList](x1) = [1] x1 + [0] 70.71/24.08 70.71/24.08 [activate](x1) = [1] x1 + [0] 70.71/24.08 70.71/24.08 [U31](x1) = [1] x1 + [7] 70.71/24.08 70.71/24.08 [U41](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.08 70.71/24.08 [U42](x1) = [1] x1 + [3] 70.71/24.08 70.71/24.08 [isNeList](x1) = [1] x1 + [0] 70.71/24.08 70.71/24.08 [U51](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.08 70.71/24.08 [U52](x1) = [1] x1 + [7] 70.71/24.08 70.71/24.08 [U61](x1) = [1] x1 + [7] 70.71/24.08 70.71/24.08 [U71](x1, x2) = [1] x1 + [1] x2 + [7] 70.71/24.08 70.71/24.08 [U72](x1) = [1] x1 + [7] 70.71/24.08 70.71/24.08 [isPal](x1) = [1] x1 + [4] 70.71/24.08 70.71/24.08 [U81](x1) = [1] x1 + [3] 70.71/24.08 70.71/24.08 [n__nil] = [0] 70.71/24.08 70.71/24.08 [n____](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.08 70.71/24.08 [isQid](x1) = [1] x1 + [0] 70.71/24.08 70.71/24.08 [isNePal](x1) = [1] x1 + [0] 70.71/24.08 70.71/24.08 [n__a] = [0] 70.71/24.08 70.71/24.08 [n__e] = [0] 70.71/24.08 70.71/24.08 [n__i] = [0] 70.71/24.08 70.71/24.08 [n__o] = [0] 70.71/24.08 70.71/24.08 [n__u] = [0] 70.71/24.08 70.71/24.08 [a] = [0] 70.71/24.08 70.71/24.08 [e] = [0] 70.71/24.08 70.71/24.08 [i] = [0] 70.71/24.08 70.71/24.08 [o] = [0] 70.71/24.08 70.71/24.08 [u] = [0] 70.71/24.08 70.71/24.08 The order satisfies the following ordering constraints: 70.71/24.08 70.71/24.08 [__(X1, X2)] = [1] X1 + [1] X2 + [0] 70.71/24.08 >= [1] X1 + [1] X2 + [0] 70.71/24.08 = [n____(X1, X2)] 70.71/24.08 70.71/24.08 [nil()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__nil()] 70.71/24.08 70.71/24.08 [U11(tt())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [U21(tt(), V2)] = [1] V2 + [0] 70.71/24.08 ? [1] V2 + [7] 70.71/24.08 = [U22(isList(activate(V2)))] 70.71/24.08 70.71/24.08 [U22(tt())] = [7] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isList(V)] = [1] V + [0] 70.71/24.08 >= [1] V + [0] 70.71/24.08 = [U11(isNeList(activate(V)))] 70.71/24.08 70.71/24.08 [isList(n__nil())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isList(n____(V1, V2))] = [1] V2 + [1] V1 + [0] 70.71/24.08 >= [1] V2 + [1] V1 + [0] 70.71/24.08 = [U21(isList(activate(V1)), activate(V2))] 70.71/24.08 70.71/24.08 [activate(X)] = [1] X + [0] 70.71/24.08 >= [1] X + [0] 70.71/24.08 = [X] 70.71/24.08 70.71/24.08 [activate(n__nil())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [nil()] 70.71/24.08 70.71/24.08 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0] 70.71/24.08 >= [1] X1 + [1] X2 + [0] 70.71/24.08 = [__(X1, X2)] 70.71/24.08 70.71/24.08 [activate(n__a())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [a()] 70.71/24.08 70.71/24.08 [activate(n__e())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [e()] 70.71/24.08 70.71/24.08 [activate(n__i())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [i()] 70.71/24.08 70.71/24.08 [activate(n__o())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [o()] 70.71/24.08 70.71/24.08 [activate(n__u())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [u()] 70.71/24.08 70.71/24.08 [U31(tt())] = [7] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [U41(tt(), V2)] = [1] V2 + [0] 70.71/24.08 ? [1] V2 + [3] 70.71/24.08 = [U42(isNeList(activate(V2)))] 70.71/24.08 70.71/24.08 [U42(tt())] = [3] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isNeList(V)] = [1] V + [0] 70.71/24.08 ? [1] V + [7] 70.71/24.08 = [U31(isQid(activate(V)))] 70.71/24.08 70.71/24.08 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0] 70.71/24.08 >= [1] V2 + [1] V1 + [0] 70.71/24.08 = [U41(isList(activate(V1)), activate(V2))] 70.71/24.08 70.71/24.08 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0] 70.71/24.08 >= [1] V2 + [1] V1 + [0] 70.71/24.08 = [U51(isNeList(activate(V1)), activate(V2))] 70.71/24.08 70.71/24.08 [U51(tt(), V2)] = [1] V2 + [0] 70.71/24.08 ? [1] V2 + [7] 70.71/24.08 = [U52(isList(activate(V2)))] 70.71/24.08 70.71/24.08 [U52(tt())] = [7] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [U61(tt())] = [7] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [U71(tt(), P)] = [1] P + [7] 70.71/24.08 ? [1] P + [11] 70.71/24.08 = [U72(isPal(activate(P)))] 70.71/24.08 70.71/24.08 [U72(tt())] = [7] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isPal(V)] = [1] V + [4] 70.71/24.08 > [1] V + [3] 70.71/24.08 = [U81(isNePal(activate(V)))] 70.71/24.08 70.71/24.08 [isPal(n__nil())] = [4] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [U81(tt())] = [3] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isQid(n__a())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isQid(n__e())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isQid(n__i())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isQid(n__o())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isQid(n__u())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isNePal(V)] = [1] V + [0] 70.71/24.08 ? [1] V + [7] 70.71/24.08 = [U61(isQid(activate(V)))] 70.71/24.08 70.71/24.08 [a()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__a()] 70.71/24.08 70.71/24.08 [e()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__e()] 70.71/24.08 70.71/24.08 [i()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__i()] 70.71/24.08 70.71/24.08 [o()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__o()] 70.71/24.08 70.71/24.08 [u()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__u()] 70.71/24.08 70.71/24.08 70.71/24.08 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.71/24.08 70.71/24.08 We are left with following problem, upon which TcT provides the 70.71/24.08 certificate YES(O(1),O(n^1)). 70.71/24.08 70.71/24.08 Strict Trs: 70.71/24.08 { nil() -> n__nil() 70.71/24.08 , U21(tt(), V2) -> U22(isList(activate(V2))) 70.71/24.08 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 70.71/24.08 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 70.71/24.08 , isNeList(V) -> U31(isQid(activate(V))) 70.71/24.08 , isNeList(n____(V1, V2)) -> 70.71/24.08 U41(isList(activate(V1)), activate(V2)) 70.71/24.08 , isNeList(n____(V1, V2)) -> 70.71/24.08 U51(isNeList(activate(V1)), activate(V2)) 70.71/24.08 , U51(tt(), V2) -> U52(isList(activate(V2))) 70.71/24.08 , U71(tt(), P) -> U72(isPal(activate(P))) 70.71/24.08 , isNePal(V) -> U61(isQid(activate(V))) 70.71/24.08 , a() -> n__a() 70.71/24.08 , e() -> n__e() 70.71/24.08 , i() -> n__i() 70.71/24.08 , o() -> n__o() 70.71/24.08 , u() -> n__u() } 70.71/24.08 Weak Trs: 70.71/24.08 { __(X1, X2) -> n____(X1, X2) 70.71/24.08 , U11(tt()) -> tt() 70.71/24.08 , U22(tt()) -> tt() 70.71/24.08 , isList(V) -> U11(isNeList(activate(V))) 70.71/24.08 , isList(n__nil()) -> tt() 70.71/24.08 , activate(X) -> X 70.71/24.08 , activate(n__nil()) -> nil() 70.71/24.08 , activate(n____(X1, X2)) -> __(X1, X2) 70.71/24.08 , activate(n__a()) -> a() 70.71/24.08 , activate(n__e()) -> e() 70.71/24.08 , activate(n__i()) -> i() 70.71/24.08 , activate(n__o()) -> o() 70.71/24.08 , activate(n__u()) -> u() 70.71/24.08 , U31(tt()) -> tt() 70.71/24.08 , U42(tt()) -> tt() 70.71/24.08 , U52(tt()) -> tt() 70.71/24.08 , U61(tt()) -> tt() 70.71/24.08 , U72(tt()) -> tt() 70.71/24.08 , isPal(V) -> U81(isNePal(activate(V))) 70.71/24.08 , isPal(n__nil()) -> tt() 70.71/24.08 , U81(tt()) -> tt() 70.71/24.08 , isQid(n__a()) -> tt() 70.71/24.08 , isQid(n__e()) -> tt() 70.71/24.08 , isQid(n__i()) -> tt() 70.71/24.08 , isQid(n__o()) -> tt() 70.71/24.08 , isQid(n__u()) -> tt() } 70.71/24.08 Obligation: 70.71/24.08 innermost runtime complexity 70.71/24.08 Answer: 70.71/24.08 YES(O(1),O(n^1)) 70.71/24.08 70.71/24.08 The weightgap principle applies (using the following nonconstant 70.71/24.08 growth matrix-interpretation) 70.71/24.08 70.71/24.08 The following argument positions are usable: 70.71/24.08 Uargs(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1}, 70.71/24.08 Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2}, 70.71/24.08 Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2}, 70.71/24.08 Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1}, 70.71/24.08 Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {1}, 70.71/24.08 Uargs(isNePal) = {1} 70.71/24.08 70.71/24.08 TcT has computed the following matrix interpretation satisfying 70.71/24.08 not(EDA) and not(IDA(1)). 70.71/24.08 70.71/24.08 [__](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.08 70.71/24.08 [nil] = [0] 70.71/24.08 70.71/24.08 [U11](x1) = [1] x1 + [0] 70.71/24.08 70.71/24.08 [tt] = [0] 70.71/24.08 70.71/24.08 [U21](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.08 70.71/24.08 [U22](x1) = [1] x1 + [7] 70.71/24.08 70.71/24.08 [isList](x1) = [1] x1 + [0] 70.71/24.08 70.71/24.08 [activate](x1) = [1] x1 + [0] 70.71/24.08 70.71/24.08 [U31](x1) = [1] x1 + [7] 70.71/24.08 70.71/24.08 [U41](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.08 70.71/24.08 [U42](x1) = [1] x1 + [3] 70.71/24.08 70.71/24.08 [isNeList](x1) = [1] x1 + [0] 70.71/24.08 70.71/24.08 [U51](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.08 70.71/24.08 [U52](x1) = [1] x1 + [3] 70.71/24.08 70.71/24.08 [U61](x1) = [1] x1 + [3] 70.71/24.08 70.71/24.08 [U71](x1, x2) = [1] x1 + [1] x2 + [7] 70.71/24.08 70.71/24.08 [U72](x1) = [1] x1 + [2] 70.71/24.08 70.71/24.08 [isPal](x1) = [1] x1 + [4] 70.71/24.08 70.71/24.08 [U81](x1) = [1] x1 + [4] 70.71/24.08 70.71/24.08 [n__nil] = [0] 70.71/24.08 70.71/24.08 [n____](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.08 70.71/24.08 [isQid](x1) = [1] x1 + [0] 70.71/24.08 70.71/24.08 [isNePal](x1) = [1] x1 + [0] 70.71/24.08 70.71/24.08 [n__a] = [0] 70.71/24.08 70.71/24.08 [n__e] = [0] 70.71/24.08 70.71/24.08 [n__i] = [0] 70.71/24.08 70.71/24.08 [n__o] = [0] 70.71/24.08 70.71/24.08 [n__u] = [0] 70.71/24.08 70.71/24.08 [a] = [0] 70.71/24.08 70.71/24.08 [e] = [0] 70.71/24.08 70.71/24.08 [i] = [0] 70.71/24.08 70.71/24.08 [o] = [0] 70.71/24.08 70.71/24.08 [u] = [0] 70.71/24.08 70.71/24.08 The order satisfies the following ordering constraints: 70.71/24.08 70.71/24.08 [__(X1, X2)] = [1] X1 + [1] X2 + [0] 70.71/24.08 >= [1] X1 + [1] X2 + [0] 70.71/24.08 = [n____(X1, X2)] 70.71/24.08 70.71/24.08 [nil()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__nil()] 70.71/24.08 70.71/24.08 [U11(tt())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [U21(tt(), V2)] = [1] V2 + [0] 70.71/24.08 ? [1] V2 + [7] 70.71/24.08 = [U22(isList(activate(V2)))] 70.71/24.08 70.71/24.08 [U22(tt())] = [7] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isList(V)] = [1] V + [0] 70.71/24.08 >= [1] V + [0] 70.71/24.08 = [U11(isNeList(activate(V)))] 70.71/24.08 70.71/24.08 [isList(n__nil())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isList(n____(V1, V2))] = [1] V2 + [1] V1 + [0] 70.71/24.08 >= [1] V2 + [1] V1 + [0] 70.71/24.08 = [U21(isList(activate(V1)), activate(V2))] 70.71/24.08 70.71/24.08 [activate(X)] = [1] X + [0] 70.71/24.08 >= [1] X + [0] 70.71/24.08 = [X] 70.71/24.08 70.71/24.08 [activate(n__nil())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [nil()] 70.71/24.08 70.71/24.08 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0] 70.71/24.08 >= [1] X1 + [1] X2 + [0] 70.71/24.08 = [__(X1, X2)] 70.71/24.08 70.71/24.08 [activate(n__a())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [a()] 70.71/24.08 70.71/24.08 [activate(n__e())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [e()] 70.71/24.08 70.71/24.08 [activate(n__i())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [i()] 70.71/24.08 70.71/24.08 [activate(n__o())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [o()] 70.71/24.08 70.71/24.08 [activate(n__u())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [u()] 70.71/24.08 70.71/24.08 [U31(tt())] = [7] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [U41(tt(), V2)] = [1] V2 + [0] 70.71/24.08 ? [1] V2 + [3] 70.71/24.08 = [U42(isNeList(activate(V2)))] 70.71/24.08 70.71/24.08 [U42(tt())] = [3] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isNeList(V)] = [1] V + [0] 70.71/24.08 ? [1] V + [7] 70.71/24.08 = [U31(isQid(activate(V)))] 70.71/24.08 70.71/24.08 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0] 70.71/24.08 >= [1] V2 + [1] V1 + [0] 70.71/24.08 = [U41(isList(activate(V1)), activate(V2))] 70.71/24.08 70.71/24.08 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0] 70.71/24.08 >= [1] V2 + [1] V1 + [0] 70.71/24.08 = [U51(isNeList(activate(V1)), activate(V2))] 70.71/24.08 70.71/24.08 [U51(tt(), V2)] = [1] V2 + [0] 70.71/24.08 ? [1] V2 + [3] 70.71/24.08 = [U52(isList(activate(V2)))] 70.71/24.08 70.71/24.08 [U52(tt())] = [3] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [U61(tt())] = [3] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [U71(tt(), P)] = [1] P + [7] 70.71/24.08 > [1] P + [6] 70.71/24.08 = [U72(isPal(activate(P)))] 70.71/24.08 70.71/24.08 [U72(tt())] = [2] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isPal(V)] = [1] V + [4] 70.71/24.08 >= [1] V + [4] 70.71/24.08 = [U81(isNePal(activate(V)))] 70.71/24.08 70.71/24.08 [isPal(n__nil())] = [4] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [U81(tt())] = [4] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isQid(n__a())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isQid(n__e())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isQid(n__i())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isQid(n__o())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isQid(n__u())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isNePal(V)] = [1] V + [0] 70.71/24.08 ? [1] V + [3] 70.71/24.08 = [U61(isQid(activate(V)))] 70.71/24.08 70.71/24.08 [a()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__a()] 70.71/24.08 70.71/24.08 [e()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__e()] 70.71/24.08 70.71/24.08 [i()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__i()] 70.71/24.08 70.71/24.08 [o()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__o()] 70.71/24.08 70.71/24.08 [u()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__u()] 70.71/24.08 70.71/24.08 70.71/24.08 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.71/24.08 70.71/24.08 We are left with following problem, upon which TcT provides the 70.71/24.08 certificate YES(O(1),O(n^1)). 70.71/24.08 70.71/24.08 Strict Trs: 70.71/24.08 { nil() -> n__nil() 70.71/24.08 , U21(tt(), V2) -> U22(isList(activate(V2))) 70.71/24.08 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 70.71/24.08 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 70.71/24.08 , isNeList(V) -> U31(isQid(activate(V))) 70.71/24.08 , isNeList(n____(V1, V2)) -> 70.71/24.08 U41(isList(activate(V1)), activate(V2)) 70.71/24.08 , isNeList(n____(V1, V2)) -> 70.71/24.08 U51(isNeList(activate(V1)), activate(V2)) 70.71/24.08 , U51(tt(), V2) -> U52(isList(activate(V2))) 70.71/24.08 , isNePal(V) -> U61(isQid(activate(V))) 70.71/24.08 , a() -> n__a() 70.71/24.08 , e() -> n__e() 70.71/24.08 , i() -> n__i() 70.71/24.08 , o() -> n__o() 70.71/24.08 , u() -> n__u() } 70.71/24.08 Weak Trs: 70.71/24.08 { __(X1, X2) -> n____(X1, X2) 70.71/24.08 , U11(tt()) -> tt() 70.71/24.08 , U22(tt()) -> tt() 70.71/24.08 , isList(V) -> U11(isNeList(activate(V))) 70.71/24.08 , isList(n__nil()) -> tt() 70.71/24.08 , activate(X) -> X 70.71/24.08 , activate(n__nil()) -> nil() 70.71/24.08 , activate(n____(X1, X2)) -> __(X1, X2) 70.71/24.08 , activate(n__a()) -> a() 70.71/24.08 , activate(n__e()) -> e() 70.71/24.08 , activate(n__i()) -> i() 70.71/24.08 , activate(n__o()) -> o() 70.71/24.08 , activate(n__u()) -> u() 70.71/24.08 , U31(tt()) -> tt() 70.71/24.08 , U42(tt()) -> tt() 70.71/24.08 , U52(tt()) -> tt() 70.71/24.08 , U61(tt()) -> tt() 70.71/24.08 , U71(tt(), P) -> U72(isPal(activate(P))) 70.71/24.08 , U72(tt()) -> tt() 70.71/24.08 , isPal(V) -> U81(isNePal(activate(V))) 70.71/24.08 , isPal(n__nil()) -> tt() 70.71/24.08 , U81(tt()) -> tt() 70.71/24.08 , isQid(n__a()) -> tt() 70.71/24.08 , isQid(n__e()) -> tt() 70.71/24.08 , isQid(n__i()) -> tt() 70.71/24.08 , isQid(n__o()) -> tt() 70.71/24.08 , isQid(n__u()) -> tt() } 70.71/24.08 Obligation: 70.71/24.08 innermost runtime complexity 70.71/24.08 Answer: 70.71/24.08 YES(O(1),O(n^1)) 70.71/24.08 70.71/24.08 The weightgap principle applies (using the following nonconstant 70.71/24.08 growth matrix-interpretation) 70.71/24.08 70.71/24.08 The following argument positions are usable: 70.71/24.08 Uargs(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1}, 70.71/24.08 Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2}, 70.71/24.08 Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2}, 70.71/24.08 Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1}, 70.71/24.08 Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {1}, 70.71/24.08 Uargs(isNePal) = {1} 70.71/24.08 70.71/24.08 TcT has computed the following matrix interpretation satisfying 70.71/24.08 not(EDA) and not(IDA(1)). 70.71/24.08 70.71/24.08 [__](x1, x2) = [1] x1 + [1] x2 + [1] 70.71/24.08 70.71/24.08 [nil] = [0] 70.71/24.08 70.71/24.08 [U11](x1) = [1] x1 + [0] 70.71/24.08 70.71/24.08 [tt] = [0] 70.71/24.08 70.71/24.08 [U21](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.08 70.71/24.08 [U22](x1) = [1] x1 + [3] 70.71/24.08 70.71/24.08 [isList](x1) = [1] x1 + [0] 70.71/24.08 70.71/24.08 [activate](x1) = [1] x1 + [0] 70.71/24.08 70.71/24.08 [U31](x1) = [1] x1 + [7] 70.71/24.08 70.71/24.08 [U41](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.08 70.71/24.08 [U42](x1) = [1] x1 + [3] 70.71/24.08 70.71/24.08 [isNeList](x1) = [1] x1 + [0] 70.71/24.08 70.71/24.08 [U51](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.08 70.71/24.08 [U52](x1) = [1] x1 + [3] 70.71/24.08 70.71/24.08 [U61](x1) = [1] x1 + [3] 70.71/24.08 70.71/24.08 [U71](x1, x2) = [1] x1 + [1] x2 + [7] 70.71/24.08 70.71/24.08 [U72](x1) = [1] x1 + [3] 70.71/24.08 70.71/24.08 [isPal](x1) = [1] x1 + [4] 70.71/24.08 70.71/24.08 [U81](x1) = [1] x1 + [4] 70.71/24.08 70.71/24.08 [n__nil] = [0] 70.71/24.08 70.71/24.08 [n____](x1, x2) = [1] x1 + [1] x2 + [1] 70.71/24.08 70.71/24.08 [isQid](x1) = [1] x1 + [0] 70.71/24.08 70.71/24.08 [isNePal](x1) = [1] x1 + [0] 70.71/24.08 70.71/24.08 [n__a] = [0] 70.71/24.08 70.71/24.08 [n__e] = [0] 70.71/24.08 70.71/24.08 [n__i] = [0] 70.71/24.08 70.71/24.08 [n__o] = [0] 70.71/24.08 70.71/24.08 [n__u] = [0] 70.71/24.08 70.71/24.08 [a] = [0] 70.71/24.08 70.71/24.08 [e] = [0] 70.71/24.08 70.71/24.08 [i] = [0] 70.71/24.08 70.71/24.08 [o] = [0] 70.71/24.08 70.71/24.08 [u] = [0] 70.71/24.08 70.71/24.08 The order satisfies the following ordering constraints: 70.71/24.08 70.71/24.08 [__(X1, X2)] = [1] X1 + [1] X2 + [1] 70.71/24.08 >= [1] X1 + [1] X2 + [1] 70.71/24.08 = [n____(X1, X2)] 70.71/24.08 70.71/24.08 [nil()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__nil()] 70.71/24.08 70.71/24.08 [U11(tt())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [U21(tt(), V2)] = [1] V2 + [0] 70.71/24.08 ? [1] V2 + [3] 70.71/24.08 = [U22(isList(activate(V2)))] 70.71/24.08 70.71/24.08 [U22(tt())] = [3] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isList(V)] = [1] V + [0] 70.71/24.08 >= [1] V + [0] 70.71/24.08 = [U11(isNeList(activate(V)))] 70.71/24.08 70.71/24.08 [isList(n__nil())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isList(n____(V1, V2))] = [1] V2 + [1] V1 + [1] 70.71/24.08 > [1] V2 + [1] V1 + [0] 70.71/24.08 = [U21(isList(activate(V1)), activate(V2))] 70.71/24.08 70.71/24.08 [activate(X)] = [1] X + [0] 70.71/24.08 >= [1] X + [0] 70.71/24.08 = [X] 70.71/24.08 70.71/24.08 [activate(n__nil())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [nil()] 70.71/24.08 70.71/24.08 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [1] 70.71/24.08 >= [1] X1 + [1] X2 + [1] 70.71/24.08 = [__(X1, X2)] 70.71/24.08 70.71/24.08 [activate(n__a())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [a()] 70.71/24.08 70.71/24.08 [activate(n__e())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [e()] 70.71/24.08 70.71/24.08 [activate(n__i())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [i()] 70.71/24.08 70.71/24.08 [activate(n__o())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [o()] 70.71/24.08 70.71/24.08 [activate(n__u())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [u()] 70.71/24.08 70.71/24.08 [U31(tt())] = [7] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [U41(tt(), V2)] = [1] V2 + [0] 70.71/24.08 ? [1] V2 + [3] 70.71/24.08 = [U42(isNeList(activate(V2)))] 70.71/24.08 70.71/24.08 [U42(tt())] = [3] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isNeList(V)] = [1] V + [0] 70.71/24.08 ? [1] V + [7] 70.71/24.08 = [U31(isQid(activate(V)))] 70.71/24.08 70.71/24.08 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [1] 70.71/24.08 > [1] V2 + [1] V1 + [0] 70.71/24.08 = [U41(isList(activate(V1)), activate(V2))] 70.71/24.08 70.71/24.08 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [1] 70.71/24.08 > [1] V2 + [1] V1 + [0] 70.71/24.08 = [U51(isNeList(activate(V1)), activate(V2))] 70.71/24.08 70.71/24.08 [U51(tt(), V2)] = [1] V2 + [0] 70.71/24.08 ? [1] V2 + [3] 70.71/24.08 = [U52(isList(activate(V2)))] 70.71/24.08 70.71/24.08 [U52(tt())] = [3] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [U61(tt())] = [3] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [U71(tt(), P)] = [1] P + [7] 70.71/24.08 >= [1] P + [7] 70.71/24.08 = [U72(isPal(activate(P)))] 70.71/24.08 70.71/24.08 [U72(tt())] = [3] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isPal(V)] = [1] V + [4] 70.71/24.08 >= [1] V + [4] 70.71/24.08 = [U81(isNePal(activate(V)))] 70.71/24.08 70.71/24.08 [isPal(n__nil())] = [4] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [U81(tt())] = [4] 70.71/24.08 > [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isQid(n__a())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isQid(n__e())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isQid(n__i())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isQid(n__o())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isQid(n__u())] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [tt()] 70.71/24.08 70.71/24.08 [isNePal(V)] = [1] V + [0] 70.71/24.08 ? [1] V + [3] 70.71/24.08 = [U61(isQid(activate(V)))] 70.71/24.08 70.71/24.08 [a()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__a()] 70.71/24.08 70.71/24.08 [e()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__e()] 70.71/24.08 70.71/24.08 [i()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__i()] 70.71/24.08 70.71/24.08 [o()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__o()] 70.71/24.08 70.71/24.08 [u()] = [0] 70.71/24.08 >= [0] 70.71/24.08 = [n__u()] 70.71/24.08 70.71/24.08 70.71/24.08 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.71/24.08 70.71/24.08 We are left with following problem, upon which TcT provides the 70.71/24.08 certificate YES(O(1),O(n^1)). 70.71/24.08 70.71/24.08 Strict Trs: 70.71/24.08 { nil() -> n__nil() 70.71/24.08 , U21(tt(), V2) -> U22(isList(activate(V2))) 70.71/24.08 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 70.71/24.08 , isNeList(V) -> U31(isQid(activate(V))) 70.71/24.08 , U51(tt(), V2) -> U52(isList(activate(V2))) 70.71/24.08 , isNePal(V) -> U61(isQid(activate(V))) 70.71/24.08 , a() -> n__a() 70.71/24.08 , e() -> n__e() 70.71/24.08 , i() -> n__i() 70.71/24.08 , o() -> n__o() 70.71/24.08 , u() -> n__u() } 70.71/24.08 Weak Trs: 70.71/24.08 { __(X1, X2) -> n____(X1, X2) 70.71/24.08 , U11(tt()) -> tt() 70.71/24.08 , U22(tt()) -> tt() 70.71/24.08 , isList(V) -> U11(isNeList(activate(V))) 70.71/24.08 , isList(n__nil()) -> tt() 70.71/24.08 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 70.71/24.08 , activate(X) -> X 70.71/24.08 , activate(n__nil()) -> nil() 70.71/24.08 , activate(n____(X1, X2)) -> __(X1, X2) 70.71/24.08 , activate(n__a()) -> a() 70.71/24.08 , activate(n__e()) -> e() 70.71/24.08 , activate(n__i()) -> i() 70.71/24.08 , activate(n__o()) -> o() 70.71/24.08 , activate(n__u()) -> u() 70.71/24.08 , U31(tt()) -> tt() 70.71/24.08 , U42(tt()) -> tt() 70.71/24.08 , isNeList(n____(V1, V2)) -> 70.71/24.08 U41(isList(activate(V1)), activate(V2)) 70.71/24.09 , isNeList(n____(V1, V2)) -> 70.71/24.09 U51(isNeList(activate(V1)), activate(V2)) 70.71/24.09 , U52(tt()) -> tt() 70.71/24.09 , U61(tt()) -> tt() 70.71/24.09 , U71(tt(), P) -> U72(isPal(activate(P))) 70.71/24.09 , U72(tt()) -> tt() 70.71/24.09 , isPal(V) -> U81(isNePal(activate(V))) 70.71/24.09 , isPal(n__nil()) -> tt() 70.71/24.09 , U81(tt()) -> tt() 70.71/24.09 , isQid(n__a()) -> tt() 70.71/24.09 , isQid(n__e()) -> tt() 70.71/24.09 , isQid(n__i()) -> tt() 70.71/24.09 , isQid(n__o()) -> tt() 70.71/24.09 , isQid(n__u()) -> tt() } 70.71/24.09 Obligation: 70.71/24.09 innermost runtime complexity 70.71/24.09 Answer: 70.71/24.09 YES(O(1),O(n^1)) 70.71/24.09 70.71/24.09 The weightgap principle applies (using the following nonconstant 70.71/24.09 growth matrix-interpretation) 70.71/24.09 70.71/24.09 The following argument positions are usable: 70.71/24.09 Uargs(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1}, 70.71/24.09 Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2}, 70.71/24.09 Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2}, 70.71/24.09 Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1}, 70.71/24.09 Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {1}, 70.71/24.09 Uargs(isNePal) = {1} 70.71/24.09 70.71/24.09 TcT has computed the following matrix interpretation satisfying 70.71/24.09 not(EDA) and not(IDA(1)). 70.71/24.09 70.71/24.09 [__](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.09 70.71/24.09 [nil] = [1] 70.71/24.09 70.71/24.09 [U11](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [tt] = [1] 70.71/24.09 70.71/24.09 [U21](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.09 70.71/24.09 [U22](x1) = [1] x1 + [3] 70.71/24.09 70.71/24.09 [isList](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [activate](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [U31](x1) = [1] x1 + [7] 70.71/24.09 70.71/24.09 [U41](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.09 70.71/24.09 [U42](x1) = [1] x1 + [3] 70.71/24.09 70.71/24.09 [isNeList](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [U51](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.09 70.71/24.09 [U52](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [U61](x1) = [1] x1 + [7] 70.71/24.09 70.71/24.09 [U71](x1, x2) = [1] x2 + [7] 70.71/24.09 70.71/24.09 [U72](x1) = [1] x1 + [3] 70.71/24.09 70.71/24.09 [isPal](x1) = [1] x1 + [4] 70.71/24.09 70.71/24.09 [U81](x1) = [1] x1 + [4] 70.71/24.09 70.71/24.09 [n__nil] = [1] 70.71/24.09 70.71/24.09 [n____](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.09 70.71/24.09 [isQid](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [isNePal](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [n__a] = [1] 70.71/24.09 70.71/24.09 [n__e] = [1] 70.71/24.09 70.71/24.09 [n__i] = [1] 70.71/24.09 70.71/24.09 [n__o] = [1] 70.71/24.09 70.71/24.09 [n__u] = [1] 70.71/24.09 70.71/24.09 [a] = [1] 70.71/24.09 70.71/24.09 [e] = [1] 70.71/24.09 70.71/24.09 [i] = [1] 70.71/24.09 70.71/24.09 [o] = [1] 70.71/24.09 70.71/24.09 [u] = [1] 70.71/24.09 70.71/24.09 The order satisfies the following ordering constraints: 70.71/24.09 70.71/24.09 [__(X1, X2)] = [1] X1 + [1] X2 + [0] 70.71/24.09 >= [1] X1 + [1] X2 + [0] 70.71/24.09 = [n____(X1, X2)] 70.71/24.09 70.71/24.09 [nil()] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [n__nil()] 70.71/24.09 70.71/24.09 [U11(tt())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [U21(tt(), V2)] = [1] V2 + [1] 70.71/24.09 ? [1] V2 + [3] 70.71/24.09 = [U22(isList(activate(V2)))] 70.71/24.09 70.71/24.09 [U22(tt())] = [4] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isList(V)] = [1] V + [0] 70.71/24.09 >= [1] V + [0] 70.71/24.09 = [U11(isNeList(activate(V)))] 70.71/24.09 70.71/24.09 [isList(n__nil())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isList(n____(V1, V2))] = [1] V2 + [1] V1 + [0] 70.71/24.09 >= [1] V2 + [1] V1 + [0] 70.71/24.09 = [U21(isList(activate(V1)), activate(V2))] 70.71/24.09 70.71/24.09 [activate(X)] = [1] X + [0] 70.71/24.09 >= [1] X + [0] 70.71/24.09 = [X] 70.71/24.09 70.71/24.09 [activate(n__nil())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [nil()] 70.71/24.09 70.71/24.09 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0] 70.71/24.09 >= [1] X1 + [1] X2 + [0] 70.71/24.09 = [__(X1, X2)] 70.71/24.09 70.71/24.09 [activate(n__a())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [a()] 70.71/24.09 70.71/24.09 [activate(n__e())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [e()] 70.71/24.09 70.71/24.09 [activate(n__i())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [i()] 70.71/24.09 70.71/24.09 [activate(n__o())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [o()] 70.71/24.09 70.71/24.09 [activate(n__u())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [u()] 70.71/24.09 70.71/24.09 [U31(tt())] = [8] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [U41(tt(), V2)] = [1] V2 + [1] 70.71/24.09 ? [1] V2 + [3] 70.71/24.09 = [U42(isNeList(activate(V2)))] 70.71/24.09 70.71/24.09 [U42(tt())] = [4] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isNeList(V)] = [1] V + [0] 70.71/24.09 ? [1] V + [7] 70.71/24.09 = [U31(isQid(activate(V)))] 70.71/24.09 70.71/24.09 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0] 70.71/24.09 >= [1] V2 + [1] V1 + [0] 70.71/24.09 = [U41(isList(activate(V1)), activate(V2))] 70.71/24.09 70.71/24.09 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0] 70.71/24.09 >= [1] V2 + [1] V1 + [0] 70.71/24.09 = [U51(isNeList(activate(V1)), activate(V2))] 70.71/24.09 70.71/24.09 [U51(tt(), V2)] = [1] V2 + [1] 70.71/24.09 > [1] V2 + [0] 70.71/24.09 = [U52(isList(activate(V2)))] 70.71/24.09 70.71/24.09 [U52(tt())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [U61(tt())] = [8] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [U71(tt(), P)] = [1] P + [7] 70.71/24.09 >= [1] P + [7] 70.71/24.09 = [U72(isPal(activate(P)))] 70.71/24.09 70.71/24.09 [U72(tt())] = [4] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isPal(V)] = [1] V + [4] 70.71/24.09 >= [1] V + [4] 70.71/24.09 = [U81(isNePal(activate(V)))] 70.71/24.09 70.71/24.09 [isPal(n__nil())] = [5] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [U81(tt())] = [5] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isQid(n__a())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isQid(n__e())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isQid(n__i())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isQid(n__o())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isQid(n__u())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isNePal(V)] = [1] V + [0] 70.71/24.09 ? [1] V + [7] 70.71/24.09 = [U61(isQid(activate(V)))] 70.71/24.09 70.71/24.09 [a()] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [n__a()] 70.71/24.09 70.71/24.09 [e()] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [n__e()] 70.71/24.09 70.71/24.09 [i()] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [n__i()] 70.71/24.09 70.71/24.09 [o()] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [n__o()] 70.71/24.09 70.71/24.09 [u()] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [n__u()] 70.71/24.09 70.71/24.09 70.71/24.09 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.71/24.09 70.71/24.09 We are left with following problem, upon which TcT provides the 70.71/24.09 certificate YES(O(1),O(n^1)). 70.71/24.09 70.71/24.09 Strict Trs: 70.71/24.09 { nil() -> n__nil() 70.71/24.09 , U21(tt(), V2) -> U22(isList(activate(V2))) 70.71/24.09 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 70.71/24.09 , isNeList(V) -> U31(isQid(activate(V))) 70.71/24.09 , isNePal(V) -> U61(isQid(activate(V))) 70.71/24.09 , a() -> n__a() 70.71/24.09 , e() -> n__e() 70.71/24.09 , i() -> n__i() 70.71/24.09 , o() -> n__o() 70.71/24.09 , u() -> n__u() } 70.71/24.09 Weak Trs: 70.71/24.09 { __(X1, X2) -> n____(X1, X2) 70.71/24.09 , U11(tt()) -> tt() 70.71/24.09 , U22(tt()) -> tt() 70.71/24.09 , isList(V) -> U11(isNeList(activate(V))) 70.71/24.09 , isList(n__nil()) -> tt() 70.71/24.09 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 70.71/24.09 , activate(X) -> X 70.71/24.09 , activate(n__nil()) -> nil() 70.71/24.09 , activate(n____(X1, X2)) -> __(X1, X2) 70.71/24.09 , activate(n__a()) -> a() 70.71/24.09 , activate(n__e()) -> e() 70.71/24.09 , activate(n__i()) -> i() 70.71/24.09 , activate(n__o()) -> o() 70.71/24.09 , activate(n__u()) -> u() 70.71/24.09 , U31(tt()) -> tt() 70.71/24.09 , U42(tt()) -> tt() 70.71/24.09 , isNeList(n____(V1, V2)) -> 70.71/24.09 U41(isList(activate(V1)), activate(V2)) 70.71/24.09 , isNeList(n____(V1, V2)) -> 70.71/24.09 U51(isNeList(activate(V1)), activate(V2)) 70.71/24.09 , U51(tt(), V2) -> U52(isList(activate(V2))) 70.71/24.09 , U52(tt()) -> tt() 70.71/24.09 , U61(tt()) -> tt() 70.71/24.09 , U71(tt(), P) -> U72(isPal(activate(P))) 70.71/24.09 , U72(tt()) -> tt() 70.71/24.09 , isPal(V) -> U81(isNePal(activate(V))) 70.71/24.09 , isPal(n__nil()) -> tt() 70.71/24.09 , U81(tt()) -> tt() 70.71/24.09 , isQid(n__a()) -> tt() 70.71/24.09 , isQid(n__e()) -> tt() 70.71/24.09 , isQid(n__i()) -> tt() 70.71/24.09 , isQid(n__o()) -> tt() 70.71/24.09 , isQid(n__u()) -> tt() } 70.71/24.09 Obligation: 70.71/24.09 innermost runtime complexity 70.71/24.09 Answer: 70.71/24.09 YES(O(1),O(n^1)) 70.71/24.09 70.71/24.09 The weightgap principle applies (using the following nonconstant 70.71/24.09 growth matrix-interpretation) 70.71/24.09 70.71/24.09 The following argument positions are usable: 70.71/24.09 Uargs(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1}, 70.71/24.09 Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2}, 70.71/24.09 Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2}, 70.71/24.09 Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1}, 70.71/24.09 Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {1}, 70.71/24.09 Uargs(isNePal) = {1} 70.71/24.09 70.71/24.09 TcT has computed the following matrix interpretation satisfying 70.71/24.09 not(EDA) and not(IDA(1)). 70.71/24.09 70.71/24.09 [__](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.09 70.71/24.09 [nil] = [1] 70.71/24.09 70.71/24.09 [U11](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [tt] = [1] 70.71/24.09 70.71/24.09 [U21](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.09 70.71/24.09 [U22](x1) = [1] x1 + [3] 70.71/24.09 70.71/24.09 [isList](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [activate](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [U31](x1) = [1] x1 + [7] 70.71/24.09 70.71/24.09 [U41](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.09 70.71/24.09 [U42](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [isNeList](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [U51](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.09 70.71/24.09 [U52](x1) = [1] x1 + [1] 70.71/24.09 70.71/24.09 [U61](x1) = [1] x1 + [3] 70.71/24.09 70.71/24.09 [U71](x1, x2) = [1] x2 + [7] 70.71/24.09 70.71/24.09 [U72](x1) = [1] x1 + [3] 70.71/24.09 70.71/24.09 [isPal](x1) = [1] x1 + [4] 70.71/24.09 70.71/24.09 [U81](x1) = [1] x1 + [4] 70.71/24.09 70.71/24.09 [n__nil] = [1] 70.71/24.09 70.71/24.09 [n____](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.09 70.71/24.09 [isQid](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [isNePal](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [n__a] = [1] 70.71/24.09 70.71/24.09 [n__e] = [1] 70.71/24.09 70.71/24.09 [n__i] = [1] 70.71/24.09 70.71/24.09 [n__o] = [1] 70.71/24.09 70.71/24.09 [n__u] = [1] 70.71/24.09 70.71/24.09 [a] = [1] 70.71/24.09 70.71/24.09 [e] = [1] 70.71/24.09 70.71/24.09 [i] = [1] 70.71/24.09 70.71/24.09 [o] = [1] 70.71/24.09 70.71/24.09 [u] = [1] 70.71/24.09 70.71/24.09 The order satisfies the following ordering constraints: 70.71/24.09 70.71/24.09 [__(X1, X2)] = [1] X1 + [1] X2 + [0] 70.71/24.09 >= [1] X1 + [1] X2 + [0] 70.71/24.09 = [n____(X1, X2)] 70.71/24.09 70.71/24.09 [nil()] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [n__nil()] 70.71/24.09 70.71/24.09 [U11(tt())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [U21(tt(), V2)] = [1] V2 + [1] 70.71/24.09 ? [1] V2 + [3] 70.71/24.09 = [U22(isList(activate(V2)))] 70.71/24.09 70.71/24.09 [U22(tt())] = [4] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isList(V)] = [1] V + [0] 70.71/24.09 >= [1] V + [0] 70.71/24.09 = [U11(isNeList(activate(V)))] 70.71/24.09 70.71/24.09 [isList(n__nil())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isList(n____(V1, V2))] = [1] V2 + [1] V1 + [0] 70.71/24.09 >= [1] V2 + [1] V1 + [0] 70.71/24.09 = [U21(isList(activate(V1)), activate(V2))] 70.71/24.09 70.71/24.09 [activate(X)] = [1] X + [0] 70.71/24.09 >= [1] X + [0] 70.71/24.09 = [X] 70.71/24.09 70.71/24.09 [activate(n__nil())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [nil()] 70.71/24.09 70.71/24.09 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0] 70.71/24.09 >= [1] X1 + [1] X2 + [0] 70.71/24.09 = [__(X1, X2)] 70.71/24.09 70.71/24.09 [activate(n__a())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [a()] 70.71/24.09 70.71/24.09 [activate(n__e())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [e()] 70.71/24.09 70.71/24.09 [activate(n__i())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [i()] 70.71/24.09 70.71/24.09 [activate(n__o())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [o()] 70.71/24.09 70.71/24.09 [activate(n__u())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [u()] 70.71/24.09 70.71/24.09 [U31(tt())] = [8] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [U41(tt(), V2)] = [1] V2 + [1] 70.71/24.09 > [1] V2 + [0] 70.71/24.09 = [U42(isNeList(activate(V2)))] 70.71/24.09 70.71/24.09 [U42(tt())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isNeList(V)] = [1] V + [0] 70.71/24.09 ? [1] V + [7] 70.71/24.09 = [U31(isQid(activate(V)))] 70.71/24.09 70.71/24.09 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0] 70.71/24.09 >= [1] V2 + [1] V1 + [0] 70.71/24.09 = [U41(isList(activate(V1)), activate(V2))] 70.71/24.09 70.71/24.09 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0] 70.71/24.09 >= [1] V2 + [1] V1 + [0] 70.71/24.09 = [U51(isNeList(activate(V1)), activate(V2))] 70.71/24.09 70.71/24.09 [U51(tt(), V2)] = [1] V2 + [1] 70.71/24.09 >= [1] V2 + [1] 70.71/24.09 = [U52(isList(activate(V2)))] 70.71/24.09 70.71/24.09 [U52(tt())] = [2] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [U61(tt())] = [4] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [U71(tt(), P)] = [1] P + [7] 70.71/24.09 >= [1] P + [7] 70.71/24.09 = [U72(isPal(activate(P)))] 70.71/24.09 70.71/24.09 [U72(tt())] = [4] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isPal(V)] = [1] V + [4] 70.71/24.09 >= [1] V + [4] 70.71/24.09 = [U81(isNePal(activate(V)))] 70.71/24.09 70.71/24.09 [isPal(n__nil())] = [5] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [U81(tt())] = [5] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isQid(n__a())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isQid(n__e())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isQid(n__i())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isQid(n__o())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isQid(n__u())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isNePal(V)] = [1] V + [0] 70.71/24.09 ? [1] V + [3] 70.71/24.09 = [U61(isQid(activate(V)))] 70.71/24.09 70.71/24.09 [a()] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [n__a()] 70.71/24.09 70.71/24.09 [e()] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [n__e()] 70.71/24.09 70.71/24.09 [i()] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [n__i()] 70.71/24.09 70.71/24.09 [o()] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [n__o()] 70.71/24.09 70.71/24.09 [u()] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [n__u()] 70.71/24.09 70.71/24.09 70.71/24.09 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.71/24.09 70.71/24.09 We are left with following problem, upon which TcT provides the 70.71/24.09 certificate YES(O(1),O(n^1)). 70.71/24.09 70.71/24.09 Strict Trs: 70.71/24.09 { nil() -> n__nil() 70.71/24.09 , U21(tt(), V2) -> U22(isList(activate(V2))) 70.71/24.09 , isNeList(V) -> U31(isQid(activate(V))) 70.71/24.09 , isNePal(V) -> U61(isQid(activate(V))) 70.71/24.09 , a() -> n__a() 70.71/24.09 , e() -> n__e() 70.71/24.09 , i() -> n__i() 70.71/24.09 , o() -> n__o() 70.71/24.09 , u() -> n__u() } 70.71/24.09 Weak Trs: 70.71/24.09 { __(X1, X2) -> n____(X1, X2) 70.71/24.09 , U11(tt()) -> tt() 70.71/24.09 , U22(tt()) -> tt() 70.71/24.09 , isList(V) -> U11(isNeList(activate(V))) 70.71/24.09 , isList(n__nil()) -> tt() 70.71/24.09 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 70.71/24.09 , activate(X) -> X 70.71/24.09 , activate(n__nil()) -> nil() 70.71/24.09 , activate(n____(X1, X2)) -> __(X1, X2) 70.71/24.09 , activate(n__a()) -> a() 70.71/24.09 , activate(n__e()) -> e() 70.71/24.09 , activate(n__i()) -> i() 70.71/24.09 , activate(n__o()) -> o() 70.71/24.09 , activate(n__u()) -> u() 70.71/24.09 , U31(tt()) -> tt() 70.71/24.09 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 70.71/24.09 , U42(tt()) -> tt() 70.71/24.09 , isNeList(n____(V1, V2)) -> 70.71/24.09 U41(isList(activate(V1)), activate(V2)) 70.71/24.09 , isNeList(n____(V1, V2)) -> 70.71/24.09 U51(isNeList(activate(V1)), activate(V2)) 70.71/24.09 , U51(tt(), V2) -> U52(isList(activate(V2))) 70.71/24.09 , U52(tt()) -> tt() 70.71/24.09 , U61(tt()) -> tt() 70.71/24.09 , U71(tt(), P) -> U72(isPal(activate(P))) 70.71/24.09 , U72(tt()) -> tt() 70.71/24.09 , isPal(V) -> U81(isNePal(activate(V))) 70.71/24.09 , isPal(n__nil()) -> tt() 70.71/24.09 , U81(tt()) -> tt() 70.71/24.09 , isQid(n__a()) -> tt() 70.71/24.09 , isQid(n__e()) -> tt() 70.71/24.09 , isQid(n__i()) -> tt() 70.71/24.09 , isQid(n__o()) -> tt() 70.71/24.09 , isQid(n__u()) -> tt() } 70.71/24.09 Obligation: 70.71/24.09 innermost runtime complexity 70.71/24.09 Answer: 70.71/24.09 YES(O(1),O(n^1)) 70.71/24.09 70.71/24.09 The weightgap principle applies (using the following nonconstant 70.71/24.09 growth matrix-interpretation) 70.71/24.09 70.71/24.09 The following argument positions are usable: 70.71/24.09 Uargs(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1}, 70.71/24.09 Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2}, 70.71/24.09 Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2}, 70.71/24.09 Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1}, 70.71/24.09 Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {1}, 70.71/24.09 Uargs(isNePal) = {1} 70.71/24.09 70.71/24.09 TcT has computed the following matrix interpretation satisfying 70.71/24.09 not(EDA) and not(IDA(1)). 70.71/24.09 70.71/24.09 [__](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.09 70.71/24.09 [nil] = [1] 70.71/24.09 70.71/24.09 [U11](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [tt] = [1] 70.71/24.09 70.71/24.09 [U21](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.09 70.71/24.09 [U22](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [isList](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [activate](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [U31](x1) = [1] x1 + [7] 70.71/24.09 70.71/24.09 [U41](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.09 70.71/24.09 [U42](x1) = [1] x1 + [1] 70.71/24.09 70.71/24.09 [isNeList](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [U51](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.09 70.71/24.09 [U52](x1) = [1] x1 + [1] 70.71/24.09 70.71/24.09 [U61](x1) = [1] x1 + [7] 70.71/24.09 70.71/24.09 [U71](x1, x2) = [1] x2 + [7] 70.71/24.09 70.71/24.09 [U72](x1) = [1] x1 + [3] 70.71/24.09 70.71/24.09 [isPal](x1) = [1] x1 + [4] 70.71/24.09 70.71/24.09 [U81](x1) = [1] x1 + [4] 70.71/24.09 70.71/24.09 [n__nil] = [1] 70.71/24.09 70.71/24.09 [n____](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.09 70.71/24.09 [isQid](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [isNePal](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [n__a] = [1] 70.71/24.09 70.71/24.09 [n__e] = [1] 70.71/24.09 70.71/24.09 [n__i] = [1] 70.71/24.09 70.71/24.09 [n__o] = [1] 70.71/24.09 70.71/24.09 [n__u] = [1] 70.71/24.09 70.71/24.09 [a] = [1] 70.71/24.09 70.71/24.09 [e] = [1] 70.71/24.09 70.71/24.09 [i] = [1] 70.71/24.09 70.71/24.09 [o] = [1] 70.71/24.09 70.71/24.09 [u] = [1] 70.71/24.09 70.71/24.09 The order satisfies the following ordering constraints: 70.71/24.09 70.71/24.09 [__(X1, X2)] = [1] X1 + [1] X2 + [0] 70.71/24.09 >= [1] X1 + [1] X2 + [0] 70.71/24.09 = [n____(X1, X2)] 70.71/24.09 70.71/24.09 [nil()] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [n__nil()] 70.71/24.09 70.71/24.09 [U11(tt())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [U21(tt(), V2)] = [1] V2 + [1] 70.71/24.09 > [1] V2 + [0] 70.71/24.09 = [U22(isList(activate(V2)))] 70.71/24.09 70.71/24.09 [U22(tt())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isList(V)] = [1] V + [0] 70.71/24.09 >= [1] V + [0] 70.71/24.09 = [U11(isNeList(activate(V)))] 70.71/24.09 70.71/24.09 [isList(n__nil())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isList(n____(V1, V2))] = [1] V2 + [1] V1 + [0] 70.71/24.09 >= [1] V2 + [1] V1 + [0] 70.71/24.09 = [U21(isList(activate(V1)), activate(V2))] 70.71/24.09 70.71/24.09 [activate(X)] = [1] X + [0] 70.71/24.09 >= [1] X + [0] 70.71/24.09 = [X] 70.71/24.09 70.71/24.09 [activate(n__nil())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [nil()] 70.71/24.09 70.71/24.09 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0] 70.71/24.09 >= [1] X1 + [1] X2 + [0] 70.71/24.09 = [__(X1, X2)] 70.71/24.09 70.71/24.09 [activate(n__a())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [a()] 70.71/24.09 70.71/24.09 [activate(n__e())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [e()] 70.71/24.09 70.71/24.09 [activate(n__i())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [i()] 70.71/24.09 70.71/24.09 [activate(n__o())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [o()] 70.71/24.09 70.71/24.09 [activate(n__u())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [u()] 70.71/24.09 70.71/24.09 [U31(tt())] = [8] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [U41(tt(), V2)] = [1] V2 + [1] 70.71/24.09 >= [1] V2 + [1] 70.71/24.09 = [U42(isNeList(activate(V2)))] 70.71/24.09 70.71/24.09 [U42(tt())] = [2] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isNeList(V)] = [1] V + [0] 70.71/24.09 ? [1] V + [7] 70.71/24.09 = [U31(isQid(activate(V)))] 70.71/24.09 70.71/24.09 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0] 70.71/24.09 >= [1] V2 + [1] V1 + [0] 70.71/24.09 = [U41(isList(activate(V1)), activate(V2))] 70.71/24.09 70.71/24.09 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0] 70.71/24.09 >= [1] V2 + [1] V1 + [0] 70.71/24.09 = [U51(isNeList(activate(V1)), activate(V2))] 70.71/24.09 70.71/24.09 [U51(tt(), V2)] = [1] V2 + [1] 70.71/24.09 >= [1] V2 + [1] 70.71/24.09 = [U52(isList(activate(V2)))] 70.71/24.09 70.71/24.09 [U52(tt())] = [2] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [U61(tt())] = [8] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [U71(tt(), P)] = [1] P + [7] 70.71/24.09 >= [1] P + [7] 70.71/24.09 = [U72(isPal(activate(P)))] 70.71/24.09 70.71/24.09 [U72(tt())] = [4] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isPal(V)] = [1] V + [4] 70.71/24.09 >= [1] V + [4] 70.71/24.09 = [U81(isNePal(activate(V)))] 70.71/24.09 70.71/24.09 [isPal(n__nil())] = [5] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [U81(tt())] = [5] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isQid(n__a())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isQid(n__e())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isQid(n__i())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isQid(n__o())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isQid(n__u())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isNePal(V)] = [1] V + [0] 70.71/24.09 ? [1] V + [7] 70.71/24.09 = [U61(isQid(activate(V)))] 70.71/24.09 70.71/24.09 [a()] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [n__a()] 70.71/24.09 70.71/24.09 [e()] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [n__e()] 70.71/24.09 70.71/24.09 [i()] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [n__i()] 70.71/24.09 70.71/24.09 [o()] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [n__o()] 70.71/24.09 70.71/24.09 [u()] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [n__u()] 70.71/24.09 70.71/24.09 70.71/24.09 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.71/24.09 70.71/24.09 We are left with following problem, upon which TcT provides the 70.71/24.09 certificate YES(O(1),O(n^1)). 70.71/24.09 70.71/24.09 Strict Trs: 70.71/24.09 { nil() -> n__nil() 70.71/24.09 , isNeList(V) -> U31(isQid(activate(V))) 70.71/24.09 , isNePal(V) -> U61(isQid(activate(V))) 70.71/24.09 , a() -> n__a() 70.71/24.09 , e() -> n__e() 70.71/24.09 , i() -> n__i() 70.71/24.09 , o() -> n__o() 70.71/24.09 , u() -> n__u() } 70.71/24.09 Weak Trs: 70.71/24.09 { __(X1, X2) -> n____(X1, X2) 70.71/24.09 , U11(tt()) -> tt() 70.71/24.09 , U21(tt(), V2) -> U22(isList(activate(V2))) 70.71/24.09 , U22(tt()) -> tt() 70.71/24.09 , isList(V) -> U11(isNeList(activate(V))) 70.71/24.09 , isList(n__nil()) -> tt() 70.71/24.09 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 70.71/24.09 , activate(X) -> X 70.71/24.09 , activate(n__nil()) -> nil() 70.71/24.09 , activate(n____(X1, X2)) -> __(X1, X2) 70.71/24.09 , activate(n__a()) -> a() 70.71/24.09 , activate(n__e()) -> e() 70.71/24.09 , activate(n__i()) -> i() 70.71/24.09 , activate(n__o()) -> o() 70.71/24.09 , activate(n__u()) -> u() 70.71/24.09 , U31(tt()) -> tt() 70.71/24.09 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 70.71/24.09 , U42(tt()) -> tt() 70.71/24.09 , isNeList(n____(V1, V2)) -> 70.71/24.09 U41(isList(activate(V1)), activate(V2)) 70.71/24.09 , isNeList(n____(V1, V2)) -> 70.71/24.09 U51(isNeList(activate(V1)), activate(V2)) 70.71/24.09 , U51(tt(), V2) -> U52(isList(activate(V2))) 70.71/24.09 , U52(tt()) -> tt() 70.71/24.09 , U61(tt()) -> tt() 70.71/24.09 , U71(tt(), P) -> U72(isPal(activate(P))) 70.71/24.09 , U72(tt()) -> tt() 70.71/24.09 , isPal(V) -> U81(isNePal(activate(V))) 70.71/24.09 , isPal(n__nil()) -> tt() 70.71/24.09 , U81(tt()) -> tt() 70.71/24.09 , isQid(n__a()) -> tt() 70.71/24.09 , isQid(n__e()) -> tt() 70.71/24.09 , isQid(n__i()) -> tt() 70.71/24.09 , isQid(n__o()) -> tt() 70.71/24.09 , isQid(n__u()) -> tt() } 70.71/24.09 Obligation: 70.71/24.09 innermost runtime complexity 70.71/24.09 Answer: 70.71/24.09 YES(O(1),O(n^1)) 70.71/24.09 70.71/24.09 The weightgap principle applies (using the following nonconstant 70.71/24.09 growth matrix-interpretation) 70.71/24.09 70.71/24.09 The following argument positions are usable: 70.71/24.09 Uargs(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1}, 70.71/24.09 Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2}, 70.71/24.09 Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2}, 70.71/24.09 Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1}, 70.71/24.09 Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {1}, 70.71/24.09 Uargs(isNePal) = {1} 70.71/24.09 70.71/24.09 TcT has computed the following matrix interpretation satisfying 70.71/24.09 not(EDA) and not(IDA(1)). 70.71/24.09 70.71/24.09 [__](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.09 70.71/24.09 [nil] = [0] 70.71/24.09 70.71/24.09 [U11](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [tt] = [1] 70.71/24.09 70.71/24.09 [U21](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.09 70.71/24.09 [U22](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [isList](x1) = [1] x1 + [1] 70.71/24.09 70.71/24.09 [activate](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [U31](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [U41](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.09 70.71/24.09 [U42](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [isNeList](x1) = [1] x1 + [1] 70.71/24.09 70.71/24.09 [U51](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.09 70.71/24.09 [U52](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [U61](x1) = [1] x1 + [7] 70.71/24.09 70.71/24.09 [U71](x1, x2) = [1] x2 + [7] 70.71/24.09 70.71/24.09 [U72](x1) = [1] x1 + [3] 70.71/24.09 70.71/24.09 [isPal](x1) = [1] x1 + [4] 70.71/24.09 70.71/24.09 [U81](x1) = [1] x1 + [4] 70.71/24.09 70.71/24.09 [n__nil] = [0] 70.71/24.09 70.71/24.09 [n____](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.09 70.71/24.09 [isQid](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [isNePal](x1) = [1] x1 + [0] 70.71/24.09 70.71/24.09 [n__a] = [1] 70.71/24.09 70.71/24.09 [n__e] = [1] 70.71/24.09 70.71/24.09 [n__i] = [1] 70.71/24.09 70.71/24.09 [n__o] = [1] 70.71/24.09 70.71/24.09 [n__u] = [1] 70.71/24.09 70.71/24.09 [a] = [1] 70.71/24.09 70.71/24.09 [e] = [1] 70.71/24.09 70.71/24.09 [i] = [1] 70.71/24.09 70.71/24.09 [o] = [1] 70.71/24.09 70.71/24.09 [u] = [1] 70.71/24.09 70.71/24.09 The order satisfies the following ordering constraints: 70.71/24.09 70.71/24.09 [__(X1, X2)] = [1] X1 + [1] X2 + [0] 70.71/24.09 >= [1] X1 + [1] X2 + [0] 70.71/24.09 = [n____(X1, X2)] 70.71/24.09 70.71/24.09 [nil()] = [0] 70.71/24.09 >= [0] 70.71/24.09 = [n__nil()] 70.71/24.09 70.71/24.09 [U11(tt())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [U21(tt(), V2)] = [1] V2 + [1] 70.71/24.09 >= [1] V2 + [1] 70.71/24.09 = [U22(isList(activate(V2)))] 70.71/24.09 70.71/24.09 [U22(tt())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isList(V)] = [1] V + [1] 70.71/24.09 >= [1] V + [1] 70.71/24.09 = [U11(isNeList(activate(V)))] 70.71/24.09 70.71/24.09 [isList(n__nil())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isList(n____(V1, V2))] = [1] V2 + [1] V1 + [1] 70.71/24.09 >= [1] V2 + [1] V1 + [1] 70.71/24.09 = [U21(isList(activate(V1)), activate(V2))] 70.71/24.09 70.71/24.09 [activate(X)] = [1] X + [0] 70.71/24.09 >= [1] X + [0] 70.71/24.09 = [X] 70.71/24.09 70.71/24.09 [activate(n__nil())] = [0] 70.71/24.09 >= [0] 70.71/24.09 = [nil()] 70.71/24.09 70.71/24.09 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0] 70.71/24.09 >= [1] X1 + [1] X2 + [0] 70.71/24.09 = [__(X1, X2)] 70.71/24.09 70.71/24.09 [activate(n__a())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [a()] 70.71/24.09 70.71/24.09 [activate(n__e())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [e()] 70.71/24.09 70.71/24.09 [activate(n__i())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [i()] 70.71/24.09 70.71/24.09 [activate(n__o())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [o()] 70.71/24.09 70.71/24.09 [activate(n__u())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [u()] 70.71/24.09 70.71/24.09 [U31(tt())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [U41(tt(), V2)] = [1] V2 + [1] 70.71/24.09 >= [1] V2 + [1] 70.71/24.09 = [U42(isNeList(activate(V2)))] 70.71/24.09 70.71/24.09 [U42(tt())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isNeList(V)] = [1] V + [1] 70.71/24.09 > [1] V + [0] 70.71/24.09 = [U31(isQid(activate(V)))] 70.71/24.09 70.71/24.09 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [1] 70.71/24.09 >= [1] V2 + [1] V1 + [1] 70.71/24.09 = [U41(isList(activate(V1)), activate(V2))] 70.71/24.09 70.71/24.09 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [1] 70.71/24.09 >= [1] V2 + [1] V1 + [1] 70.71/24.09 = [U51(isNeList(activate(V1)), activate(V2))] 70.71/24.09 70.71/24.09 [U51(tt(), V2)] = [1] V2 + [1] 70.71/24.09 >= [1] V2 + [1] 70.71/24.09 = [U52(isList(activate(V2)))] 70.71/24.09 70.71/24.09 [U52(tt())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [U61(tt())] = [8] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [U71(tt(), P)] = [1] P + [7] 70.71/24.09 >= [1] P + [7] 70.71/24.09 = [U72(isPal(activate(P)))] 70.71/24.09 70.71/24.09 [U72(tt())] = [4] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isPal(V)] = [1] V + [4] 70.71/24.09 >= [1] V + [4] 70.71/24.09 = [U81(isNePal(activate(V)))] 70.71/24.09 70.71/24.09 [isPal(n__nil())] = [4] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [U81(tt())] = [5] 70.71/24.09 > [1] 70.71/24.09 = [tt()] 70.71/24.09 70.71/24.09 [isQid(n__a())] = [1] 70.71/24.09 >= [1] 70.71/24.09 = [tt()] 70.71/24.10 70.71/24.10 [isQid(n__e())] = [1] 70.71/24.10 >= [1] 70.71/24.10 = [tt()] 70.71/24.10 70.71/24.10 [isQid(n__i())] = [1] 70.71/24.10 >= [1] 70.71/24.10 = [tt()] 70.71/24.10 70.71/24.10 [isQid(n__o())] = [1] 70.71/24.10 >= [1] 70.71/24.10 = [tt()] 70.71/24.10 70.71/24.10 [isQid(n__u())] = [1] 70.71/24.10 >= [1] 70.71/24.10 = [tt()] 70.71/24.10 70.71/24.10 [isNePal(V)] = [1] V + [0] 70.71/24.10 ? [1] V + [7] 70.71/24.10 = [U61(isQid(activate(V)))] 70.71/24.10 70.71/24.10 [a()] = [1] 70.71/24.10 >= [1] 70.71/24.10 = [n__a()] 70.71/24.10 70.71/24.10 [e()] = [1] 70.71/24.10 >= [1] 70.71/24.10 = [n__e()] 70.71/24.10 70.71/24.10 [i()] = [1] 70.71/24.10 >= [1] 70.71/24.10 = [n__i()] 70.71/24.10 70.71/24.10 [o()] = [1] 70.71/24.10 >= [1] 70.71/24.10 = [n__o()] 70.71/24.10 70.71/24.10 [u()] = [1] 70.71/24.10 >= [1] 70.71/24.10 = [n__u()] 70.71/24.10 70.71/24.10 70.71/24.10 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.71/24.10 70.71/24.10 We are left with following problem, upon which TcT provides the 70.71/24.10 certificate YES(O(1),O(n^1)). 70.71/24.10 70.71/24.10 Strict Trs: 70.71/24.10 { nil() -> n__nil() 70.71/24.10 , isNePal(V) -> U61(isQid(activate(V))) 70.71/24.10 , a() -> n__a() 70.71/24.10 , e() -> n__e() 70.71/24.10 , i() -> n__i() 70.71/24.10 , o() -> n__o() 70.71/24.10 , u() -> n__u() } 70.71/24.10 Weak Trs: 70.71/24.10 { __(X1, X2) -> n____(X1, X2) 70.71/24.10 , U11(tt()) -> tt() 70.71/24.10 , U21(tt(), V2) -> U22(isList(activate(V2))) 70.71/24.10 , U22(tt()) -> tt() 70.71/24.10 , isList(V) -> U11(isNeList(activate(V))) 70.71/24.10 , isList(n__nil()) -> tt() 70.71/24.10 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 70.71/24.10 , activate(X) -> X 70.71/24.10 , activate(n__nil()) -> nil() 70.71/24.10 , activate(n____(X1, X2)) -> __(X1, X2) 70.71/24.10 , activate(n__a()) -> a() 70.71/24.10 , activate(n__e()) -> e() 70.71/24.10 , activate(n__i()) -> i() 70.71/24.10 , activate(n__o()) -> o() 70.71/24.10 , activate(n__u()) -> u() 70.71/24.10 , U31(tt()) -> tt() 70.71/24.10 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 70.71/24.10 , U42(tt()) -> tt() 70.71/24.10 , isNeList(V) -> U31(isQid(activate(V))) 70.71/24.10 , isNeList(n____(V1, V2)) -> 70.71/24.10 U41(isList(activate(V1)), activate(V2)) 70.71/24.10 , isNeList(n____(V1, V2)) -> 70.71/24.10 U51(isNeList(activate(V1)), activate(V2)) 70.71/24.10 , U51(tt(), V2) -> U52(isList(activate(V2))) 70.71/24.10 , U52(tt()) -> tt() 70.71/24.10 , U61(tt()) -> tt() 70.71/24.10 , U71(tt(), P) -> U72(isPal(activate(P))) 70.71/24.10 , U72(tt()) -> tt() 70.71/24.10 , isPal(V) -> U81(isNePal(activate(V))) 70.71/24.10 , isPal(n__nil()) -> tt() 70.71/24.10 , U81(tt()) -> tt() 70.71/24.10 , isQid(n__a()) -> tt() 70.71/24.10 , isQid(n__e()) -> tt() 70.71/24.10 , isQid(n__i()) -> tt() 70.71/24.10 , isQid(n__o()) -> tt() 70.71/24.10 , isQid(n__u()) -> tt() } 70.71/24.10 Obligation: 70.71/24.10 innermost runtime complexity 70.71/24.10 Answer: 70.71/24.10 YES(O(1),O(n^1)) 70.71/24.10 70.71/24.10 The weightgap principle applies (using the following nonconstant 70.71/24.10 growth matrix-interpretation) 70.71/24.10 70.71/24.10 The following argument positions are usable: 70.71/24.10 Uargs(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1}, 70.71/24.10 Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2}, 70.71/24.10 Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2}, 70.71/24.10 Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1}, 70.71/24.10 Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {1}, 70.71/24.10 Uargs(isNePal) = {1} 70.71/24.10 70.71/24.10 TcT has computed the following matrix interpretation satisfying 70.71/24.10 not(EDA) and not(IDA(1)). 70.71/24.10 70.71/24.10 [__](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.10 70.71/24.10 [nil] = [0] 70.71/24.10 70.71/24.10 [U11](x1) = [1] x1 + [0] 70.71/24.10 70.71/24.10 [tt] = [0] 70.71/24.10 70.71/24.10 [U21](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.10 70.71/24.10 [U22](x1) = [1] x1 + [0] 70.71/24.10 70.71/24.10 [isList](x1) = [1] x1 + [0] 70.71/24.10 70.71/24.10 [activate](x1) = [1] x1 + [0] 70.71/24.10 70.71/24.10 [U31](x1) = [1] x1 + [0] 70.71/24.10 70.71/24.10 [U41](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.10 70.71/24.10 [U42](x1) = [1] x1 + [0] 70.71/24.10 70.71/24.10 [isNeList](x1) = [1] x1 + [0] 70.71/24.10 70.71/24.10 [U51](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.10 70.71/24.10 [U52](x1) = [1] x1 + [0] 70.71/24.10 70.71/24.10 [U61](x1) = [1] x1 + [0] 70.71/24.10 70.71/24.10 [U71](x1, x2) = [1] x1 + [1] x2 + [7] 70.71/24.10 70.71/24.10 [U72](x1) = [1] x1 + [1] 70.71/24.10 70.71/24.10 [isPal](x1) = [1] x1 + [5] 70.71/24.10 70.71/24.10 [U81](x1) = [1] x1 + [4] 70.71/24.10 70.71/24.10 [n__nil] = [0] 70.71/24.10 70.71/24.10 [n____](x1, x2) = [1] x1 + [1] x2 + [0] 70.71/24.10 70.71/24.10 [isQid](x1) = [1] x1 + [0] 70.71/24.10 70.71/24.10 [isNePal](x1) = [1] x1 + [1] 70.71/24.10 70.71/24.10 [n__a] = [0] 70.71/24.10 70.71/24.10 [n__e] = [0] 70.71/24.10 70.71/24.10 [n__i] = [0] 70.71/24.10 70.71/24.10 [n__o] = [0] 70.71/24.10 70.71/24.10 [n__u] = [0] 70.71/24.10 70.71/24.10 [a] = [0] 70.71/24.10 70.71/24.10 [e] = [0] 70.71/24.10 70.71/24.10 [i] = [0] 70.71/24.10 70.71/24.10 [o] = [0] 70.71/24.10 70.71/24.10 [u] = [0] 70.71/24.10 70.71/24.10 The order satisfies the following ordering constraints: 70.71/24.10 70.71/24.10 [__(X1, X2)] = [1] X1 + [1] X2 + [0] 70.96/24.11 >= [1] X1 + [1] X2 + [0] 70.96/24.11 = [n____(X1, X2)] 70.96/24.11 70.96/24.11 [nil()] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [n__nil()] 70.96/24.11 70.96/24.11 [U11(tt())] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [U21(tt(), V2)] = [1] V2 + [0] 70.96/24.11 >= [1] V2 + [0] 70.96/24.11 = [U22(isList(activate(V2)))] 70.96/24.11 70.96/24.11 [U22(tt())] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isList(V)] = [1] V + [0] 70.96/24.11 >= [1] V + [0] 70.96/24.11 = [U11(isNeList(activate(V)))] 70.96/24.11 70.96/24.11 [isList(n__nil())] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isList(n____(V1, V2))] = [1] V2 + [1] V1 + [0] 70.96/24.11 >= [1] V2 + [1] V1 + [0] 70.96/24.11 = [U21(isList(activate(V1)), activate(V2))] 70.96/24.11 70.96/24.11 [activate(X)] = [1] X + [0] 70.96/24.11 >= [1] X + [0] 70.96/24.11 = [X] 70.96/24.11 70.96/24.11 [activate(n__nil())] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [nil()] 70.96/24.11 70.96/24.11 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [0] 70.96/24.11 >= [1] X1 + [1] X2 + [0] 70.96/24.11 = [__(X1, X2)] 70.96/24.11 70.96/24.11 [activate(n__a())] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [a()] 70.96/24.11 70.96/24.11 [activate(n__e())] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [e()] 70.96/24.11 70.96/24.11 [activate(n__i())] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [i()] 70.96/24.11 70.96/24.11 [activate(n__o())] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [o()] 70.96/24.11 70.96/24.11 [activate(n__u())] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [u()] 70.96/24.11 70.96/24.11 [U31(tt())] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [U41(tt(), V2)] = [1] V2 + [0] 70.96/24.11 >= [1] V2 + [0] 70.96/24.11 = [U42(isNeList(activate(V2)))] 70.96/24.11 70.96/24.11 [U42(tt())] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isNeList(V)] = [1] V + [0] 70.96/24.11 >= [1] V + [0] 70.96/24.11 = [U31(isQid(activate(V)))] 70.96/24.11 70.96/24.11 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0] 70.96/24.11 >= [1] V2 + [1] V1 + [0] 70.96/24.11 = [U41(isList(activate(V1)), activate(V2))] 70.96/24.11 70.96/24.11 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [0] 70.96/24.11 >= [1] V2 + [1] V1 + [0] 70.96/24.11 = [U51(isNeList(activate(V1)), activate(V2))] 70.96/24.11 70.96/24.11 [U51(tt(), V2)] = [1] V2 + [0] 70.96/24.11 >= [1] V2 + [0] 70.96/24.11 = [U52(isList(activate(V2)))] 70.96/24.11 70.96/24.11 [U52(tt())] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [U61(tt())] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [U71(tt(), P)] = [1] P + [7] 70.96/24.11 > [1] P + [6] 70.96/24.11 = [U72(isPal(activate(P)))] 70.96/24.11 70.96/24.11 [U72(tt())] = [1] 70.96/24.11 > [0] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isPal(V)] = [1] V + [5] 70.96/24.11 >= [1] V + [5] 70.96/24.11 = [U81(isNePal(activate(V)))] 70.96/24.11 70.96/24.11 [isPal(n__nil())] = [5] 70.96/24.11 > [0] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [U81(tt())] = [4] 70.96/24.11 > [0] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isQid(n__a())] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isQid(n__e())] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isQid(n__i())] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isQid(n__o())] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isQid(n__u())] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isNePal(V)] = [1] V + [1] 70.96/24.11 > [1] V + [0] 70.96/24.11 = [U61(isQid(activate(V)))] 70.96/24.11 70.96/24.11 [a()] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [n__a()] 70.96/24.11 70.96/24.11 [e()] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [n__e()] 70.96/24.11 70.96/24.11 [i()] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [n__i()] 70.96/24.11 70.96/24.11 [o()] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [n__o()] 70.96/24.11 70.96/24.11 [u()] = [0] 70.96/24.11 >= [0] 70.96/24.11 = [n__u()] 70.96/24.11 70.96/24.11 70.96/24.11 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.96/24.11 70.96/24.11 We are left with following problem, upon which TcT provides the 70.96/24.11 certificate YES(O(1),O(n^1)). 70.96/24.11 70.96/24.11 Strict Trs: 70.96/24.11 { nil() -> n__nil() 70.96/24.11 , a() -> n__a() 70.96/24.11 , e() -> n__e() 70.96/24.11 , i() -> n__i() 70.96/24.11 , o() -> n__o() 70.96/24.11 , u() -> n__u() } 70.96/24.11 Weak Trs: 70.96/24.11 { __(X1, X2) -> n____(X1, X2) 70.96/24.11 , U11(tt()) -> tt() 70.96/24.11 , U21(tt(), V2) -> U22(isList(activate(V2))) 70.96/24.11 , U22(tt()) -> tt() 70.96/24.11 , isList(V) -> U11(isNeList(activate(V))) 70.96/24.11 , isList(n__nil()) -> tt() 70.96/24.11 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 70.96/24.11 , activate(X) -> X 70.96/24.11 , activate(n__nil()) -> nil() 70.96/24.11 , activate(n____(X1, X2)) -> __(X1, X2) 70.96/24.11 , activate(n__a()) -> a() 70.96/24.11 , activate(n__e()) -> e() 70.96/24.11 , activate(n__i()) -> i() 70.96/24.11 , activate(n__o()) -> o() 70.96/24.11 , activate(n__u()) -> u() 70.96/24.11 , U31(tt()) -> tt() 70.96/24.11 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 70.96/24.11 , U42(tt()) -> tt() 70.96/24.11 , isNeList(V) -> U31(isQid(activate(V))) 70.96/24.11 , isNeList(n____(V1, V2)) -> 70.96/24.11 U41(isList(activate(V1)), activate(V2)) 70.96/24.11 , isNeList(n____(V1, V2)) -> 70.96/24.11 U51(isNeList(activate(V1)), activate(V2)) 70.96/24.11 , U51(tt(), V2) -> U52(isList(activate(V2))) 70.96/24.11 , U52(tt()) -> tt() 70.96/24.11 , U61(tt()) -> tt() 70.96/24.11 , U71(tt(), P) -> U72(isPal(activate(P))) 70.96/24.11 , U72(tt()) -> tt() 70.96/24.11 , isPal(V) -> U81(isNePal(activate(V))) 70.96/24.11 , isPal(n__nil()) -> tt() 70.96/24.11 , U81(tt()) -> tt() 70.96/24.11 , isQid(n__a()) -> tt() 70.96/24.11 , isQid(n__e()) -> tt() 70.96/24.11 , isQid(n__i()) -> tt() 70.96/24.11 , isQid(n__o()) -> tt() 70.96/24.11 , isQid(n__u()) -> tt() 70.96/24.11 , isNePal(V) -> U61(isQid(activate(V))) } 70.96/24.11 Obligation: 70.96/24.11 innermost runtime complexity 70.96/24.11 Answer: 70.96/24.11 YES(O(1),O(n^1)) 70.96/24.11 70.96/24.11 The weightgap principle applies (using the following nonconstant 70.96/24.11 growth matrix-interpretation) 70.96/24.11 70.96/24.11 The following argument positions are usable: 70.96/24.11 Uargs(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1}, 70.96/24.11 Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2}, 70.96/24.11 Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2}, 70.96/24.11 Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1}, 70.96/24.11 Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {1}, 70.96/24.11 Uargs(isNePal) = {1} 70.96/24.11 70.96/24.11 TcT has computed the following matrix interpretation satisfying 70.96/24.11 not(EDA) and not(IDA(1)). 70.96/24.11 70.96/24.11 [__](x1, x2) = [1] x1 + [1] x2 + [7] 70.96/24.11 70.96/24.11 [nil] = [1] 70.96/24.11 70.96/24.11 [U11](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [tt] = [4] 70.96/24.11 70.96/24.11 [U21](x1, x2) = [1] x1 + [1] x2 + [4] 70.96/24.11 70.96/24.11 [U22](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [isList](x1) = [1] x1 + [7] 70.96/24.11 70.96/24.11 [activate](x1) = [1] x1 + [1] 70.96/24.11 70.96/24.11 [U31](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [U41](x1, x2) = [1] x1 + [1] x2 + [1] 70.96/24.11 70.96/24.11 [U42](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [isNeList](x1) = [1] x1 + [4] 70.96/24.11 70.96/24.11 [U51](x1, x2) = [1] x1 + [1] x2 + [4] 70.96/24.11 70.96/24.11 [U52](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [U61](x1) = [1] x1 + [1] 70.96/24.11 70.96/24.11 [U71](x1, x2) = [1] x2 + [7] 70.96/24.11 70.96/24.11 [U72](x1) = [1] x1 + [1] 70.96/24.11 70.96/24.11 [isPal](x1) = [1] x1 + [5] 70.96/24.11 70.96/24.11 [U81](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [n__nil] = [0] 70.96/24.11 70.96/24.11 [n____](x1, x2) = [1] x1 + [1] x2 + [7] 70.96/24.11 70.96/24.11 [isQid](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [isNePal](x1) = [1] x1 + [4] 70.96/24.11 70.96/24.11 [n__a] = [4] 70.96/24.11 70.96/24.11 [n__e] = [4] 70.96/24.11 70.96/24.11 [n__i] = [4] 70.96/24.11 70.96/24.11 [n__o] = [4] 70.96/24.11 70.96/24.11 [n__u] = [5] 70.96/24.11 70.96/24.11 [a] = [3] 70.96/24.11 70.96/24.11 [e] = [3] 70.96/24.11 70.96/24.11 [i] = [3] 70.96/24.11 70.96/24.11 [o] = [3] 70.96/24.11 70.96/24.11 [u] = [6] 70.96/24.11 70.96/24.11 The order satisfies the following ordering constraints: 70.96/24.11 70.96/24.11 [__(X1, X2)] = [1] X1 + [1] X2 + [7] 70.96/24.11 >= [1] X1 + [1] X2 + [7] 70.96/24.11 = [n____(X1, X2)] 70.96/24.11 70.96/24.11 [nil()] = [1] 70.96/24.11 > [0] 70.96/24.11 = [n__nil()] 70.96/24.11 70.96/24.11 [U11(tt())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [U21(tt(), V2)] = [1] V2 + [8] 70.96/24.11 >= [1] V2 + [8] 70.96/24.11 = [U22(isList(activate(V2)))] 70.96/24.11 70.96/24.11 [U22(tt())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isList(V)] = [1] V + [7] 70.96/24.11 > [1] V + [5] 70.96/24.11 = [U11(isNeList(activate(V)))] 70.96/24.11 70.96/24.11 [isList(n__nil())] = [7] 70.96/24.11 > [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isList(n____(V1, V2))] = [1] V2 + [1] V1 + [14] 70.96/24.11 > [1] V2 + [1] V1 + [13] 70.96/24.11 = [U21(isList(activate(V1)), activate(V2))] 70.96/24.11 70.96/24.11 [activate(X)] = [1] X + [1] 70.96/24.11 > [1] X + [0] 70.96/24.11 = [X] 70.96/24.11 70.96/24.11 [activate(n__nil())] = [1] 70.96/24.11 >= [1] 70.96/24.11 = [nil()] 70.96/24.11 70.96/24.11 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [8] 70.96/24.11 > [1] X1 + [1] X2 + [7] 70.96/24.11 = [__(X1, X2)] 70.96/24.11 70.96/24.11 [activate(n__a())] = [5] 70.96/24.11 > [3] 70.96/24.11 = [a()] 70.96/24.11 70.96/24.11 [activate(n__e())] = [5] 70.96/24.11 > [3] 70.96/24.11 = [e()] 70.96/24.11 70.96/24.11 [activate(n__i())] = [5] 70.96/24.11 > [3] 70.96/24.11 = [i()] 70.96/24.11 70.96/24.11 [activate(n__o())] = [5] 70.96/24.11 > [3] 70.96/24.11 = [o()] 70.96/24.11 70.96/24.11 [activate(n__u())] = [6] 70.96/24.11 >= [6] 70.96/24.11 = [u()] 70.96/24.11 70.96/24.11 [U31(tt())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [U41(tt(), V2)] = [1] V2 + [5] 70.96/24.11 >= [1] V2 + [5] 70.96/24.11 = [U42(isNeList(activate(V2)))] 70.96/24.11 70.96/24.11 [U42(tt())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isNeList(V)] = [1] V + [4] 70.96/24.11 > [1] V + [1] 70.96/24.11 = [U31(isQid(activate(V)))] 70.96/24.11 70.96/24.11 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [11] 70.96/24.11 > [1] V2 + [1] V1 + [10] 70.96/24.11 = [U41(isList(activate(V1)), activate(V2))] 70.96/24.11 70.96/24.11 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [11] 70.96/24.11 > [1] V2 + [1] V1 + [10] 70.96/24.11 = [U51(isNeList(activate(V1)), activate(V2))] 70.96/24.11 70.96/24.11 [U51(tt(), V2)] = [1] V2 + [8] 70.96/24.11 >= [1] V2 + [8] 70.96/24.11 = [U52(isList(activate(V2)))] 70.96/24.11 70.96/24.11 [U52(tt())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [U61(tt())] = [5] 70.96/24.11 > [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [U71(tt(), P)] = [1] P + [7] 70.96/24.11 >= [1] P + [7] 70.96/24.11 = [U72(isPal(activate(P)))] 70.96/24.11 70.96/24.11 [U72(tt())] = [5] 70.96/24.11 > [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isPal(V)] = [1] V + [5] 70.96/24.11 >= [1] V + [5] 70.96/24.11 = [U81(isNePal(activate(V)))] 70.96/24.11 70.96/24.11 [isPal(n__nil())] = [5] 70.96/24.11 > [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [U81(tt())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isQid(n__a())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isQid(n__e())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isQid(n__i())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isQid(n__o())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isQid(n__u())] = [5] 70.96/24.11 > [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isNePal(V)] = [1] V + [4] 70.96/24.11 > [1] V + [2] 70.96/24.11 = [U61(isQid(activate(V)))] 70.96/24.11 70.96/24.11 [a()] = [3] 70.96/24.11 ? [4] 70.96/24.11 = [n__a()] 70.96/24.11 70.96/24.11 [e()] = [3] 70.96/24.11 ? [4] 70.96/24.11 = [n__e()] 70.96/24.11 70.96/24.11 [i()] = [3] 70.96/24.11 ? [4] 70.96/24.11 = [n__i()] 70.96/24.11 70.96/24.11 [o()] = [3] 70.96/24.11 ? [4] 70.96/24.11 = [n__o()] 70.96/24.11 70.96/24.11 [u()] = [6] 70.96/24.11 > [5] 70.96/24.11 = [n__u()] 70.96/24.11 70.96/24.11 70.96/24.11 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.96/24.11 70.96/24.11 We are left with following problem, upon which TcT provides the 70.96/24.11 certificate YES(O(1),O(n^1)). 70.96/24.11 70.96/24.11 Strict Trs: 70.96/24.11 { a() -> n__a() 70.96/24.11 , e() -> n__e() 70.96/24.11 , i() -> n__i() 70.96/24.11 , o() -> n__o() } 70.96/24.11 Weak Trs: 70.96/24.11 { __(X1, X2) -> n____(X1, X2) 70.96/24.11 , nil() -> n__nil() 70.96/24.11 , U11(tt()) -> tt() 70.96/24.11 , U21(tt(), V2) -> U22(isList(activate(V2))) 70.96/24.11 , U22(tt()) -> tt() 70.96/24.11 , isList(V) -> U11(isNeList(activate(V))) 70.96/24.11 , isList(n__nil()) -> tt() 70.96/24.11 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 70.96/24.11 , activate(X) -> X 70.96/24.11 , activate(n__nil()) -> nil() 70.96/24.11 , activate(n____(X1, X2)) -> __(X1, X2) 70.96/24.11 , activate(n__a()) -> a() 70.96/24.11 , activate(n__e()) -> e() 70.96/24.11 , activate(n__i()) -> i() 70.96/24.11 , activate(n__o()) -> o() 70.96/24.11 , activate(n__u()) -> u() 70.96/24.11 , U31(tt()) -> tt() 70.96/24.11 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 70.96/24.11 , U42(tt()) -> tt() 70.96/24.11 , isNeList(V) -> U31(isQid(activate(V))) 70.96/24.11 , isNeList(n____(V1, V2)) -> 70.96/24.11 U41(isList(activate(V1)), activate(V2)) 70.96/24.11 , isNeList(n____(V1, V2)) -> 70.96/24.11 U51(isNeList(activate(V1)), activate(V2)) 70.96/24.11 , U51(tt(), V2) -> U52(isList(activate(V2))) 70.96/24.11 , U52(tt()) -> tt() 70.96/24.11 , U61(tt()) -> tt() 70.96/24.11 , U71(tt(), P) -> U72(isPal(activate(P))) 70.96/24.11 , U72(tt()) -> tt() 70.96/24.11 , isPal(V) -> U81(isNePal(activate(V))) 70.96/24.11 , isPal(n__nil()) -> tt() 70.96/24.11 , U81(tt()) -> tt() 70.96/24.11 , isQid(n__a()) -> tt() 70.96/24.11 , isQid(n__e()) -> tt() 70.96/24.11 , isQid(n__i()) -> tt() 70.96/24.11 , isQid(n__o()) -> tt() 70.96/24.11 , isQid(n__u()) -> tt() 70.96/24.11 , isNePal(V) -> U61(isQid(activate(V))) 70.96/24.11 , u() -> n__u() } 70.96/24.11 Obligation: 70.96/24.11 innermost runtime complexity 70.96/24.11 Answer: 70.96/24.11 YES(O(1),O(n^1)) 70.96/24.11 70.96/24.11 The weightgap principle applies (using the following nonconstant 70.96/24.11 growth matrix-interpretation) 70.96/24.11 70.96/24.11 The following argument positions are usable: 70.96/24.11 Uargs(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1}, 70.96/24.11 Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2}, 70.96/24.11 Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2}, 70.96/24.11 Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1}, 70.96/24.11 Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {1}, 70.96/24.11 Uargs(isNePal) = {1} 70.96/24.11 70.96/24.11 TcT has computed the following matrix interpretation satisfying 70.96/24.11 not(EDA) and not(IDA(1)). 70.96/24.11 70.96/24.11 [__](x1, x2) = [1] x1 + [1] x2 + [7] 70.96/24.11 70.96/24.11 [nil] = [3] 70.96/24.11 70.96/24.11 [U11](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [tt] = [3] 70.96/24.11 70.96/24.11 [U21](x1, x2) = [1] x1 + [1] x2 + [3] 70.96/24.11 70.96/24.11 [U22](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [isList](x1) = [1] x1 + [4] 70.96/24.11 70.96/24.11 [activate](x1) = [1] x1 + [2] 70.96/24.11 70.96/24.11 [U31](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [U41](x1, x2) = [1] x1 + [1] x2 + [1] 70.96/24.11 70.96/24.11 [U42](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [isNeList](x1) = [1] x1 + [2] 70.96/24.11 70.96/24.11 [U51](x1, x2) = [1] x1 + [1] x2 + [3] 70.96/24.11 70.96/24.11 [U52](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [U61](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [U71](x1, x2) = [1] x2 + [7] 70.96/24.11 70.96/24.11 [U72](x1) = [1] x1 + [1] 70.96/24.11 70.96/24.11 [isPal](x1) = [1] x1 + [4] 70.96/24.11 70.96/24.11 [U81](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [n__nil] = [2] 70.96/24.11 70.96/24.11 [n____](x1, x2) = [1] x1 + [1] x2 + [7] 70.96/24.11 70.96/24.11 [isQid](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [isNePal](x1) = [1] x1 + [2] 70.96/24.11 70.96/24.11 [n__a] = [3] 70.96/24.11 70.96/24.11 [n__e] = [3] 70.96/24.11 70.96/24.11 [n__i] = [3] 70.96/24.11 70.96/24.11 [n__o] = [6] 70.96/24.11 70.96/24.11 [n__u] = [4] 70.96/24.11 70.96/24.11 [a] = [5] 70.96/24.11 70.96/24.11 [e] = [3] 70.96/24.11 70.96/24.11 [i] = [3] 70.96/24.11 70.96/24.11 [o] = [7] 70.96/24.11 70.96/24.11 [u] = [5] 70.96/24.11 70.96/24.11 The order satisfies the following ordering constraints: 70.96/24.11 70.96/24.11 [__(X1, X2)] = [1] X1 + [1] X2 + [7] 70.96/24.11 >= [1] X1 + [1] X2 + [7] 70.96/24.11 = [n____(X1, X2)] 70.96/24.11 70.96/24.11 [nil()] = [3] 70.96/24.11 > [2] 70.96/24.11 = [n__nil()] 70.96/24.11 70.96/24.11 [U11(tt())] = [3] 70.96/24.11 >= [3] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [U21(tt(), V2)] = [1] V2 + [6] 70.96/24.11 >= [1] V2 + [6] 70.96/24.11 = [U22(isList(activate(V2)))] 70.96/24.11 70.96/24.11 [U22(tt())] = [3] 70.96/24.11 >= [3] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isList(V)] = [1] V + [4] 70.96/24.11 >= [1] V + [4] 70.96/24.11 = [U11(isNeList(activate(V)))] 70.96/24.11 70.96/24.11 [isList(n__nil())] = [6] 70.96/24.11 > [3] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isList(n____(V1, V2))] = [1] V2 + [1] V1 + [11] 70.96/24.11 >= [1] V2 + [1] V1 + [11] 70.96/24.11 = [U21(isList(activate(V1)), activate(V2))] 70.96/24.11 70.96/24.11 [activate(X)] = [1] X + [2] 70.96/24.11 > [1] X + [0] 70.96/24.11 = [X] 70.96/24.11 70.96/24.11 [activate(n__nil())] = [4] 70.96/24.11 > [3] 70.96/24.11 = [nil()] 70.96/24.11 70.96/24.11 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [9] 70.96/24.11 > [1] X1 + [1] X2 + [7] 70.96/24.11 = [__(X1, X2)] 70.96/24.11 70.96/24.11 [activate(n__a())] = [5] 70.96/24.11 >= [5] 70.96/24.11 = [a()] 70.96/24.11 70.96/24.11 [activate(n__e())] = [5] 70.96/24.11 > [3] 70.96/24.11 = [e()] 70.96/24.11 70.96/24.11 [activate(n__i())] = [5] 70.96/24.11 > [3] 70.96/24.11 = [i()] 70.96/24.11 70.96/24.11 [activate(n__o())] = [8] 70.96/24.11 > [7] 70.96/24.11 = [o()] 70.96/24.11 70.96/24.11 [activate(n__u())] = [6] 70.96/24.11 > [5] 70.96/24.11 = [u()] 70.96/24.11 70.96/24.11 [U31(tt())] = [3] 70.96/24.11 >= [3] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [U41(tt(), V2)] = [1] V2 + [4] 70.96/24.11 >= [1] V2 + [4] 70.96/24.11 = [U42(isNeList(activate(V2)))] 70.96/24.11 70.96/24.11 [U42(tt())] = [3] 70.96/24.11 >= [3] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isNeList(V)] = [1] V + [2] 70.96/24.11 >= [1] V + [2] 70.96/24.11 = [U31(isQid(activate(V)))] 70.96/24.11 70.96/24.11 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [9] 70.96/24.11 >= [1] V2 + [1] V1 + [9] 70.96/24.11 = [U41(isList(activate(V1)), activate(V2))] 70.96/24.11 70.96/24.11 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [9] 70.96/24.11 >= [1] V2 + [1] V1 + [9] 70.96/24.11 = [U51(isNeList(activate(V1)), activate(V2))] 70.96/24.11 70.96/24.11 [U51(tt(), V2)] = [1] V2 + [6] 70.96/24.11 >= [1] V2 + [6] 70.96/24.11 = [U52(isList(activate(V2)))] 70.96/24.11 70.96/24.11 [U52(tt())] = [3] 70.96/24.11 >= [3] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [U61(tt())] = [3] 70.96/24.11 >= [3] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [U71(tt(), P)] = [1] P + [7] 70.96/24.11 >= [1] P + [7] 70.96/24.11 = [U72(isPal(activate(P)))] 70.96/24.11 70.96/24.11 [U72(tt())] = [4] 70.96/24.11 > [3] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isPal(V)] = [1] V + [4] 70.96/24.11 >= [1] V + [4] 70.96/24.11 = [U81(isNePal(activate(V)))] 70.96/24.11 70.96/24.11 [isPal(n__nil())] = [6] 70.96/24.11 > [3] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [U81(tt())] = [3] 70.96/24.11 >= [3] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isQid(n__a())] = [3] 70.96/24.11 >= [3] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isQid(n__e())] = [3] 70.96/24.11 >= [3] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isQid(n__i())] = [3] 70.96/24.11 >= [3] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isQid(n__o())] = [6] 70.96/24.11 > [3] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isQid(n__u())] = [4] 70.96/24.11 > [3] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isNePal(V)] = [1] V + [2] 70.96/24.11 >= [1] V + [2] 70.96/24.11 = [U61(isQid(activate(V)))] 70.96/24.11 70.96/24.11 [a()] = [5] 70.96/24.11 > [3] 70.96/24.11 = [n__a()] 70.96/24.11 70.96/24.11 [e()] = [3] 70.96/24.11 >= [3] 70.96/24.11 = [n__e()] 70.96/24.11 70.96/24.11 [i()] = [3] 70.96/24.11 >= [3] 70.96/24.11 = [n__i()] 70.96/24.11 70.96/24.11 [o()] = [7] 70.96/24.11 > [6] 70.96/24.11 = [n__o()] 70.96/24.11 70.96/24.11 [u()] = [5] 70.96/24.11 > [4] 70.96/24.11 = [n__u()] 70.96/24.11 70.96/24.11 70.96/24.11 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.96/24.11 70.96/24.11 We are left with following problem, upon which TcT provides the 70.96/24.11 certificate YES(O(1),O(n^1)). 70.96/24.11 70.96/24.11 Strict Trs: 70.96/24.11 { e() -> n__e() 70.96/24.11 , i() -> n__i() } 70.96/24.11 Weak Trs: 70.96/24.11 { __(X1, X2) -> n____(X1, X2) 70.96/24.11 , nil() -> n__nil() 70.96/24.11 , U11(tt()) -> tt() 70.96/24.11 , U21(tt(), V2) -> U22(isList(activate(V2))) 70.96/24.11 , U22(tt()) -> tt() 70.96/24.11 , isList(V) -> U11(isNeList(activate(V))) 70.96/24.11 , isList(n__nil()) -> tt() 70.96/24.11 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 70.96/24.11 , activate(X) -> X 70.96/24.11 , activate(n__nil()) -> nil() 70.96/24.11 , activate(n____(X1, X2)) -> __(X1, X2) 70.96/24.11 , activate(n__a()) -> a() 70.96/24.11 , activate(n__e()) -> e() 70.96/24.11 , activate(n__i()) -> i() 70.96/24.11 , activate(n__o()) -> o() 70.96/24.11 , activate(n__u()) -> u() 70.96/24.11 , U31(tt()) -> tt() 70.96/24.11 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 70.96/24.11 , U42(tt()) -> tt() 70.96/24.11 , isNeList(V) -> U31(isQid(activate(V))) 70.96/24.11 , isNeList(n____(V1, V2)) -> 70.96/24.11 U41(isList(activate(V1)), activate(V2)) 70.96/24.11 , isNeList(n____(V1, V2)) -> 70.96/24.11 U51(isNeList(activate(V1)), activate(V2)) 70.96/24.11 , U51(tt(), V2) -> U52(isList(activate(V2))) 70.96/24.11 , U52(tt()) -> tt() 70.96/24.11 , U61(tt()) -> tt() 70.96/24.11 , U71(tt(), P) -> U72(isPal(activate(P))) 70.96/24.11 , U72(tt()) -> tt() 70.96/24.11 , isPal(V) -> U81(isNePal(activate(V))) 70.96/24.11 , isPal(n__nil()) -> tt() 70.96/24.11 , U81(tt()) -> tt() 70.96/24.11 , isQid(n__a()) -> tt() 70.96/24.11 , isQid(n__e()) -> tt() 70.96/24.11 , isQid(n__i()) -> tt() 70.96/24.11 , isQid(n__o()) -> tt() 70.96/24.11 , isQid(n__u()) -> tt() 70.96/24.11 , isNePal(V) -> U61(isQid(activate(V))) 70.96/24.11 , a() -> n__a() 70.96/24.11 , o() -> n__o() 70.96/24.11 , u() -> n__u() } 70.96/24.11 Obligation: 70.96/24.11 innermost runtime complexity 70.96/24.11 Answer: 70.96/24.11 YES(O(1),O(n^1)) 70.96/24.11 70.96/24.11 The weightgap principle applies (using the following nonconstant 70.96/24.11 growth matrix-interpretation) 70.96/24.11 70.96/24.11 The following argument positions are usable: 70.96/24.11 Uargs(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1}, 70.96/24.11 Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2}, 70.96/24.11 Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2}, 70.96/24.11 Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1}, 70.96/24.11 Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {1}, 70.96/24.11 Uargs(isNePal) = {1} 70.96/24.11 70.96/24.11 TcT has computed the following matrix interpretation satisfying 70.96/24.11 not(EDA) and not(IDA(1)). 70.96/24.11 70.96/24.11 [__](x1, x2) = [1] x1 + [1] x2 + [7] 70.96/24.11 70.96/24.11 [nil] = [3] 70.96/24.11 70.96/24.11 [U11](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [tt] = [4] 70.96/24.11 70.96/24.11 [U21](x1, x2) = [1] x1 + [1] x2 + [4] 70.96/24.11 70.96/24.11 [U22](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [isList](x1) = [1] x1 + [7] 70.96/24.11 70.96/24.11 [activate](x1) = [1] x1 + [1] 70.96/24.11 70.96/24.11 [U31](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [U41](x1, x2) = [1] x1 + [1] x2 + [1] 70.96/24.11 70.96/24.11 [U42](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [isNeList](x1) = [1] x1 + [4] 70.96/24.11 70.96/24.11 [U51](x1, x2) = [1] x1 + [1] x2 + [4] 70.96/24.11 70.96/24.11 [U52](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [U61](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [U71](x1, x2) = [1] x2 + [7] 70.96/24.11 70.96/24.11 [U72](x1) = [1] x1 + [1] 70.96/24.11 70.96/24.11 [isPal](x1) = [1] x1 + [4] 70.96/24.11 70.96/24.11 [U81](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [n__nil] = [2] 70.96/24.11 70.96/24.11 [n____](x1, x2) = [1] x1 + [1] x2 + [6] 70.96/24.11 70.96/24.11 [isQid](x1) = [1] x1 + [0] 70.96/24.11 70.96/24.11 [isNePal](x1) = [1] x1 + [1] 70.96/24.11 70.96/24.11 [n__a] = [4] 70.96/24.11 70.96/24.11 [n__e] = [4] 70.96/24.11 70.96/24.11 [n__i] = [5] 70.96/24.11 70.96/24.11 [n__o] = [4] 70.96/24.11 70.96/24.11 [n__u] = [4] 70.96/24.11 70.96/24.11 [a] = [5] 70.96/24.11 70.96/24.11 [e] = [3] 70.96/24.11 70.96/24.11 [i] = [6] 70.96/24.11 70.96/24.11 [o] = [5] 70.96/24.11 70.96/24.11 [u] = [5] 70.96/24.11 70.96/24.11 The order satisfies the following ordering constraints: 70.96/24.11 70.96/24.11 [__(X1, X2)] = [1] X1 + [1] X2 + [7] 70.96/24.11 > [1] X1 + [1] X2 + [6] 70.96/24.11 = [n____(X1, X2)] 70.96/24.11 70.96/24.11 [nil()] = [3] 70.96/24.11 > [2] 70.96/24.11 = [n__nil()] 70.96/24.11 70.96/24.11 [U11(tt())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [U21(tt(), V2)] = [1] V2 + [8] 70.96/24.11 >= [1] V2 + [8] 70.96/24.11 = [U22(isList(activate(V2)))] 70.96/24.11 70.96/24.11 [U22(tt())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isList(V)] = [1] V + [7] 70.96/24.11 > [1] V + [5] 70.96/24.11 = [U11(isNeList(activate(V)))] 70.96/24.11 70.96/24.11 [isList(n__nil())] = [9] 70.96/24.11 > [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isList(n____(V1, V2))] = [1] V2 + [1] V1 + [13] 70.96/24.11 >= [1] V2 + [1] V1 + [13] 70.96/24.11 = [U21(isList(activate(V1)), activate(V2))] 70.96/24.11 70.96/24.11 [activate(X)] = [1] X + [1] 70.96/24.11 > [1] X + [0] 70.96/24.11 = [X] 70.96/24.11 70.96/24.11 [activate(n__nil())] = [3] 70.96/24.11 >= [3] 70.96/24.11 = [nil()] 70.96/24.11 70.96/24.11 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [7] 70.96/24.11 >= [1] X1 + [1] X2 + [7] 70.96/24.11 = [__(X1, X2)] 70.96/24.11 70.96/24.11 [activate(n__a())] = [5] 70.96/24.11 >= [5] 70.96/24.11 = [a()] 70.96/24.11 70.96/24.11 [activate(n__e())] = [5] 70.96/24.11 > [3] 70.96/24.11 = [e()] 70.96/24.11 70.96/24.11 [activate(n__i())] = [6] 70.96/24.11 >= [6] 70.96/24.11 = [i()] 70.96/24.11 70.96/24.11 [activate(n__o())] = [5] 70.96/24.11 >= [5] 70.96/24.11 = [o()] 70.96/24.11 70.96/24.11 [activate(n__u())] = [5] 70.96/24.11 >= [5] 70.96/24.11 = [u()] 70.96/24.11 70.96/24.11 [U31(tt())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [U41(tt(), V2)] = [1] V2 + [5] 70.96/24.11 >= [1] V2 + [5] 70.96/24.11 = [U42(isNeList(activate(V2)))] 70.96/24.11 70.96/24.11 [U42(tt())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isNeList(V)] = [1] V + [4] 70.96/24.11 > [1] V + [1] 70.96/24.11 = [U31(isQid(activate(V)))] 70.96/24.11 70.96/24.11 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [10] 70.96/24.11 >= [1] V2 + [1] V1 + [10] 70.96/24.11 = [U41(isList(activate(V1)), activate(V2))] 70.96/24.11 70.96/24.11 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [10] 70.96/24.11 >= [1] V2 + [1] V1 + [10] 70.96/24.11 = [U51(isNeList(activate(V1)), activate(V2))] 70.96/24.11 70.96/24.11 [U51(tt(), V2)] = [1] V2 + [8] 70.96/24.11 >= [1] V2 + [8] 70.96/24.11 = [U52(isList(activate(V2)))] 70.96/24.11 70.96/24.11 [U52(tt())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [U61(tt())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [U71(tt(), P)] = [1] P + [7] 70.96/24.11 > [1] P + [6] 70.96/24.11 = [U72(isPal(activate(P)))] 70.96/24.11 70.96/24.11 [U72(tt())] = [5] 70.96/24.11 > [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isPal(V)] = [1] V + [4] 70.96/24.11 > [1] V + [2] 70.96/24.11 = [U81(isNePal(activate(V)))] 70.96/24.11 70.96/24.11 [isPal(n__nil())] = [6] 70.96/24.11 > [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [U81(tt())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isQid(n__a())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isQid(n__e())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isQid(n__i())] = [5] 70.96/24.11 > [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isQid(n__o())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isQid(n__u())] = [4] 70.96/24.11 >= [4] 70.96/24.11 = [tt()] 70.96/24.11 70.96/24.11 [isNePal(V)] = [1] V + [1] 70.96/24.11 >= [1] V + [1] 70.96/24.11 = [U61(isQid(activate(V)))] 70.96/24.11 70.96/24.11 [a()] = [5] 70.96/24.11 > [4] 70.96/24.11 = [n__a()] 70.96/24.11 70.96/24.11 [e()] = [3] 70.96/24.11 ? [4] 70.96/24.11 = [n__e()] 70.96/24.11 70.96/24.11 [i()] = [6] 70.96/24.11 > [5] 70.96/24.11 = [n__i()] 70.96/24.11 70.96/24.11 [o()] = [5] 70.96/24.11 > [4] 70.96/24.11 = [n__o()] 70.96/24.11 70.96/24.11 [u()] = [5] 70.96/24.11 > [4] 70.96/24.11 = [n__u()] 70.96/24.11 70.96/24.11 70.96/24.11 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.96/24.11 70.96/24.11 We are left with following problem, upon which TcT provides the 70.96/24.11 certificate YES(O(1),O(n^1)). 70.96/24.11 70.96/24.11 Strict Trs: { e() -> n__e() } 70.96/24.11 Weak Trs: 70.96/24.11 { __(X1, X2) -> n____(X1, X2) 70.96/24.11 , nil() -> n__nil() 70.96/24.11 , U11(tt()) -> tt() 70.96/24.11 , U21(tt(), V2) -> U22(isList(activate(V2))) 70.96/24.11 , U22(tt()) -> tt() 70.96/24.11 , isList(V) -> U11(isNeList(activate(V))) 70.96/24.11 , isList(n__nil()) -> tt() 70.96/24.11 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 70.96/24.11 , activate(X) -> X 70.96/24.11 , activate(n__nil()) -> nil() 70.96/24.11 , activate(n____(X1, X2)) -> __(X1, X2) 70.96/24.11 , activate(n__a()) -> a() 70.96/24.11 , activate(n__e()) -> e() 70.96/24.11 , activate(n__i()) -> i() 70.96/24.11 , activate(n__o()) -> o() 70.96/24.11 , activate(n__u()) -> u() 70.96/24.11 , U31(tt()) -> tt() 70.96/24.11 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 70.96/24.11 , U42(tt()) -> tt() 70.96/24.11 , isNeList(V) -> U31(isQid(activate(V))) 70.96/24.11 , isNeList(n____(V1, V2)) -> 70.96/24.11 U41(isList(activate(V1)), activate(V2)) 70.96/24.11 , isNeList(n____(V1, V2)) -> 70.96/24.11 U51(isNeList(activate(V1)), activate(V2)) 70.96/24.11 , U51(tt(), V2) -> U52(isList(activate(V2))) 70.96/24.11 , U52(tt()) -> tt() 70.96/24.11 , U61(tt()) -> tt() 70.96/24.11 , U71(tt(), P) -> U72(isPal(activate(P))) 70.96/24.11 , U72(tt()) -> tt() 70.96/24.11 , isPal(V) -> U81(isNePal(activate(V))) 70.96/24.11 , isPal(n__nil()) -> tt() 70.96/24.11 , U81(tt()) -> tt() 70.96/24.11 , isQid(n__a()) -> tt() 70.96/24.11 , isQid(n__e()) -> tt() 70.96/24.11 , isQid(n__i()) -> tt() 70.96/24.11 , isQid(n__o()) -> tt() 70.96/24.11 , isQid(n__u()) -> tt() 70.96/24.11 , isNePal(V) -> U61(isQid(activate(V))) 70.96/24.11 , a() -> n__a() 70.96/24.11 , i() -> n__i() 70.96/24.11 , o() -> n__o() 70.96/24.11 , u() -> n__u() } 70.96/24.11 Obligation: 70.96/24.11 innermost runtime complexity 70.96/24.11 Answer: 70.96/24.11 YES(O(1),O(n^1)) 70.96/24.11 70.96/24.11 The weightgap principle applies (using the following nonconstant 70.96/24.11 growth matrix-interpretation) 70.96/24.11 70.96/24.11 The following argument positions are usable: 70.96/24.12 Uargs(U11) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1}, 70.96/24.12 Uargs(isList) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1, 2}, 70.96/24.12 Uargs(U42) = {1}, Uargs(isNeList) = {1}, Uargs(U51) = {1, 2}, 70.96/24.12 Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U72) = {1}, 70.96/24.12 Uargs(isPal) = {1}, Uargs(U81) = {1}, Uargs(isQid) = {1}, 70.96/24.12 Uargs(isNePal) = {1} 70.96/24.12 70.96/24.12 TcT has computed the following matrix interpretation satisfying 70.96/24.12 not(EDA) and not(IDA(1)). 70.96/24.12 70.96/24.12 [__](x1, x2) = [1] x1 + [1] x2 + [7] 70.96/24.12 70.96/24.12 [nil] = [1] 70.96/24.12 70.96/24.12 [U11](x1) = [1] x1 + [0] 70.96/24.12 70.96/24.12 [tt] = [3] 70.96/24.12 70.96/24.12 [U21](x1, x2) = [1] x1 + [1] x2 + [5] 70.96/24.12 70.96/24.12 [U22](x1) = [1] x1 + [0] 70.96/24.12 70.96/24.12 [isList](x1) = [1] x1 + [7] 70.96/24.12 70.96/24.12 [activate](x1) = [1] x1 + [1] 70.96/24.12 70.96/24.12 [U31](x1) = [1] x1 + [0] 70.96/24.12 70.96/24.12 [U41](x1, x2) = [1] x1 + [1] x2 + [2] 70.96/24.12 70.96/24.12 [U42](x1) = [1] x1 + [0] 70.96/24.12 70.96/24.12 [isNeList](x1) = [1] x1 + [4] 70.96/24.12 70.96/24.12 [U51](x1, x2) = [1] x1 + [1] x2 + [5] 70.96/24.12 70.96/24.12 [U52](x1) = [1] x1 + [0] 70.96/24.12 70.96/24.12 [U61](x1) = [1] x1 + [0] 70.96/24.12 70.96/24.12 [U71](x1, x2) = [1] x1 + [1] x2 + [7] 70.96/24.12 70.96/24.12 [U72](x1) = [1] x1 + [2] 70.96/24.12 70.96/24.12 [isPal](x1) = [1] x1 + [7] 70.96/24.12 70.96/24.12 [U81](x1) = [1] x1 + [0] 70.96/24.12 70.96/24.12 [n__nil] = [0] 70.96/24.12 70.96/24.12 [n____](x1, x2) = [1] x1 + [1] x2 + [7] 70.96/24.12 70.96/24.12 [isQid](x1) = [1] x1 + [0] 70.96/24.12 70.96/24.12 [isNePal](x1) = [1] x1 + [1] 70.96/24.12 70.96/24.12 [n__a] = [4] 70.96/24.12 70.96/24.12 [n__e] = [4] 70.96/24.12 70.96/24.12 [n__i] = [4] 70.96/24.12 70.96/24.12 [n__o] = [4] 70.96/24.12 70.96/24.12 [n__u] = [4] 70.96/24.12 70.96/24.12 [a] = [5] 70.96/24.12 70.96/24.12 [e] = [5] 70.96/24.12 70.96/24.12 [i] = [5] 70.96/24.12 70.96/24.12 [o] = [5] 70.96/24.12 70.96/24.12 [u] = [5] 70.96/24.12 70.96/24.12 The order satisfies the following ordering constraints: 70.96/24.12 70.96/24.12 [__(X1, X2)] = [1] X1 + [1] X2 + [7] 70.96/24.12 >= [1] X1 + [1] X2 + [7] 70.96/24.12 = [n____(X1, X2)] 70.96/24.12 70.96/24.12 [nil()] = [1] 70.96/24.12 > [0] 70.96/24.12 = [n__nil()] 70.96/24.12 70.96/24.12 [U11(tt())] = [3] 70.96/24.12 >= [3] 70.96/24.12 = [tt()] 70.96/24.12 70.96/24.12 [U21(tt(), V2)] = [1] V2 + [8] 70.96/24.12 >= [1] V2 + [8] 70.96/24.12 = [U22(isList(activate(V2)))] 70.96/24.12 70.96/24.12 [U22(tt())] = [3] 70.96/24.12 >= [3] 70.96/24.12 = [tt()] 70.96/24.12 70.96/24.12 [isList(V)] = [1] V + [7] 70.96/24.12 > [1] V + [5] 70.96/24.12 = [U11(isNeList(activate(V)))] 70.96/24.12 70.96/24.12 [isList(n__nil())] = [7] 70.96/24.12 > [3] 70.96/24.12 = [tt()] 70.96/24.12 70.96/24.12 [isList(n____(V1, V2))] = [1] V2 + [1] V1 + [14] 70.96/24.12 >= [1] V2 + [1] V1 + [14] 70.96/24.12 = [U21(isList(activate(V1)), activate(V2))] 70.96/24.12 70.96/24.12 [activate(X)] = [1] X + [1] 70.96/24.12 > [1] X + [0] 70.96/24.12 = [X] 70.96/24.12 70.96/24.12 [activate(n__nil())] = [1] 70.96/24.12 >= [1] 70.96/24.12 = [nil()] 70.96/24.12 70.96/24.12 [activate(n____(X1, X2))] = [1] X1 + [1] X2 + [8] 70.96/24.12 > [1] X1 + [1] X2 + [7] 70.96/24.12 = [__(X1, X2)] 70.96/24.12 70.96/24.12 [activate(n__a())] = [5] 70.96/24.12 >= [5] 70.96/24.12 = [a()] 70.96/24.12 70.96/24.12 [activate(n__e())] = [5] 70.96/24.12 >= [5] 70.96/24.12 = [e()] 70.96/24.12 70.96/24.12 [activate(n__i())] = [5] 70.96/24.12 >= [5] 70.96/24.12 = [i()] 70.96/24.12 70.96/24.12 [activate(n__o())] = [5] 70.96/24.12 >= [5] 70.96/24.12 = [o()] 70.96/24.12 70.96/24.12 [activate(n__u())] = [5] 70.96/24.12 >= [5] 70.96/24.12 = [u()] 70.96/24.12 70.96/24.12 [U31(tt())] = [3] 70.96/24.12 >= [3] 70.96/24.12 = [tt()] 70.96/24.12 70.96/24.12 [U41(tt(), V2)] = [1] V2 + [5] 70.96/24.12 >= [1] V2 + [5] 70.96/24.12 = [U42(isNeList(activate(V2)))] 70.96/24.12 70.96/24.12 [U42(tt())] = [3] 70.96/24.12 >= [3] 70.96/24.12 = [tt()] 70.96/24.12 70.96/24.12 [isNeList(V)] = [1] V + [4] 70.96/24.12 > [1] V + [1] 70.96/24.12 = [U31(isQid(activate(V)))] 70.96/24.12 70.96/24.12 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [11] 70.96/24.12 >= [1] V2 + [1] V1 + [11] 70.96/24.12 = [U41(isList(activate(V1)), activate(V2))] 70.96/24.12 70.96/24.12 [isNeList(n____(V1, V2))] = [1] V2 + [1] V1 + [11] 70.96/24.12 >= [1] V2 + [1] V1 + [11] 70.96/24.12 = [U51(isNeList(activate(V1)), activate(V2))] 70.96/24.12 70.96/24.12 [U51(tt(), V2)] = [1] V2 + [8] 70.96/24.12 >= [1] V2 + [8] 70.96/24.12 = [U52(isList(activate(V2)))] 70.96/24.12 70.96/24.12 [U52(tt())] = [3] 70.96/24.12 >= [3] 70.96/24.12 = [tt()] 70.96/24.12 70.96/24.12 [U61(tt())] = [3] 70.96/24.12 >= [3] 70.96/24.12 = [tt()] 70.96/24.12 70.96/24.12 [U71(tt(), P)] = [1] P + [10] 70.96/24.12 >= [1] P + [10] 70.96/24.12 = [U72(isPal(activate(P)))] 70.96/24.12 70.96/24.12 [U72(tt())] = [5] 70.96/24.12 > [3] 70.96/24.12 = [tt()] 70.96/24.12 70.96/24.12 [isPal(V)] = [1] V + [7] 70.96/24.12 > [1] V + [2] 70.96/24.12 = [U81(isNePal(activate(V)))] 70.96/24.12 70.96/24.12 [isPal(n__nil())] = [7] 70.96/24.12 > [3] 70.96/24.12 = [tt()] 70.96/24.12 70.96/24.12 [U81(tt())] = [3] 70.96/24.12 >= [3] 70.96/24.12 = [tt()] 70.96/24.12 70.96/24.12 [isQid(n__a())] = [4] 70.96/24.12 > [3] 70.96/24.12 = [tt()] 70.96/24.12 70.96/24.12 [isQid(n__e())] = [4] 70.96/24.12 > [3] 70.96/24.12 = [tt()] 70.96/24.12 70.96/24.12 [isQid(n__i())] = [4] 70.96/24.12 > [3] 70.96/24.12 = [tt()] 70.96/24.12 70.96/24.12 [isQid(n__o())] = [4] 70.96/24.12 > [3] 70.96/24.12 = [tt()] 70.96/24.12 70.96/24.12 [isQid(n__u())] = [4] 70.96/24.12 > [3] 70.96/24.12 = [tt()] 70.96/24.12 70.96/24.12 [isNePal(V)] = [1] V + [1] 70.96/24.12 >= [1] V + [1] 70.96/24.12 = [U61(isQid(activate(V)))] 70.96/24.12 70.96/24.12 [a()] = [5] 70.96/24.12 > [4] 70.96/24.12 = [n__a()] 70.96/24.12 70.96/24.12 [e()] = [5] 70.96/24.12 > [4] 70.96/24.12 = [n__e()] 70.96/24.12 70.96/24.12 [i()] = [5] 70.96/24.12 > [4] 70.96/24.12 = [n__i()] 70.96/24.12 70.96/24.12 [o()] = [5] 70.96/24.12 > [4] 70.96/24.12 = [n__o()] 70.96/24.12 70.96/24.12 [u()] = [5] 70.96/24.12 > [4] 70.96/24.12 = [n__u()] 70.96/24.12 70.96/24.12 70.96/24.12 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 70.96/24.12 70.96/24.12 We are left with following problem, upon which TcT provides the 70.96/24.12 certificate YES(O(1),O(1)). 70.96/24.12 70.96/24.12 Weak Trs: 70.96/24.12 { __(X1, X2) -> n____(X1, X2) 70.96/24.12 , nil() -> n__nil() 70.96/24.12 , U11(tt()) -> tt() 70.96/24.12 , U21(tt(), V2) -> U22(isList(activate(V2))) 70.96/24.12 , U22(tt()) -> tt() 70.96/24.12 , isList(V) -> U11(isNeList(activate(V))) 70.96/24.12 , isList(n__nil()) -> tt() 70.96/24.12 , isList(n____(V1, V2)) -> U21(isList(activate(V1)), activate(V2)) 70.96/24.12 , activate(X) -> X 70.96/24.12 , activate(n__nil()) -> nil() 70.96/24.12 , activate(n____(X1, X2)) -> __(X1, X2) 70.96/24.12 , activate(n__a()) -> a() 70.96/24.12 , activate(n__e()) -> e() 70.96/24.12 , activate(n__i()) -> i() 70.96/24.12 , activate(n__o()) -> o() 70.96/24.12 , activate(n__u()) -> u() 70.96/24.12 , U31(tt()) -> tt() 70.96/24.12 , U41(tt(), V2) -> U42(isNeList(activate(V2))) 70.96/24.12 , U42(tt()) -> tt() 70.96/24.12 , isNeList(V) -> U31(isQid(activate(V))) 70.96/24.12 , isNeList(n____(V1, V2)) -> 70.96/24.12 U41(isList(activate(V1)), activate(V2)) 70.96/24.12 , isNeList(n____(V1, V2)) -> 70.96/24.12 U51(isNeList(activate(V1)), activate(V2)) 70.96/24.12 , U51(tt(), V2) -> U52(isList(activate(V2))) 70.96/24.12 , U52(tt()) -> tt() 70.96/24.12 , U61(tt()) -> tt() 70.96/24.12 , U71(tt(), P) -> U72(isPal(activate(P))) 70.96/24.12 , U72(tt()) -> tt() 70.96/24.12 , isPal(V) -> U81(isNePal(activate(V))) 70.96/24.12 , isPal(n__nil()) -> tt() 70.96/24.12 , U81(tt()) -> tt() 70.96/24.12 , isQid(n__a()) -> tt() 70.96/24.12 , isQid(n__e()) -> tt() 70.96/24.12 , isQid(n__i()) -> tt() 70.96/24.12 , isQid(n__o()) -> tt() 70.96/24.12 , isQid(n__u()) -> tt() 70.96/24.12 , isNePal(V) -> U61(isQid(activate(V))) 70.96/24.12 , a() -> n__a() 70.96/24.12 , e() -> n__e() 70.96/24.12 , i() -> n__i() 70.96/24.12 , o() -> n__o() 70.96/24.12 , u() -> n__u() } 70.96/24.12 Obligation: 70.96/24.12 innermost runtime complexity 70.96/24.12 Answer: 70.96/24.12 YES(O(1),O(1)) 70.96/24.12 70.96/24.12 Empty rules are trivially bounded 70.96/24.12 70.96/24.12 Hurray, we answered YES(O(1),O(n^1)) 70.96/24.12 EOF