We are left with following problem, upon which TcT provides the
certificate YES(O(1),POLY).
Strict Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS))
, U21(tt(), X) -> U22(tt(), activate(X))
, U22(tt(), X) -> activate(X)
, U31(tt(), N) -> U32(tt(), activate(N))
, U32(tt(), N) -> activate(N)
, U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS))
, U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
, head(cons(N, XS)) -> U31(tt(), N)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, U61(tt(), N, X, XS) ->
U62(tt(), activate(N), activate(X), activate(XS))
, U62(tt(), N, X, XS) ->
U63(tt(), activate(N), activate(X), activate(XS))
, U63(tt(), N, X, XS) ->
U64(splitAt(activate(N), activate(XS)), activate(X))
, U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
, U71(tt(), XS) -> U72(tt(), activate(XS))
, U72(tt(), XS) -> activate(XS)
, U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS))
, U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
, fst(pair(X, Y)) -> U21(tt(), X)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, sel(N, XS) -> U41(tt(), N, XS)
, s(X) -> n__s(X)
, tail(cons(N, XS)) -> U71(tt(), activate(XS))
, take(N, XS) -> U81(tt(), N, XS) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),POLY)
Arguments of following rules are not normal-forms:
{ splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)) }
All above mentioned rules can be savely removed.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),POLY).
Strict Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, U21(tt(), X) -> U22(tt(), activate(X))
, U22(tt(), X) -> activate(X)
, U31(tt(), N) -> U32(tt(), activate(N))
, U32(tt(), N) -> activate(N)
, U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS))
, U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
, head(cons(N, XS)) -> U31(tt(), N)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, U61(tt(), N, X, XS) ->
U62(tt(), activate(N), activate(X), activate(XS))
, U62(tt(), N, X, XS) ->
U63(tt(), activate(N), activate(X), activate(XS))
, U63(tt(), N, X, XS) ->
U64(splitAt(activate(N), activate(XS)), activate(X))
, U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
, U71(tt(), XS) -> U72(tt(), activate(XS))
, U72(tt(), XS) -> activate(XS)
, U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS))
, U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
, fst(pair(X, Y)) -> U21(tt(), X)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, sel(N, XS) -> U41(tt(), N, XS)
, s(X) -> n__s(X)
, tail(cons(N, XS)) -> U71(tt(), activate(XS))
, take(N, XS) -> U81(tt(), N, XS) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),POLY)
We add the following dependency tuples:
Strict DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, activate^#(X) -> c_3()
, activate^#(n__natsFrom(X)) ->
c_4(natsFrom^#(activate(X)), activate^#(X))
, activate^#(n__s(X)) -> c_5(s^#(activate(X)), activate^#(X))
, snd^#(pair(X, Y)) -> c_6(U51^#(tt(), Y))
, splitAt^#(0(), XS) -> c_7()
, natsFrom^#(N) -> c_27()
, natsFrom^#(X) -> c_28()
, s^#(X) -> c_30()
, U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_9(activate^#(X))
, U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_11(activate^#(N))
, U41^#(tt(), N, XS) ->
c_12(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_13(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, head^#(cons(N, XS)) -> c_14(U31^#(tt(), N))
, afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS))
, U52^#(tt(), Y) -> c_17(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_18(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_19(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_21(activate^#(X))
, U71^#(tt(), XS) ->
c_22(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_23(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_24(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_25(fst^#(splitAt(activate(N), activate(XS))),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X))
, sel^#(N, XS) -> c_29(U41^#(tt(), N, XS))
, tail^#(cons(N, XS)) ->
c_31(U71^#(tt(), activate(XS)), activate^#(XS))
, take^#(N, XS) -> c_32(U81^#(tt(), N, XS)) }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),POLY).
Strict DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, activate^#(X) -> c_3()
, activate^#(n__natsFrom(X)) ->
c_4(natsFrom^#(activate(X)), activate^#(X))
, activate^#(n__s(X)) -> c_5(s^#(activate(X)), activate^#(X))
, snd^#(pair(X, Y)) -> c_6(U51^#(tt(), Y))
, splitAt^#(0(), XS) -> c_7()
, natsFrom^#(N) -> c_27()
, natsFrom^#(X) -> c_28()
, s^#(X) -> c_30()
, U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_9(activate^#(X))
, U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_11(activate^#(N))
, U41^#(tt(), N, XS) ->
c_12(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_13(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, head^#(cons(N, XS)) -> c_14(U31^#(tt(), N))
, afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS))
, U52^#(tt(), Y) -> c_17(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_18(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_19(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_21(activate^#(X))
, U71^#(tt(), XS) ->
c_22(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_23(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_24(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_25(fst^#(splitAt(activate(N), activate(XS))),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X))
, sel^#(N, XS) -> c_29(U41^#(tt(), N, XS))
, tail^#(cons(N, XS)) ->
c_31(U71^#(tt(), activate(XS)), activate^#(XS))
, take^#(N, XS) -> c_32(U81^#(tt(), N, XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, U21(tt(), X) -> U22(tt(), activate(X))
, U22(tt(), X) -> activate(X)
, U31(tt(), N) -> U32(tt(), activate(N))
, U32(tt(), N) -> activate(N)
, U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS))
, U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
, head(cons(N, XS)) -> U31(tt(), N)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, U61(tt(), N, X, XS) ->
U62(tt(), activate(N), activate(X), activate(XS))
, U62(tt(), N, X, XS) ->
U63(tt(), activate(N), activate(X), activate(XS))
, U63(tt(), N, X, XS) ->
U64(splitAt(activate(N), activate(XS)), activate(X))
, U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
, U71(tt(), XS) -> U72(tt(), activate(XS))
, U72(tt(), XS) -> activate(XS)
, U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS))
, U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
, fst(pair(X, Y)) -> U21(tt(), X)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, sel(N, XS) -> U41(tt(), N, XS)
, s(X) -> n__s(X)
, tail(cons(N, XS)) -> U71(tt(), activate(XS))
, take(N, XS) -> U81(tt(), N, XS) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),POLY)
We estimate the number of application of {3,7,8,9,10} by
applications of Pre({3,7,8,9,10}) =
{1,2,4,5,11,12,13,14,15,16,17,20,21,22,23,24,25,26,27,28,31}. Here
rules are labeled as follows:
DPs:
{ 1: U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 2: U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 3: activate^#(X) -> c_3()
, 4: activate^#(n__natsFrom(X)) ->
c_4(natsFrom^#(activate(X)), activate^#(X))
, 5: activate^#(n__s(X)) -> c_5(s^#(activate(X)), activate^#(X))
, 6: snd^#(pair(X, Y)) -> c_6(U51^#(tt(), Y))
, 7: splitAt^#(0(), XS) -> c_7()
, 8: natsFrom^#(N) -> c_27()
, 9: natsFrom^#(X) -> c_28()
, 10: s^#(X) -> c_30()
, 11: U51^#(tt(), Y) ->
c_16(U52^#(tt(), activate(Y)), activate^#(Y))
, 12: U21^#(tt(), X) ->
c_8(U22^#(tt(), activate(X)), activate^#(X))
, 13: U22^#(tt(), X) -> c_9(activate^#(X))
, 14: U31^#(tt(), N) ->
c_10(U32^#(tt(), activate(N)), activate^#(N))
, 15: U32^#(tt(), N) -> c_11(activate^#(N))
, 16: U41^#(tt(), N, XS) ->
c_12(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 17: U42^#(tt(), N, XS) ->
c_13(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 18: head^#(cons(N, XS)) -> c_14(U31^#(tt(), N))
, 19: afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS))
, 20: U52^#(tt(), Y) -> c_17(activate^#(Y))
, 21: U61^#(tt(), N, X, XS) ->
c_18(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 22: U62^#(tt(), N, X, XS) ->
c_19(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 23: U63^#(tt(), N, X, XS) ->
c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS),
activate^#(X))
, 24: U64^#(pair(YS, ZS), X) -> c_21(activate^#(X))
, 25: U71^#(tt(), XS) ->
c_22(U72^#(tt(), activate(XS)), activate^#(XS))
, 26: U72^#(tt(), XS) -> c_23(activate^#(XS))
, 27: U81^#(tt(), N, XS) ->
c_24(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 28: U82^#(tt(), N, XS) ->
c_25(fst^#(splitAt(activate(N), activate(XS))),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 29: fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X))
, 30: sel^#(N, XS) -> c_29(U41^#(tt(), N, XS))
, 31: tail^#(cons(N, XS)) ->
c_31(U71^#(tt(), activate(XS)), activate^#(XS))
, 32: take^#(N, XS) -> c_32(U81^#(tt(), N, XS)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),POLY).
Strict DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) ->
c_4(natsFrom^#(activate(X)), activate^#(X))
, activate^#(n__s(X)) -> c_5(s^#(activate(X)), activate^#(X))
, snd^#(pair(X, Y)) -> c_6(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_9(activate^#(X))
, U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_11(activate^#(N))
, U41^#(tt(), N, XS) ->
c_12(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_13(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, head^#(cons(N, XS)) -> c_14(U31^#(tt(), N))
, afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS))
, U52^#(tt(), Y) -> c_17(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_18(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_19(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_21(activate^#(X))
, U71^#(tt(), XS) ->
c_22(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_23(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_24(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_25(fst^#(splitAt(activate(N), activate(XS))),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X))
, sel^#(N, XS) -> c_29(U41^#(tt(), N, XS))
, tail^#(cons(N, XS)) ->
c_31(U71^#(tt(), activate(XS)), activate^#(XS))
, take^#(N, XS) -> c_32(U81^#(tt(), N, XS)) }
Weak DPs:
{ activate^#(X) -> c_3()
, splitAt^#(0(), XS) -> c_7()
, natsFrom^#(N) -> c_27()
, natsFrom^#(X) -> c_28()
, s^#(X) -> c_30() }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, U21(tt(), X) -> U22(tt(), activate(X))
, U22(tt(), X) -> activate(X)
, U31(tt(), N) -> U32(tt(), activate(N))
, U32(tt(), N) -> activate(N)
, U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS))
, U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
, head(cons(N, XS)) -> U31(tt(), N)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, U61(tt(), N, X, XS) ->
U62(tt(), activate(N), activate(X), activate(XS))
, U62(tt(), N, X, XS) ->
U63(tt(), activate(N), activate(X), activate(XS))
, U63(tt(), N, X, XS) ->
U64(splitAt(activate(N), activate(XS)), activate(X))
, U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
, U71(tt(), XS) -> U72(tt(), activate(XS))
, U72(tt(), XS) -> activate(XS)
, U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS))
, U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
, fst(pair(X, Y)) -> U21(tt(), X)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, sel(N, XS) -> U41(tt(), N, XS)
, s(X) -> n__s(X)
, tail(cons(N, XS)) -> U71(tt(), activate(XS))
, take(N, XS) -> U81(tt(), N, XS) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),POLY)
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ activate^#(X) -> c_3()
, splitAt^#(0(), XS) -> c_7()
, natsFrom^#(N) -> c_27()
, natsFrom^#(X) -> c_28()
, s^#(X) -> c_30() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),POLY).
Strict DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) ->
c_4(natsFrom^#(activate(X)), activate^#(X))
, activate^#(n__s(X)) -> c_5(s^#(activate(X)), activate^#(X))
, snd^#(pair(X, Y)) -> c_6(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_9(activate^#(X))
, U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_11(activate^#(N))
, U41^#(tt(), N, XS) ->
c_12(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_13(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, head^#(cons(N, XS)) -> c_14(U31^#(tt(), N))
, afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS))
, U52^#(tt(), Y) -> c_17(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_18(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_19(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_21(activate^#(X))
, U71^#(tt(), XS) ->
c_22(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_23(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_24(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_25(fst^#(splitAt(activate(N), activate(XS))),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X))
, sel^#(N, XS) -> c_29(U41^#(tt(), N, XS))
, tail^#(cons(N, XS)) ->
c_31(U71^#(tt(), activate(XS)), activate^#(XS))
, take^#(N, XS) -> c_32(U81^#(tt(), N, XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, U21(tt(), X) -> U22(tt(), activate(X))
, U22(tt(), X) -> activate(X)
, U31(tt(), N) -> U32(tt(), activate(N))
, U32(tt(), N) -> activate(N)
, U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS))
, U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
, head(cons(N, XS)) -> U31(tt(), N)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, U61(tt(), N, X, XS) ->
U62(tt(), activate(N), activate(X), activate(XS))
, U62(tt(), N, X, XS) ->
U63(tt(), activate(N), activate(X), activate(XS))
, U63(tt(), N, X, XS) ->
U64(splitAt(activate(N), activate(XS)), activate(X))
, U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
, U71(tt(), XS) -> U72(tt(), activate(XS))
, U72(tt(), XS) -> activate(XS)
, U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS))
, U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
, fst(pair(X, Y)) -> U21(tt(), X)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, sel(N, XS) -> U41(tt(), N, XS)
, s(X) -> n__s(X)
, tail(cons(N, XS)) -> U71(tt(), activate(XS))
, take(N, XS) -> U81(tt(), N, XS) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),POLY)
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) ->
c_4(natsFrom^#(activate(X)), activate^#(X))
, activate^#(n__s(X)) -> c_5(s^#(activate(X)), activate^#(X))
, U63^#(tt(), N, X, XS) ->
c_20(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U82^#(tt(), N, XS) ->
c_25(fst^#(splitAt(activate(N), activate(XS))),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),POLY).
Strict DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, sel^#(N, XS) -> c_25(U41^#(tt(), N, XS))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS))
, take^#(N, XS) -> c_27(U81^#(tt(), N, XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, U21(tt(), X) -> U22(tt(), activate(X))
, U22(tt(), X) -> activate(X)
, U31(tt(), N) -> U32(tt(), activate(N))
, U32(tt(), N) -> activate(N)
, U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS))
, U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
, head(cons(N, XS)) -> U31(tt(), N)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, U61(tt(), N, X, XS) ->
U62(tt(), activate(N), activate(X), activate(XS))
, U62(tt(), N, X, XS) ->
U63(tt(), activate(N), activate(X), activate(XS))
, U63(tt(), N, X, XS) ->
U64(splitAt(activate(N), activate(XS)), activate(X))
, U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
, U71(tt(), XS) -> U72(tt(), activate(XS))
, U72(tt(), XS) -> activate(XS)
, U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS))
, U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
, fst(pair(X, Y)) -> U21(tt(), X)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, sel(N, XS) -> U41(tt(), N, XS)
, s(X) -> n__s(X)
, tail(cons(N, XS)) -> U71(tt(), activate(XS))
, take(N, XS) -> U81(tt(), N, XS) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),POLY)
We replace rewrite rules by usable rules:
Weak Usable Rules:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),POLY).
Strict DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, sel^#(N, XS) -> c_25(U41^#(tt(), N, XS))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS))
, take^#(N, XS) -> c_27(U81^#(tt(), N, XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),POLY)
Consider the dependency graph
1: U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
-->_3 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_3 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
-->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
-->_1 U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS)) :2
2: U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
-->_1 snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y)) :5
-->_3 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_3 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
-->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
3: activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
-->_1 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_1 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
4: activate^#(n__s(X)) -> c_4(activate^#(X))
-->_1 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_1 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
5: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
-->_1 U51^#(tt(), Y) ->
c_6(U52^#(tt(), activate(Y)), activate^#(Y)) :6
6: U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
-->_1 U52^#(tt(), Y) -> c_15(activate^#(Y)) :15
-->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
7: U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
-->_1 U22^#(tt(), X) -> c_8(activate^#(X)) :8
-->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
8: U22^#(tt(), X) -> c_8(activate^#(X))
-->_1 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_1 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
9: U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
-->_1 U32^#(tt(), N) -> c_10(activate^#(N)) :10
-->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
10: U32^#(tt(), N) -> c_10(activate^#(N))
-->_1 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_1 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
11: U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
-->_1 U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS)) :12
-->_3 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_3 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
-->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
12: U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
-->_2 afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) :14
-->_1 head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) :13
-->_4 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_3 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_4 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
-->_3 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
13: head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
-->_1 U31^#(tt(), N) ->
c_9(U32^#(tt(), activate(N)), activate^#(N)) :9
14: afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS))
-->_1 U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS)) :1
15: U52^#(tt(), Y) -> c_15(activate^#(Y))
-->_1 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_1 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
16: U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
-->_1 U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS)) :17
-->_4 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_3 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_4 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
-->_3 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
-->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
17: U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
-->_1 U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X)) :18
-->_4 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_3 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_4 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
-->_3 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
-->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
18: U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
-->_1 U64^#(pair(YS, ZS), X) -> c_19(activate^#(X)) :19
-->_4 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_3 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_4 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
-->_3 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
-->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
19: U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
-->_1 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_1 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
20: U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
-->_1 U72^#(tt(), XS) -> c_21(activate^#(XS)) :21
-->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
21: U72^#(tt(), XS) -> c_21(activate^#(XS))
-->_1 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_1 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
22: U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
-->_1 U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS)) :23
-->_3 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_3 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
-->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
23: U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
-->_1 fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X)) :24
-->_3 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_3 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
-->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
24: fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
-->_1 U21^#(tt(), X) ->
c_7(U22^#(tt(), activate(X)), activate^#(X)) :7
25: sel^#(N, XS) -> c_25(U41^#(tt(), N, XS))
-->_1 U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS)) :11
26: tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS))
-->_1 U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS)) :20
-->_2 activate^#(n__s(X)) -> c_4(activate^#(X)) :4
-->_2 activate^#(n__natsFrom(X)) -> c_3(activate^#(X)) :3
27: take^#(N, XS) -> c_27(U81^#(tt(), N, XS))
-->_1 U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS)) :22
Following roots of the dependency graph are removed, as the
considered set of starting terms is closed under reduction with
respect to these rules (modulo compound contexts).
{ sel^#(N, XS) -> c_25(U41^#(tt(), N, XS))
, take^#(N, XS) -> c_27(U81^#(tt(), N, XS)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),POLY).
Strict DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),POLY)
We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict
rules from (R) into the weak component:
Problem (R):
------------
Strict DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) }
Weak DPs:
{ U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
StartTerms: basic terms
Strategy: innermost
Problem (S):
------------
Strict DPs:
{ U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
Weak DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
StartTerms: basic terms
Strategy: innermost
Overall, the transformation results in the following sub-problem(s):
Generated new problems:
-----------------------
R) Strict DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) }
Weak DPs:
{ U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
StartTerms: basic terms
Strategy: innermost
This problem was proven YES(O(1),POLY).
S) Strict DPs:
{ U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
Weak DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
StartTerms: basic terms
Strategy: innermost
This problem was proven YES(O(1),O(1)).
Proofs for generated problems:
------------------------------
R) We are left with following problem, upon which TcT provides the
certificate YES(O(1),POLY).
Strict DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) }
Weak DPs:
{ U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),POLY)
We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict
rules from (R) into the weak component:
Problem (R):
------------
Strict DPs:
{ activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS)) }
Weak DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
StartTerms: basic terms
Strategy: innermost
Problem (S):
------------
Strict DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) }
Weak DPs:
{ U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
StartTerms: basic terms
Strategy: innermost
Overall, the transformation results in the following sub-problem(s):
Generated new problems:
-----------------------
R) Strict DPs:
{ activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS)) }
Weak DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
StartTerms: basic terms
Strategy: innermost
This problem was proven YES(?,POLY).
S) Strict DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) }
Weak DPs:
{ U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
StartTerms: basic terms
Strategy: innermost
This problem was proven YES(O(1),O(1)).
Proofs for generated problems:
------------------------------
R) We are left with following problem, upon which TcT provides the
certificate YES(?,POLY).
Strict DPs:
{ activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS)) }
Weak DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
Obligation:
innermost runtime complexity
Answer:
YES(?,POLY)
The input was oriented with the instance of 'Polynomial Path Order
(PS)' as induced by the safe mapping
safe(U11) = {1}, safe(tt) = {}, safe(U12) = {1},
safe(activate) = {}, safe(snd) = {}, safe(splitAt) = {1, 2},
safe(afterNth) = {}, safe(U51) = {}, safe(U52) = {},
safe(pair) = {1, 2}, safe(cons) = {1, 2}, safe(natsFrom) = {1},
safe(n__natsFrom) = {1}, safe(n__s) = {1}, safe(0) = {},
safe(nil) = {}, safe(s) = {1}, safe(U11^#) = {}, safe(U12^#) = {},
safe(activate^#) = {}, safe(snd^#) = {}, safe(U51^#) = {},
safe(U21^#) = {1}, safe(U22^#) = {}, safe(U31^#) = {},
safe(U32^#) = {}, safe(U41^#) = {}, safe(U42^#) = {},
safe(head^#) = {}, safe(afterNth^#) = {}, safe(U52^#) = {},
safe(U61^#) = {}, safe(U62^#) = {}, safe(U63^#) = {},
safe(U64^#) = {}, safe(U71^#) = {}, safe(U72^#) = {},
safe(U81^#) = {}, safe(U82^#) = {}, safe(fst^#) = {},
safe(tail^#) = {}, safe(c_1) = {}, safe(c_2) = {}, safe(c_3) = {},
safe(c_4) = {}, safe(c_5) = {}, safe(c_6) = {}, safe(c_7) = {},
safe(c_8) = {}, safe(c_9) = {}, safe(c_10) = {}, safe(c_11) = {},
safe(c_12) = {}, safe(c_13) = {}, safe(c_14) = {}, safe(c_15) = {},
safe(c_16) = {}, safe(c_17) = {}, safe(c_18) = {}, safe(c_19) = {},
safe(c_20) = {}, safe(c_21) = {}, safe(c_22) = {}, safe(c_23) = {},
safe(c_24) = {}, safe(c_26) = {}
and precedence
U11 > U12, U11 > activate, U12 > activate, U12 > snd,
U12 > splitAt, activate > natsFrom, activate > s, snd > U51,
afterNth > U11, U51 > activate, U51 > U52, U11^# > activate,
U11^# > U12^#, U11^# > activate^#, U12^# > activate,
U12^# > splitAt, U12^# > activate^#, U12^# > snd^#, snd^# > U51^#,
U51^# > activate, U51^# > activate^#, U51^# > U52^#,
U21^# > activate, U21^# > activate^#, U21^# > U22^#,
U31^# > activate, U31^# > activate^#, U31^# > U32^#,
U41^# > activate, U41^# > activate^#, U41^# > U42^#,
U42^# > activate, U42^# > afterNth, U42^# > activate^#,
U42^# > head^#, U42^# > afterNth^#, afterNth^# > U11^#,
U61^# > activate, U61^# > activate^#, U61^# > U62^#,
U62^# > activate, U62^# > activate^#, U62^# > U63^#,
U63^# > activate, U63^# > splitAt, U63^# > activate^#,
U63^# > U64^#, U64^# > activate^#, U71^# > activate,
U71^# > activate^#, U71^# > U72^#, U72^# > activate^#,
U81^# > activate, U81^# > activate^#, U81^# > U82^#,
U82^# > activate, U82^# > splitAt, U82^# > activate^#,
U82^# > fst^#, tail^# > activate, tail^# > activate^#,
tail^# > U71^#, activate ~ U52, activate^# ~ U22^#,
activate^# ~ U32^#, activate^# ~ U52^#, U21^# ~ fst^#,
U31^# ~ head^# .
Following symbols are considered recursive:
{U11, U12, activate, snd, afterNth, U51, U52, U11^#, activate^#,
snd^#, U51^#, U21^#, U22^#, U31^#, U32^#, U41^#, U42^#, head^#,
U52^#, U61^#, U62^#, U63^#, U64^#, U71^#, U72^#, U81^#, U82^#,
fst^#, tail^#}
The recursion depth is 8.
Further, following argument filtering is employed:
pi(U11) = [1, 3], pi(tt) = [], pi(U12) = [3], pi(activate) = [1],
pi(snd) = [1], pi(splitAt) = [2], pi(afterNth) = [1, 2],
pi(U51) = [2], pi(U52) = [2], pi(pair) = [1, 2], pi(cons) = [1, 2],
pi(natsFrom) = [1], pi(n__natsFrom) = [1], pi(n__s) = [1],
pi(0) = [], pi(nil) = [], pi(s) = [1], pi(U11^#) = [2, 3],
pi(U12^#) = [2, 3], pi(activate^#) = [1], pi(snd^#) = [1],
pi(U51^#) = [2], pi(U21^#) = [1, 2], pi(U22^#) = [1, 2],
pi(U31^#) = [2], pi(U32^#) = [1, 2], pi(U41^#) = [2, 3],
pi(U42^#) = [2, 3], pi(head^#) = [1], pi(afterNth^#) = [1, 2],
pi(U52^#) = [1, 2], pi(U61^#) = [2, 3, 4],
pi(U62^#) = [1, 2, 3, 4], pi(U63^#) = [2, 3, 4], pi(U64^#) = [2],
pi(U71^#) = [1, 2], pi(U72^#) = [1, 2], pi(U81^#) = [2, 3],
pi(U82^#) = [2, 3], pi(fst^#) = [1], pi(tail^#) = [1],
pi(c_1) = [1, 2, 3], pi(c_2) = [1, 2, 3], pi(c_3) = [1],
pi(c_4) = [1], pi(c_5) = [1], pi(c_6) = [1, 2], pi(c_7) = [1, 2],
pi(c_8) = [1], pi(c_9) = [1, 2], pi(c_10) = [1],
pi(c_11) = [1, 2, 3], pi(c_12) = [1, 2, 3, 4], pi(c_13) = [1],
pi(c_14) = [1], pi(c_15) = [1], pi(c_16) = [1, 2, 3, 4],
pi(c_17) = [1, 2, 3, 4], pi(c_18) = [1, 2, 3, 4], pi(c_19) = [1],
pi(c_20) = [1, 2], pi(c_21) = [1], pi(c_22) = [1, 2, 3],
pi(c_23) = [1, 2, 3], pi(c_24) = [1], pi(c_26) = [1, 2]
Usable defined function symbols are a subset of:
{U11, U12, activate, snd, splitAt, afterNth, U51, U52, natsFrom, s,
U11^#, U12^#, activate^#, snd^#, U51^#, U21^#, U22^#, U31^#, U32^#,
U41^#, U42^#, head^#, afterNth^#, U52^#, U61^#, U62^#, U63^#,
U64^#, U71^#, U72^#, U81^#, U82^#, fst^#, tail^#}
For your convenience, here are the satisfied ordering constraints:
pi(U11^#(tt(), N, XS)) = U11^#(N, XS;)
> c_1(U12^#(activate(N;), activate(XS;);),
activate^#(N;),
activate^#(XS;);)
= pi(c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS)))
pi(U12^#(tt(), N, XS)) = U12^#(N, XS;)
> c_2(snd^#(splitAt(; activate(XS;));),
activate^#(N;),
activate^#(XS;);)
= pi(c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS)))
pi(activate^#(n__natsFrom(X))) = activate^#(n__natsFrom(; X);)
> c_3(activate^#(X;);)
= pi(c_3(activate^#(X)))
pi(activate^#(n__s(X))) = activate^#(n__s(; X);)
> c_4(activate^#(X;);)
= pi(c_4(activate^#(X)))
pi(snd^#(pair(X, Y))) = snd^#(pair(; X, Y);)
> c_5(U51^#(Y;);)
= pi(c_5(U51^#(tt(), Y)))
pi(U51^#(tt(), Y)) = U51^#(Y;)
> c_6(U52^#(tt(), activate(Y;);), activate^#(Y;);)
= pi(c_6(U52^#(tt(), activate(Y)), activate^#(Y)))
pi(U21^#(tt(), X)) = U21^#(X; tt())
> c_7(U22^#(tt(), activate(X;);), activate^#(X;);)
= pi(c_7(U22^#(tt(), activate(X)), activate^#(X)))
pi(U22^#(tt(), X)) = U22^#(tt(), X;)
> c_8(activate^#(X;);)
= pi(c_8(activate^#(X)))
pi(U31^#(tt(), N)) = U31^#(N;)
> c_9(U32^#(tt(), activate(N;);), activate^#(N;);)
= pi(c_9(U32^#(tt(), activate(N)), activate^#(N)))
pi(U32^#(tt(), N)) = U32^#(tt(), N;)
> c_10(activate^#(N;);)
= pi(c_10(activate^#(N)))
pi(U41^#(tt(), N, XS)) = U41^#(N, XS;)
> c_11(U42^#(activate(N;), activate(XS;);),
activate^#(N;),
activate^#(XS;);)
= pi(c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS)))
pi(U42^#(tt(), N, XS)) = U42^#(N, XS;)
> c_12(head^#(afterNth(activate(N;), activate(XS;););),
afterNth^#(activate(N;), activate(XS;);),
activate^#(N;),
activate^#(XS;);)
= pi(c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS)))
pi(head^#(cons(N, XS))) = head^#(cons(; N, XS);)
> c_13(U31^#(N;);)
= pi(c_13(U31^#(tt(), N)))
pi(afterNth^#(N, XS)) = afterNth^#(N, XS;)
> c_14(U11^#(N, XS;);)
= pi(c_14(U11^#(tt(), N, XS)))
pi(U52^#(tt(), Y)) = U52^#(tt(), Y;)
> c_15(activate^#(Y;);)
= pi(c_15(activate^#(Y)))
pi(U61^#(tt(), N, X, XS)) = U61^#(N, X, XS;)
> c_16(U62^#(tt(), activate(N;), activate(X;), activate(XS;);),
activate^#(N;),
activate^#(X;),
activate^#(XS;);)
= pi(c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS)))
pi(U62^#(tt(), N, X, XS)) = U62^#(tt(), N, X, XS;)
> c_17(U63^#(activate(N;), activate(X;), activate(XS;);),
activate^#(N;),
activate^#(X;),
activate^#(XS;);)
= pi(c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS)))
pi(U63^#(tt(), N, X, XS)) = U63^#(N, X, XS;)
> c_18(U64^#(activate(X;);),
activate^#(N;),
activate^#(XS;),
activate^#(X;);)
= pi(c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X)))
pi(U64^#(pair(YS, ZS), X)) = U64^#(X;)
> c_19(activate^#(X;);)
= pi(c_19(activate^#(X)))
pi(U71^#(tt(), XS)) = U71^#(tt(), XS;)
> c_20(U72^#(tt(), activate(XS;);), activate^#(XS;);)
= pi(c_20(U72^#(tt(), activate(XS)), activate^#(XS)))
pi(U72^#(tt(), XS)) = U72^#(tt(), XS;)
> c_21(activate^#(XS;);)
= pi(c_21(activate^#(XS)))
pi(U81^#(tt(), N, XS)) = U81^#(N, XS;)
> c_22(U82^#(activate(N;), activate(XS;);),
activate^#(N;),
activate^#(XS;);)
= pi(c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS)))
pi(U82^#(tt(), N, XS)) = U82^#(N, XS;)
> c_23(fst^#(splitAt(; activate(XS;));),
activate^#(N;),
activate^#(XS;);)
= pi(c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS)))
pi(fst^#(pair(X, Y))) = fst^#(pair(; X, Y);)
> c_24(U21^#(X; tt());)
= pi(c_24(U21^#(tt(), X)))
pi(tail^#(cons(N, XS))) = tail^#(cons(; N, XS);)
> c_26(U71^#(tt(), activate(XS;);), activate^#(XS;);)
= pi(c_26(U71^#(tt(), activate(XS)), activate^#(XS)))
pi(U11(tt(), N, XS)) = U11(XS; tt())
> U12(activate(XS;);)
= pi(U12(tt(), activate(N), activate(XS)))
pi(U12(tt(), N, XS)) = U12(XS;)
> snd(splitAt(; activate(XS;));)
= pi(snd(splitAt(activate(N), activate(XS))))
pi(activate(X)) = activate(X;)
> X
= pi(X)
pi(activate(n__natsFrom(X))) = activate(n__natsFrom(; X);)
> natsFrom(; activate(X;))
= pi(natsFrom(activate(X)))
pi(activate(n__s(X))) = activate(n__s(; X);)
> s(; activate(X;))
= pi(s(activate(X)))
pi(snd(pair(X, Y))) = snd(pair(; X, Y);)
> U51(Y;)
= pi(U51(tt(), Y))
pi(splitAt(0(), XS)) = splitAt(; XS)
> pair(; nil(), XS)
= pi(pair(nil(), XS))
pi(afterNth(N, XS)) = afterNth(N, XS;)
> U11(XS; tt())
= pi(U11(tt(), N, XS))
pi(U51(tt(), Y)) = U51(Y;)
> U52(activate(Y;);)
= pi(U52(tt(), activate(Y)))
pi(U52(tt(), Y)) = U52(Y;)
>= activate(Y;)
= pi(activate(Y))
pi(natsFrom(N)) = natsFrom(; N)
> cons(; N, n__natsFrom(; n__s(; N)))
= pi(cons(N, n__natsFrom(n__s(N))))
pi(natsFrom(X)) = natsFrom(; X)
> n__natsFrom(; X)
= pi(n__natsFrom(X))
pi(s(X)) = s(; X)
> n__s(; X)
= pi(n__s(X))
S) We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) }
Weak DPs:
{ U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
We estimate the number of application of {1} by applications of
Pre({1}) = {2}. Here rules are labeled as follows:
DPs:
{ 1: U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 2: afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS))
, 3: U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, 4: activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, 5: activate^#(n__s(X)) -> c_4(activate^#(X))
, 6: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, 7: U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, 8: U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, 9: U22^#(tt(), X) -> c_8(activate^#(X))
, 10: U31^#(tt(), N) ->
c_9(U32^#(tt(), activate(N)), activate^#(N))
, 11: U32^#(tt(), N) -> c_10(activate^#(N))
, 12: U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 13: U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 14: head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, 15: U52^#(tt(), Y) -> c_15(activate^#(Y))
, 16: U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 17: U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 18: U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, 19: U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, 20: U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, 21: U72^#(tt(), XS) -> c_21(activate^#(XS))
, 22: U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 23: U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, 24: fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, 25: tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs: { afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) }
Weak DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
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.
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs: { afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) }
Weak DPs:
{ U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs: { afterNth^#(N, XS) -> c_1() }
Weak DPs:
{ U41^#(tt(), N, XS) -> c_2(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) ->
c_3(afterNth^#(activate(N), activate(XS))) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
We replace rewrite rules by usable rules:
Weak Usable Rules:
{ activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs: { afterNth^#(N, XS) -> c_1() }
Weak DPs:
{ U41^#(tt(), N, XS) -> c_2(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) ->
c_3(afterNth^#(activate(N), activate(XS))) }
Weak Trs:
{ activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
The dependency graph contains no loops, we remove all dependency
pairs.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
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
S) We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
Weak DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
We estimate the number of application of {5,7,9,13,15} by
applications of Pre({5,7,9,13,15}) = {3,4,6,12,14}. Here rules are
labeled as follows:
DPs:
{ 1: U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, 2: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, 3: U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, 4: U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, 5: U22^#(tt(), X) -> c_8(activate^#(X))
, 6: U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, 7: U32^#(tt(), N) -> c_10(activate^#(N))
, 8: head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, 9: U52^#(tt(), Y) -> c_15(activate^#(Y))
, 10: U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 11: U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 12: U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, 13: U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, 14: U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, 15: U72^#(tt(), XS) -> c_21(activate^#(XS))
, 16: U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 17: U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, 18: fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, 19: tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS))
, 20: U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 21: activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, 22: activate^#(n__s(X)) -> c_4(activate^#(X))
, 23: U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 24: U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 25: afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
Weak DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U32^#(tt(), N) -> c_10(activate^#(N))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U72^#(tt(), XS) -> c_21(activate^#(XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
We estimate the number of application of {3,4,5,9,10} by
applications of Pre({3,4,5,9,10}) = {2,6,8,13,14}. Here rules are
labeled as follows:
DPs:
{ 1: U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, 2: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, 3: U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, 4: U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, 5: U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, 6: head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, 7: U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 8: U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 9: U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, 10: U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, 11: U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 12: U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, 13: fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, 14: tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS))
, 15: U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 16: activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, 17: activate^#(n__s(X)) -> c_4(activate^#(X))
, 18: U22^#(tt(), X) -> c_8(activate^#(X))
, 19: U32^#(tt(), N) -> c_10(activate^#(N))
, 20: U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 21: U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 22: afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS))
, 23: U52^#(tt(), Y) -> c_15(activate^#(Y))
, 24: U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, 25: U72^#(tt(), XS) -> c_21(activate^#(XS)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
Weak DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
We estimate the number of application of {2,5,8,9} by applications
of Pre({2,5,8,9}) = {1,4,7}. Here rules are labeled as follows:
DPs:
{ 1: U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, 2: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, 3: head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, 4: U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 5: U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 6: U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 7: U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, 8: fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, 9: tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS))
, 10: U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 11: activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, 12: activate^#(n__s(X)) -> c_4(activate^#(X))
, 13: U51^#(tt(), Y) ->
c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, 14: U21^#(tt(), X) ->
c_7(U22^#(tt(), activate(X)), activate^#(X))
, 15: U22^#(tt(), X) -> c_8(activate^#(X))
, 16: U31^#(tt(), N) ->
c_9(U32^#(tt(), activate(N)), activate^#(N))
, 17: U32^#(tt(), N) -> c_10(activate^#(N))
, 18: U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 19: U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 20: afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS))
, 21: U52^#(tt(), Y) -> c_15(activate^#(Y))
, 22: U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, 23: U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, 24: U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, 25: U72^#(tt(), XS) -> c_21(activate^#(XS)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS)) }
Weak DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
We estimate the number of application of {3,5} by applications of
Pre({3,5}) = {4}. Here rules are labeled as follows:
DPs:
{ 1: U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, 2: head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, 3: U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 4: U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 5: U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, 6: U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 7: activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, 8: activate^#(n__s(X)) -> c_4(activate^#(X))
, 9: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, 10: U51^#(tt(), Y) ->
c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, 11: U21^#(tt(), X) ->
c_7(U22^#(tt(), activate(X)), activate^#(X))
, 12: U22^#(tt(), X) -> c_8(activate^#(X))
, 13: U31^#(tt(), N) ->
c_9(U32^#(tt(), activate(N)), activate^#(N))
, 14: U32^#(tt(), N) -> c_10(activate^#(N))
, 15: U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 16: U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 17: afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS))
, 18: U52^#(tt(), Y) -> c_15(activate^#(Y))
, 19: U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 20: U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, 21: U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, 22: U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, 23: U72^#(tt(), XS) -> c_21(activate^#(XS))
, 24: fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, 25: tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS)) }
Weak DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
We estimate the number of application of {3} by applications of
Pre({3}) = {}. Here rules are labeled as follows:
DPs:
{ 1: U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, 2: head^#(cons(N, XS)) -> c_13(U31^#(tt(), N))
, 3: U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 4: U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 5: activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, 6: activate^#(n__s(X)) -> c_4(activate^#(X))
, 7: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, 8: U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, 9: U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, 10: U22^#(tt(), X) -> c_8(activate^#(X))
, 11: U31^#(tt(), N) ->
c_9(U32^#(tt(), activate(N)), activate^#(N))
, 12: U32^#(tt(), N) -> c_10(activate^#(N))
, 13: U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 14: U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 15: afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS))
, 16: U52^#(tt(), Y) -> c_15(activate^#(Y))
, 17: U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 18: U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 19: U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, 20: U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, 21: U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, 22: U72^#(tt(), XS) -> c_21(activate^#(XS))
, 23: U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, 24: fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, 25: tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) }
Weak DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
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.
{ activate^#(n__natsFrom(X)) -> c_3(activate^#(X))
, activate^#(n__s(X)) -> c_4(activate^#(X))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, U51^#(tt(), Y) -> c_6(U52^#(tt(), activate(Y)), activate^#(Y))
, U21^#(tt(), X) -> c_7(U22^#(tt(), activate(X)), activate^#(X))
, U22^#(tt(), X) -> c_8(activate^#(X))
, U31^#(tt(), N) -> c_9(U32^#(tt(), activate(N)), activate^#(N))
, U32^#(tt(), N) -> c_10(activate^#(N))
, U52^#(tt(), Y) -> c_15(activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_16(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U62^#(tt(), N, X, XS) ->
c_17(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U63^#(tt(), N, X, XS) ->
c_18(U64^#(splitAt(activate(N), activate(XS)), activate(X)),
activate^#(N),
activate^#(XS),
activate^#(X))
, U64^#(pair(YS, ZS), X) -> c_19(activate^#(X))
, U71^#(tt(), XS) ->
c_20(U72^#(tt(), activate(XS)), activate^#(XS))
, U72^#(tt(), XS) -> c_21(activate^#(XS))
, U81^#(tt(), N, XS) ->
c_22(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U82^#(tt(), N, XS) ->
c_23(fst^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_26(U71^#(tt(), activate(XS)), activate^#(XS)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) }
Weak DPs:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, afterNth^#(N, XS) -> c_14(U11^#(tt(), N, XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U12^#(tt(), N, XS) ->
c_2(snd^#(splitAt(activate(N), activate(XS))),
activate^#(N),
activate^#(XS))
, U41^#(tt(), N, XS) ->
c_11(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, U42^#(tt(), N, XS) ->
c_12(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, head^#(cons(N, XS)) -> c_13(U31^#(tt(), N)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ U12^#(tt(), N, XS) -> c_1()
, head^#(cons(N, XS)) -> c_2() }
Weak DPs:
{ U11^#(tt(), N, XS) -> c_3(U12^#(tt(), activate(N), activate(XS)))
, U41^#(tt(), N, XS) -> c_4(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) ->
c_5(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_6(U11^#(tt(), N, XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict
rules from (R) into the weak component:
Problem (R):
------------
Strict DPs: { U12^#(tt(), N, XS) -> c_1() }
Weak DPs:
{ U11^#(tt(), N, XS) -> c_3(U12^#(tt(), activate(N), activate(XS)))
, U41^#(tt(), N, XS) -> c_4(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) ->
c_5(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)))
, head^#(cons(N, XS)) -> c_2()
, afterNth^#(N, XS) -> c_6(U11^#(tt(), N, XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
StartTerms: basic terms
Strategy: innermost
Problem (S):
------------
Strict DPs: { head^#(cons(N, XS)) -> c_2() }
Weak DPs:
{ U11^#(tt(), N, XS) -> c_3(U12^#(tt(), activate(N), activate(XS)))
, U12^#(tt(), N, XS) -> c_1()
, U41^#(tt(), N, XS) -> c_4(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) ->
c_5(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_6(U11^#(tt(), N, XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
StartTerms: basic terms
Strategy: innermost
Overall, the transformation results in the following sub-problem(s):
Generated new problems:
-----------------------
R) Strict DPs: { U12^#(tt(), N, XS) -> c_1() }
Weak DPs:
{ U11^#(tt(), N, XS) -> c_3(U12^#(tt(), activate(N), activate(XS)))
, U41^#(tt(), N, XS) -> c_4(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) ->
c_5(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)))
, head^#(cons(N, XS)) -> c_2()
, afterNth^#(N, XS) -> c_6(U11^#(tt(), N, XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
StartTerms: basic terms
Strategy: innermost
This problem was proven YES(O(1),O(1)).
S) Strict DPs: { head^#(cons(N, XS)) -> c_2() }
Weak DPs:
{ U11^#(tt(), N, XS) -> c_3(U12^#(tt(), activate(N), activate(XS)))
, U12^#(tt(), N, XS) -> c_1()
, U41^#(tt(), N, XS) -> c_4(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) ->
c_5(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_6(U11^#(tt(), N, XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
StartTerms: basic terms
Strategy: innermost
This problem was proven YES(O(1),O(1)).
Proofs for generated problems:
------------------------------
R) We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs: { U12^#(tt(), N, XS) -> c_1() }
Weak DPs:
{ U11^#(tt(), N, XS) -> c_3(U12^#(tt(), activate(N), activate(XS)))
, U41^#(tt(), N, XS) -> c_4(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) ->
c_5(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)))
, head^#(cons(N, XS)) -> c_2()
, afterNth^#(N, XS) -> c_6(U11^#(tt(), N, XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
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.
{ head^#(cons(N, XS)) -> c_2() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs: { U12^#(tt(), N, XS) -> c_1() }
Weak DPs:
{ U11^#(tt(), N, XS) -> c_3(U12^#(tt(), activate(N), activate(XS)))
, U41^#(tt(), N, XS) -> c_4(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) ->
c_5(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_6(U11^#(tt(), N, XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ U42^#(tt(), N, XS) ->
c_5(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs: { U12^#(tt(), N, XS) -> c_1() }
Weak DPs:
{ U11^#(tt(), N, XS) -> c_2(U12^#(tt(), activate(N), activate(XS)))
, U41^#(tt(), N, XS) -> c_3(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) -> c_4(afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_5(U11^#(tt(), N, XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
We replace rewrite rules by usable rules:
Weak Usable Rules:
{ activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs: { U12^#(tt(), N, XS) -> c_1() }
Weak DPs:
{ U11^#(tt(), N, XS) -> c_2(U12^#(tt(), activate(N), activate(XS)))
, U41^#(tt(), N, XS) -> c_3(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) -> c_4(afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_5(U11^#(tt(), N, XS)) }
Weak Trs:
{ activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
The dependency graph contains no loops, we remove all dependency
pairs.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
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
S) We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs: { head^#(cons(N, XS)) -> c_2() }
Weak DPs:
{ U11^#(tt(), N, XS) -> c_3(U12^#(tt(), activate(N), activate(XS)))
, U12^#(tt(), N, XS) -> c_1()
, U41^#(tt(), N, XS) -> c_4(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) ->
c_5(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_6(U11^#(tt(), N, XS)) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
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.
{ U11^#(tt(), N, XS) -> c_3(U12^#(tt(), activate(N), activate(XS)))
, U12^#(tt(), N, XS) -> c_1()
, afterNth^#(N, XS) -> c_6(U11^#(tt(), N, XS)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs: { head^#(cons(N, XS)) -> c_2() }
Weak DPs:
{ U41^#(tt(), N, XS) -> c_4(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) ->
c_5(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS))) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ U42^#(tt(), N, XS) ->
c_5(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs: { head^#(cons(N, XS)) -> c_1() }
Weak DPs:
{ U41^#(tt(), N, XS) -> c_2(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) ->
c_3(head^#(afterNth(activate(N), activate(XS)))) }
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
The dependency graph contains no loops, we remove all dependency
pairs.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS))
, U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
, activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(activate(X))
, activate(n__s(X)) -> s(activate(X))
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(0(), XS) -> pair(nil(), XS)
, afterNth(N, XS) -> U11(tt(), N, XS)
, U51(tt(), Y) -> U52(tt(), activate(Y))
, U52(tt(), Y) -> activate(Y)
, natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
, natsFrom(X) -> n__natsFrom(X)
, s(X) -> n__s(X) }
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),POLY)