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