We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
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(X)
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS))
, 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(s(N)))
, natsFrom(X) -> n__natsFrom(X)
, sel(N, XS) -> U41(tt(), N, XS)
, tail(cons(N, XS)) -> U71(tt(), activate(XS))
, take(N, XS) -> U81(tt(), N, XS) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
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^#(X))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, splitAt^#(s(N), cons(X, XS)) ->
c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS))
, splitAt^#(0(), XS) -> c_7()
, natsFrom^#(N) -> c_27()
, natsFrom^#(X) -> c_28()
, U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_18(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 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))
, 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_30(U71^#(tt(), activate(XS)), activate^#(XS))
, take^#(N, XS) -> c_31(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),O(n^1)).
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^#(X))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, splitAt^#(s(N), cons(X, XS)) ->
c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS))
, splitAt^#(0(), XS) -> c_7()
, natsFrom^#(N) -> c_27()
, natsFrom^#(X) -> c_28()
, U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_18(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 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))
, 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_30(U71^#(tt(), activate(XS)), activate^#(XS))
, take^#(N, XS) -> c_31(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(X)
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS))
, 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(s(N)))
, natsFrom(X) -> n__natsFrom(X)
, sel(N, XS) -> U41(tt(), N, XS)
, tail(cons(N, XS)) -> U71(tt(), activate(XS))
, take(N, XS) -> U81(tt(), N, XS) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of {3,7,8,9} by applications
of Pre({3,7,8,9}) =
{1,2,4,6,10,11,12,13,14,15,16,17,20,21,22,23,24,25,26,27,30}. 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^#(X))
, 5: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, 6: splitAt^#(s(N), cons(X, XS)) ->
c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS))
, 7: splitAt^#(0(), XS) -> c_7()
, 8: natsFrom^#(N) -> c_27()
, 9: natsFrom^#(X) -> c_28()
, 10: U51^#(tt(), Y) ->
c_16(U52^#(tt(), activate(Y)), activate^#(Y))
, 11: U61^#(tt(), N, X, XS) ->
c_18(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 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: U62^#(tt(), N, X, XS) ->
c_19(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 22: 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))
, 23: U64^#(pair(YS, ZS), X) -> c_21(activate^#(X))
, 24: U71^#(tt(), XS) ->
c_22(U72^#(tt(), activate(XS)), activate^#(XS))
, 25: U72^#(tt(), XS) -> c_23(activate^#(XS))
, 26: U81^#(tt(), N, XS) ->
c_24(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 27: U82^#(tt(), N, XS) ->
c_25(fst^#(splitAt(activate(N), activate(XS))),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 28: fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X))
, 29: sel^#(N, XS) -> c_29(U41^#(tt(), N, XS))
, 30: tail^#(cons(N, XS)) ->
c_30(U71^#(tt(), activate(XS)), activate^#(XS))
, 31: take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
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^#(X))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, splitAt^#(s(N), cons(X, XS)) ->
c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS))
, U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_18(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 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))
, 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_30(U71^#(tt(), activate(XS)), activate^#(XS))
, take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) }
Weak DPs:
{ activate^#(X) -> c_3()
, splitAt^#(0(), XS) -> c_7()
, natsFrom^#(N) -> c_27()
, natsFrom^#(X) -> c_28() }
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(X)
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS))
, 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(s(N)))
, natsFrom(X) -> n__natsFrom(X)
, sel(N, XS) -> U41(tt(), N, XS)
, tail(cons(N, XS)) -> U71(tt(), activate(XS))
, take(N, XS) -> U81(tt(), N, XS) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of {3} by applications of
Pre({3}) = {1,2,5,6,7,8,9,10,11,12,13,16,17,18,19,20,21,22,23,26}.
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^#(n__natsFrom(X)) -> c_4(natsFrom^#(X))
, 4: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, 5: splitAt^#(s(N), cons(X, XS)) ->
c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS))
, 6: U51^#(tt(), Y) ->
c_16(U52^#(tt(), activate(Y)), activate^#(Y))
, 7: U61^#(tt(), N, X, XS) ->
c_18(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 8: U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X))
, 9: U22^#(tt(), X) -> c_9(activate^#(X))
, 10: U31^#(tt(), N) ->
c_10(U32^#(tt(), activate(N)), activate^#(N))
, 11: U32^#(tt(), N) -> c_11(activate^#(N))
, 12: U41^#(tt(), N, XS) ->
c_12(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 13: U42^#(tt(), N, XS) ->
c_13(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 14: head^#(cons(N, XS)) -> c_14(U31^#(tt(), N))
, 15: afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS))
, 16: U52^#(tt(), Y) -> c_17(activate^#(Y))
, 17: U62^#(tt(), N, X, XS) ->
c_19(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 18: 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))
, 19: U64^#(pair(YS, ZS), X) -> c_21(activate^#(X))
, 20: U71^#(tt(), XS) ->
c_22(U72^#(tt(), activate(XS)), activate^#(XS))
, 21: U72^#(tt(), XS) -> c_23(activate^#(XS))
, 22: U81^#(tt(), N, XS) ->
c_24(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 23: U82^#(tt(), N, XS) ->
c_25(fst^#(splitAt(activate(N), activate(XS))),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 24: fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X))
, 25: sel^#(N, XS) -> c_29(U41^#(tt(), N, XS))
, 26: tail^#(cons(N, XS)) ->
c_30(U71^#(tt(), activate(XS)), activate^#(XS))
, 27: take^#(N, XS) -> c_31(U81^#(tt(), N, XS))
, 28: activate^#(X) -> c_3()
, 29: splitAt^#(0(), XS) -> c_7()
, 30: natsFrom^#(N) -> c_27()
, 31: natsFrom^#(X) -> c_28() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
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))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, splitAt^#(s(N), cons(X, XS)) ->
c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS))
, U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_18(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 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))
, 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_30(U71^#(tt(), activate(XS)), activate^#(XS))
, take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) }
Weak DPs:
{ activate^#(X) -> c_3()
, activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X))
, splitAt^#(0(), XS) -> c_7()
, natsFrom^#(N) -> c_27()
, natsFrom^#(X) -> c_28() }
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(X)
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS))
, 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(s(N)))
, natsFrom(X) -> n__natsFrom(X)
, sel(N, XS) -> U41(tt(), N, XS)
, tail(cons(N, XS)) -> U71(tt(), activate(XS))
, take(N, XS) -> U81(tt(), N, XS) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of {8,10,15,18,20} by
applications of Pre({8,10,15,18,20}) = {5,7,9,17,19}. 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: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, 4: splitAt^#(s(N), cons(X, XS)) ->
c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS))
, 5: U51^#(tt(), Y) ->
c_16(U52^#(tt(), activate(Y)), activate^#(Y))
, 6: U61^#(tt(), N, X, XS) ->
c_18(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 7: U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X))
, 8: U22^#(tt(), X) -> c_9(activate^#(X))
, 9: U31^#(tt(), N) ->
c_10(U32^#(tt(), activate(N)), activate^#(N))
, 10: U32^#(tt(), N) -> c_11(activate^#(N))
, 11: U41^#(tt(), N, XS) ->
c_12(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 12: U42^#(tt(), N, XS) ->
c_13(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 13: head^#(cons(N, XS)) -> c_14(U31^#(tt(), N))
, 14: afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS))
, 15: U52^#(tt(), Y) -> c_17(activate^#(Y))
, 16: U62^#(tt(), N, X, XS) ->
c_19(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 17: 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))
, 18: U64^#(pair(YS, ZS), X) -> c_21(activate^#(X))
, 19: U71^#(tt(), XS) ->
c_22(U72^#(tt(), activate(XS)), activate^#(XS))
, 20: U72^#(tt(), XS) -> c_23(activate^#(XS))
, 21: U81^#(tt(), N, XS) ->
c_24(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 22: U82^#(tt(), N, XS) ->
c_25(fst^#(splitAt(activate(N), activate(XS))),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 23: fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X))
, 24: sel^#(N, XS) -> c_29(U41^#(tt(), N, XS))
, 25: tail^#(cons(N, XS)) ->
c_30(U71^#(tt(), activate(XS)), activate^#(XS))
, 26: take^#(N, XS) -> c_31(U81^#(tt(), N, XS))
, 27: activate^#(X) -> c_3()
, 28: activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X))
, 29: splitAt^#(0(), XS) -> c_7()
, 30: natsFrom^#(N) -> c_27()
, 31: natsFrom^#(X) -> c_28() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
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))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, splitAt^#(s(N), cons(X, XS)) ->
c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS))
, U51^#(tt(), Y) -> c_16(U52^#(tt(), activate(Y)), activate^#(Y))
, U61^#(tt(), N, X, XS) ->
c_18(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X))
, U31^#(tt(), N) -> c_10(U32^#(tt(), activate(N)), 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))
, 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))
, U71^#(tt(), XS) ->
c_22(U72^#(tt(), activate(XS)), 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_30(U71^#(tt(), activate(XS)), activate^#(XS))
, take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) }
Weak DPs:
{ activate^#(X) -> c_3()
, activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X))
, splitAt^#(0(), XS) -> c_7()
, natsFrom^#(N) -> c_27()
, natsFrom^#(X) -> c_28()
, U22^#(tt(), X) -> c_9(activate^#(X))
, U32^#(tt(), N) -> c_11(activate^#(N))
, U52^#(tt(), Y) -> c_17(activate^#(Y))
, U64^#(pair(YS, ZS), X) -> c_21(activate^#(X))
, U72^#(tt(), XS) -> c_23(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(X)
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS))
, 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(s(N)))
, natsFrom(X) -> n__natsFrom(X)
, sel(N, XS) -> U41(tt(), N, XS)
, tail(cons(N, XS)) -> U71(tt(), activate(XS))
, take(N, XS) -> U81(tt(), N, XS) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of {5,7,8,15} by applications
of Pre({5,7,8,15}) = {3,11,18,20}. 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: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, 4: splitAt^#(s(N), cons(X, XS)) ->
c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS))
, 5: U51^#(tt(), Y) ->
c_16(U52^#(tt(), activate(Y)), activate^#(Y))
, 6: U61^#(tt(), N, X, XS) ->
c_18(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 7: U21^#(tt(), X) -> c_8(U22^#(tt(), activate(X)), activate^#(X))
, 8: U31^#(tt(), N) ->
c_10(U32^#(tt(), activate(N)), activate^#(N))
, 9: U41^#(tt(), N, XS) ->
c_12(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 10: U42^#(tt(), N, XS) ->
c_13(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 11: head^#(cons(N, XS)) -> c_14(U31^#(tt(), N))
, 12: afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS))
, 13: U62^#(tt(), N, X, XS) ->
c_19(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 14: 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))
, 15: U71^#(tt(), XS) ->
c_22(U72^#(tt(), activate(XS)), activate^#(XS))
, 16: U81^#(tt(), N, XS) ->
c_24(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 17: U82^#(tt(), N, XS) ->
c_25(fst^#(splitAt(activate(N), activate(XS))),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 18: fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X))
, 19: sel^#(N, XS) -> c_29(U41^#(tt(), N, XS))
, 20: tail^#(cons(N, XS)) ->
c_30(U71^#(tt(), activate(XS)), activate^#(XS))
, 21: take^#(N, XS) -> c_31(U81^#(tt(), N, XS))
, 22: activate^#(X) -> c_3()
, 23: activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X))
, 24: splitAt^#(0(), XS) -> c_7()
, 25: natsFrom^#(N) -> c_27()
, 26: natsFrom^#(X) -> c_28()
, 27: U22^#(tt(), X) -> c_9(activate^#(X))
, 28: U32^#(tt(), N) -> c_11(activate^#(N))
, 29: U52^#(tt(), Y) -> c_17(activate^#(Y))
, 30: U64^#(pair(YS, ZS), X) -> c_21(activate^#(X))
, 31: U72^#(tt(), XS) -> c_23(activate^#(XS)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
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))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, splitAt^#(s(N), cons(X, XS)) ->
c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS))
, U61^#(tt(), N, X, XS) ->
c_18(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 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))
, 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))
, 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_30(U71^#(tt(), activate(XS)), activate^#(XS))
, take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) }
Weak DPs:
{ activate^#(X) -> c_3()
, activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X))
, splitAt^#(0(), XS) -> c_7()
, natsFrom^#(N) -> c_27()
, natsFrom^#(X) -> c_28()
, 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))
, U52^#(tt(), Y) -> c_17(activate^#(Y))
, 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)) }
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(X)
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS))
, 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(s(N)))
, natsFrom(X) -> n__natsFrom(X)
, sel(N, XS) -> U41(tt(), N, XS)
, tail(cons(N, XS)) -> U71(tt(), activate(XS))
, take(N, XS) -> U81(tt(), N, XS) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of {3,8,14,16} by
applications of Pre({3,8,14,16}) = {2,7,13}. 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: snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, 4: splitAt^#(s(N), cons(X, XS)) ->
c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS))
, 5: U61^#(tt(), N, X, XS) ->
c_18(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 6: U41^#(tt(), N, XS) ->
c_12(U42^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 7: U42^#(tt(), N, XS) ->
c_13(head^#(afterNth(activate(N), activate(XS))),
afterNth^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 8: head^#(cons(N, XS)) -> c_14(U31^#(tt(), N))
, 9: afterNth^#(N, XS) -> c_15(U11^#(tt(), N, XS))
, 10: U62^#(tt(), N, X, XS) ->
c_19(U63^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 11: 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))
, 12: U81^#(tt(), N, XS) ->
c_24(U82^#(tt(), activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 13: U82^#(tt(), N, XS) ->
c_25(fst^#(splitAt(activate(N), activate(XS))),
splitAt^#(activate(N), activate(XS)),
activate^#(N),
activate^#(XS))
, 14: fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X))
, 15: sel^#(N, XS) -> c_29(U41^#(tt(), N, XS))
, 16: tail^#(cons(N, XS)) ->
c_30(U71^#(tt(), activate(XS)), activate^#(XS))
, 17: take^#(N, XS) -> c_31(U81^#(tt(), N, XS))
, 18: activate^#(X) -> c_3()
, 19: activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X))
, 20: splitAt^#(0(), XS) -> c_7()
, 21: natsFrom^#(N) -> c_27()
, 22: natsFrom^#(X) -> c_28()
, 23: U51^#(tt(), Y) ->
c_16(U52^#(tt(), activate(Y)), activate^#(Y))
, 24: U21^#(tt(), X) ->
c_8(U22^#(tt(), activate(X)), activate^#(X))
, 25: U22^#(tt(), X) -> c_9(activate^#(X))
, 26: U31^#(tt(), N) ->
c_10(U32^#(tt(), activate(N)), activate^#(N))
, 27: U32^#(tt(), N) -> c_11(activate^#(N))
, 28: U52^#(tt(), Y) -> c_17(activate^#(Y))
, 29: U64^#(pair(YS, ZS), X) -> c_21(activate^#(X))
, 30: U71^#(tt(), XS) ->
c_22(U72^#(tt(), activate(XS)), activate^#(XS))
, 31: U72^#(tt(), XS) -> c_23(activate^#(XS)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
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))
, splitAt^#(s(N), cons(X, XS)) ->
c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS))
, U61^#(tt(), N, X, XS) ->
c_18(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 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))
, afterNth^#(N, XS) -> c_15(U11^#(tt(), N, 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))
, 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))
, sel^#(N, XS) -> c_29(U41^#(tt(), N, XS))
, take^#(N, XS) -> c_31(U81^#(tt(), N, XS)) }
Weak DPs:
{ activate^#(X) -> c_3()
, activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, splitAt^#(0(), XS) -> c_7()
, natsFrom^#(N) -> c_27()
, natsFrom^#(X) -> c_28()
, 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))
, head^#(cons(N, XS)) -> c_14(U31^#(tt(), N))
, U52^#(tt(), Y) -> c_17(activate^#(Y))
, 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))
, fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_30(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(X)
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS))
, 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(s(N)))
, natsFrom(X) -> n__natsFrom(X)
, sel(N, XS) -> U41(tt(), N, XS)
, tail(cons(N, XS)) -> U71(tt(), activate(XS))
, take(N, XS) -> U81(tt(), N, XS) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ activate^#(X) -> c_3()
, activate^#(n__natsFrom(X)) -> c_4(natsFrom^#(X))
, snd^#(pair(X, Y)) -> c_5(U51^#(tt(), Y))
, splitAt^#(0(), XS) -> c_7()
, natsFrom^#(N) -> c_27()
, natsFrom^#(X) -> c_28()
, 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))
, head^#(cons(N, XS)) -> c_14(U31^#(tt(), N))
, U52^#(tt(), Y) -> c_17(activate^#(Y))
, 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))
, fst^#(pair(X, Y)) -> c_26(U21^#(tt(), X))
, tail^#(cons(N, XS)) ->
c_30(U71^#(tt(), activate(XS)), activate^#(XS)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
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))
, splitAt^#(s(N), cons(X, XS)) ->
c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS))
, U61^#(tt(), N, X, XS) ->
c_18(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 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))
, afterNth^#(N, XS) -> c_15(U11^#(tt(), N, 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))
, 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))
, sel^#(N, XS) -> c_29(U41^#(tt(), N, XS))
, take^#(N, XS) -> c_31(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(X)
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS))
, 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(s(N)))
, natsFrom(X) -> n__natsFrom(X)
, sel(N, XS) -> U41(tt(), N, XS)
, tail(cons(N, XS)) -> U71(tt(), activate(XS))
, take(N, XS) -> U81(tt(), N, XS) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ 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))
, splitAt^#(s(N), cons(X, XS)) ->
c_6(U61^#(tt(), N, X, activate(XS)), activate^#(XS))
, U61^#(tt(), N, X, XS) ->
c_18(U62^#(tt(), activate(N), activate(X), activate(XS)),
activate^#(N),
activate^#(X),
activate^#(XS))
, 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))
, 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))
, 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)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)))
, U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS)))
, splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS)))
, U61^#(tt(), N, X, XS) ->
c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))
, U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
, U62^#(tt(), N, X, XS) ->
c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))
, U63^#(tt(), N, X, XS) ->
c_9(splitAt^#(activate(N), activate(XS)))
, U81^#(tt(), N, XS) ->
c_10(U82^#(tt(), activate(N), activate(XS)))
, U82^#(tt(), N, XS) -> c_11(splitAt^#(activate(N), activate(XS)))
, sel^#(N, XS) -> c_12(U41^#(tt(), N, XS))
, take^#(N, XS) -> c_13(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(X)
, snd(pair(X, Y)) -> U51(tt(), Y)
, splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS))
, 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(s(N)))
, natsFrom(X) -> n__natsFrom(X)
, sel(N, XS) -> U41(tt(), N, XS)
, tail(cons(N, XS)) -> U71(tt(), activate(XS))
, take(N, XS) -> U81(tt(), N, XS) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We replace rewrite rules by usable rules:
Weak Usable Rules:
{ activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(X)
, natsFrom(N) -> cons(N, n__natsFrom(s(N)))
, natsFrom(X) -> n__natsFrom(X) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)))
, U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS)))
, splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS)))
, U61^#(tt(), N, X, XS) ->
c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))
, U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
, U62^#(tt(), N, X, XS) ->
c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))
, U63^#(tt(), N, X, XS) ->
c_9(splitAt^#(activate(N), activate(XS)))
, U81^#(tt(), N, XS) ->
c_10(U82^#(tt(), activate(N), activate(XS)))
, U82^#(tt(), N, XS) -> c_11(splitAt^#(activate(N), activate(XS)))
, sel^#(N, XS) -> c_12(U41^#(tt(), N, XS))
, take^#(N, XS) -> c_13(U81^#(tt(), N, XS)) }
Weak Trs:
{ activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(X)
, natsFrom(N) -> cons(N, n__natsFrom(s(N)))
, natsFrom(X) -> n__natsFrom(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
Consider the dependency graph
1: U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)))
-->_1 U12^#(tt(), N, XS) ->
c_2(splitAt^#(activate(N), activate(XS))) :2
2: U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS)))
-->_1 splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS))) :3
3: splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS)))
-->_1 U61^#(tt(), N, X, XS) ->
c_4(U62^#(tt(), activate(N), activate(X), activate(XS))) :4
4: U61^#(tt(), N, X, XS) ->
c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))
-->_1 U62^#(tt(), N, X, XS) ->
c_8(U63^#(tt(), activate(N), activate(X), activate(XS))) :8
5: U41^#(tt(), N, XS) ->
c_5(U42^#(tt(), activate(N), activate(XS)))
-->_1 U42^#(tt(), N, XS) ->
c_6(afterNth^#(activate(N), activate(XS))) :6
6: U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS)))
-->_1 afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) :7
7: afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
-->_1 U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS))) :1
8: U62^#(tt(), N, X, XS) ->
c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))
-->_1 U63^#(tt(), N, X, XS) ->
c_9(splitAt^#(activate(N), activate(XS))) :9
9: U63^#(tt(), N, X, XS) ->
c_9(splitAt^#(activate(N), activate(XS)))
-->_1 splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS))) :3
10: U81^#(tt(), N, XS) ->
c_10(U82^#(tt(), activate(N), activate(XS)))
-->_1 U82^#(tt(), N, XS) ->
c_11(splitAt^#(activate(N), activate(XS))) :11
11: U82^#(tt(), N, XS) ->
c_11(splitAt^#(activate(N), activate(XS)))
-->_1 splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS))) :3
12: sel^#(N, XS) -> c_12(U41^#(tt(), N, XS))
-->_1 U41^#(tt(), N, XS) ->
c_5(U42^#(tt(), activate(N), activate(XS))) :5
13: take^#(N, XS) -> c_13(U81^#(tt(), N, XS))
-->_1 U81^#(tt(), N, XS) ->
c_10(U82^#(tt(), activate(N), activate(XS))) :10
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_12(U41^#(tt(), N, XS))
, take^#(N, XS) -> c_13(U81^#(tt(), N, XS)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)))
, U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS)))
, splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS)))
, U61^#(tt(), N, X, XS) ->
c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))
, U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
, U62^#(tt(), N, X, XS) ->
c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))
, U63^#(tt(), N, X, XS) ->
c_9(splitAt^#(activate(N), activate(XS)))
, U81^#(tt(), N, XS) ->
c_10(U82^#(tt(), activate(N), activate(XS)))
, U82^#(tt(), N, XS) ->
c_11(splitAt^#(activate(N), activate(XS))) }
Weak Trs:
{ activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(X)
, natsFrom(N) -> cons(N, n__natsFrom(s(N)))
, natsFrom(X) -> n__natsFrom(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^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:
{ U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)))
, U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS)))
, splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS)))
, U61^#(tt(), N, X, XS) ->
c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))
, U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
, U62^#(tt(), N, X, XS) ->
c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))
, U63^#(tt(), N, X, XS) ->
c_9(splitAt^#(activate(N), activate(XS))) }
Weak DPs:
{ U81^#(tt(), N, XS) ->
c_10(U82^#(tt(), activate(N), activate(XS)))
, U82^#(tt(), N, XS) ->
c_11(splitAt^#(activate(N), activate(XS))) }
Weak Trs:
{ activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(X)
, natsFrom(N) -> cons(N, n__natsFrom(s(N)))
, natsFrom(X) -> n__natsFrom(X) }
StartTerms: basic terms
Strategy: innermost
Problem (S):
------------
Strict DPs:
{ U81^#(tt(), N, XS) ->
c_10(U82^#(tt(), activate(N), activate(XS)))
, U82^#(tt(), N, XS) ->
c_11(splitAt^#(activate(N), activate(XS))) }
Weak DPs:
{ U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)))
, U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS)))
, splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS)))
, U61^#(tt(), N, X, XS) ->
c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))
, U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
, U62^#(tt(), N, X, XS) ->
c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))
, U63^#(tt(), N, X, XS) ->
c_9(splitAt^#(activate(N), activate(XS))) }
Weak Trs:
{ activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(X)
, natsFrom(N) -> cons(N, n__natsFrom(s(N)))
, natsFrom(X) -> n__natsFrom(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)))
, U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS)))
, splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS)))
, U61^#(tt(), N, X, XS) ->
c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))
, U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
, U62^#(tt(), N, X, XS) ->
c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))
, U63^#(tt(), N, X, XS) ->
c_9(splitAt^#(activate(N), activate(XS))) }
Weak DPs:
{ U81^#(tt(), N, XS) ->
c_10(U82^#(tt(), activate(N), activate(XS)))
, U82^#(tt(), N, XS) ->
c_11(splitAt^#(activate(N), activate(XS))) }
Weak Trs:
{ activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(X)
, natsFrom(N) -> cons(N, n__natsFrom(s(N)))
, natsFrom(X) -> n__natsFrom(X) }
StartTerms: basic terms
Strategy: innermost
This problem was proven YES(O(1),O(n^1)).
S) Strict DPs:
{ U81^#(tt(), N, XS) ->
c_10(U82^#(tt(), activate(N), activate(XS)))
, U82^#(tt(), N, XS) ->
c_11(splitAt^#(activate(N), activate(XS))) }
Weak DPs:
{ U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)))
, U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS)))
, splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS)))
, U61^#(tt(), N, X, XS) ->
c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))
, U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
, U62^#(tt(), N, X, XS) ->
c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))
, U63^#(tt(), N, X, XS) ->
c_9(splitAt^#(activate(N), activate(XS))) }
Weak Trs:
{ activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(X)
, natsFrom(N) -> cons(N, n__natsFrom(s(N)))
, natsFrom(X) -> n__natsFrom(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(n^1)).
Strict DPs:
{ U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)))
, U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS)))
, splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS)))
, U61^#(tt(), N, X, XS) ->
c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))
, U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
, U62^#(tt(), N, X, XS) ->
c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))
, U63^#(tt(), N, X, XS) ->
c_9(splitAt^#(activate(N), activate(XS))) }
Weak DPs:
{ U81^#(tt(), N, XS) ->
c_10(U82^#(tt(), activate(N), activate(XS)))
, U82^#(tt(), N, XS) ->
c_11(splitAt^#(activate(N), activate(XS))) }
Weak Trs:
{ activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(X)
, natsFrom(N) -> cons(N, n__natsFrom(s(N)))
, natsFrom(X) -> n__natsFrom(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 2: U12^#(tt(), N, XS) ->
c_2(splitAt^#(activate(N), activate(XS)))
, 3: splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS)))
, 4: U61^#(tt(), N, X, XS) ->
c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))
, 5: U41^#(tt(), N, XS) ->
c_5(U42^#(tt(), activate(N), activate(XS)))
, 6: U42^#(tt(), N, XS) ->
c_6(afterNth^#(activate(N), activate(XS)))
, 8: U62^#(tt(), N, X, XS) ->
c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))
, 9: U63^#(tt(), N, X, XS) ->
c_9(splitAt^#(activate(N), activate(XS)))
, 10: U81^#(tt(), N, XS) ->
c_10(U82^#(tt(), activate(N), activate(XS)))
, 11: U82^#(tt(), N, XS) ->
c_11(splitAt^#(activate(N), activate(XS))) }
Trs: { natsFrom(N) -> cons(N, n__natsFrom(s(N))) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1},
Uargs(c_7) = {1}, Uargs(c_8) = {1}, Uargs(c_9) = {1},
Uargs(c_10) = {1}, Uargs(c_11) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[tt] = [7]
[activate](x1) = [1] x1 + [0]
[cons](x1, x2) = [1] x1 + [1]
[natsFrom](x1) = [1] x1 + [2]
[n__natsFrom](x1) = [1] x1 + [2]
[s](x1) = [1] x1 + [2]
[U11^#](x1, x2, x3) = [1] x1 + [7] x2 + [6] x3 + [0]
[U12^#](x1, x2, x3) = [1] x1 + [7] x2 + [4] x3 + [0]
[splitAt^#](x1, x2) = [3] x1 + [4]
[U61^#](x1, x2, x3, x4) = [1] x1 + [3] x2 + [1]
[U41^#](x1, x2, x3) = [1] x1 + [7] x2 + [7] x3 + [4]
[U42^#](x1, x2, x3) = [1] x1 + [7] x2 + [6] x3 + [2]
[afterNth^#](x1, x2) = [7] x1 + [6] x2 + [7]
[U62^#](x1, x2, x3, x4) = [3] x2 + [7]
[U63^#](x1, x2, x3, x4) = [3] x2 + [5]
[U81^#](x1, x2, x3) = [2] x1 + [7] x2 + [7] x3 + [1]
[U82^#](x1, x2, x3) = [2] x1 + [7] x2 + [0]
[c_1](x1) = [1] x1 + [0]
[c_2](x1) = [1] x1 + [0]
[c_3](x1) = [1] x1 + [0]
[c_4](x1) = [1] x1 + [0]
[c_5](x1) = [1] x1 + [0]
[c_6](x1) = [1] x1 + [0]
[c_7](x1) = [1] x1 + [0]
[c_8](x1) = [1] x1 + [1]
[c_9](x1) = [1] x1 + [0]
[c_10](x1) = [1] x1 + [0]
[c_11](x1) = [2] x1 + [4]
The order satisfies the following ordering constraints:
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[activate(n__natsFrom(X))] = [1] X + [2]
>= [1] X + [2]
= [natsFrom(X)]
[natsFrom(N)] = [1] N + [2]
> [1] N + [1]
= [cons(N, n__natsFrom(s(N)))]
[natsFrom(X)] = [1] X + [2]
>= [1] X + [2]
= [n__natsFrom(X)]
[U11^#(tt(), N, XS)] = [7] N + [6] XS + [7]
>= [7] N + [4] XS + [7]
= [c_1(U12^#(tt(), activate(N), activate(XS)))]
[U12^#(tt(), N, XS)] = [7] N + [4] XS + [7]
> [3] N + [4]
= [c_2(splitAt^#(activate(N), activate(XS)))]
[splitAt^#(s(N), cons(X, XS))] = [3] N + [10]
> [3] N + [8]
= [c_3(U61^#(tt(), N, X, activate(XS)))]
[U61^#(tt(), N, X, XS)] = [3] N + [8]
> [3] N + [7]
= [c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))]
[U41^#(tt(), N, XS)] = [7] N + [7] XS + [11]
> [7] N + [6] XS + [9]
= [c_5(U42^#(tt(), activate(N), activate(XS)))]
[U42^#(tt(), N, XS)] = [7] N + [6] XS + [9]
> [7] N + [6] XS + [7]
= [c_6(afterNth^#(activate(N), activate(XS)))]
[afterNth^#(N, XS)] = [7] N + [6] XS + [7]
>= [7] N + [6] XS + [7]
= [c_7(U11^#(tt(), N, XS))]
[U62^#(tt(), N, X, XS)] = [3] N + [7]
> [3] N + [6]
= [c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))]
[U63^#(tt(), N, X, XS)] = [3] N + [5]
> [3] N + [4]
= [c_9(splitAt^#(activate(N), activate(XS)))]
[U81^#(tt(), N, XS)] = [7] N + [7] XS + [15]
> [7] N + [14]
= [c_10(U82^#(tt(), activate(N), activate(XS)))]
[U82^#(tt(), N, XS)] = [7] N + [14]
> [6] N + [12]
= [c_11(splitAt^#(activate(N), activate(XS)))]
We return to the main proof. Consider the set of all dependency
pairs
:
{ 1: U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)))
, 2: U12^#(tt(), N, XS) ->
c_2(splitAt^#(activate(N), activate(XS)))
, 3: splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS)))
, 4: U61^#(tt(), N, X, XS) ->
c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))
, 5: U41^#(tt(), N, XS) ->
c_5(U42^#(tt(), activate(N), activate(XS)))
, 6: U42^#(tt(), N, XS) ->
c_6(afterNth^#(activate(N), activate(XS)))
, 7: afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
, 8: U62^#(tt(), N, X, XS) ->
c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))
, 9: U63^#(tt(), N, X, XS) ->
c_9(splitAt^#(activate(N), activate(XS)))
, 10: U81^#(tt(), N, XS) ->
c_10(U82^#(tt(), activate(N), activate(XS)))
, 11: U82^#(tt(), N, XS) ->
c_11(splitAt^#(activate(N), activate(XS))) }
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {2,3,4,5,6,8,9,10,11}. These cover all (indirect)
predecessors of dependency pairs {1,2,3,4,5,6,7,8,9,10,11}, their
number of application is equally bounded. The dependency pairs are
shifted into the weak component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak DPs:
{ U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)))
, U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS)))
, splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS)))
, U61^#(tt(), N, X, XS) ->
c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))
, U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
, U62^#(tt(), N, X, XS) ->
c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))
, U63^#(tt(), N, X, XS) ->
c_9(splitAt^#(activate(N), activate(XS)))
, U81^#(tt(), N, XS) ->
c_10(U82^#(tt(), activate(N), activate(XS)))
, U82^#(tt(), N, XS) ->
c_11(splitAt^#(activate(N), activate(XS))) }
Weak Trs:
{ activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(X)
, natsFrom(N) -> cons(N, n__natsFrom(s(N)))
, natsFrom(X) -> n__natsFrom(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)))
, U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS)))
, splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS)))
, U61^#(tt(), N, X, XS) ->
c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))
, U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
, U62^#(tt(), N, X, XS) ->
c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))
, U63^#(tt(), N, X, XS) ->
c_9(splitAt^#(activate(N), activate(XS)))
, U81^#(tt(), N, XS) ->
c_10(U82^#(tt(), activate(N), activate(XS)))
, U82^#(tt(), N, XS) ->
c_11(splitAt^#(activate(N), activate(XS))) }
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(X)
, natsFrom(N) -> cons(N, n__natsFrom(s(N)))
, natsFrom(X) -> n__natsFrom(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:
{ U81^#(tt(), N, XS) ->
c_10(U82^#(tt(), activate(N), activate(XS)))
, U82^#(tt(), N, XS) ->
c_11(splitAt^#(activate(N), activate(XS))) }
Weak DPs:
{ U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)))
, U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS)))
, splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS)))
, U61^#(tt(), N, X, XS) ->
c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))
, U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
, U62^#(tt(), N, X, XS) ->
c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))
, U63^#(tt(), N, X, XS) ->
c_9(splitAt^#(activate(N), activate(XS))) }
Weak Trs:
{ activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(X)
, natsFrom(N) -> cons(N, n__natsFrom(s(N)))
, natsFrom(X) -> n__natsFrom(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
We estimate the number of application of {2} by applications of
Pre({2}) = {1}. Here rules are labeled as follows:
DPs:
{ 1: U81^#(tt(), N, XS) ->
c_10(U82^#(tt(), activate(N), activate(XS)))
, 2: U82^#(tt(), N, XS) ->
c_11(splitAt^#(activate(N), activate(XS)))
, 3: U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)))
, 4: U12^#(tt(), N, XS) ->
c_2(splitAt^#(activate(N), activate(XS)))
, 5: splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS)))
, 6: U61^#(tt(), N, X, XS) ->
c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))
, 7: U41^#(tt(), N, XS) ->
c_5(U42^#(tt(), activate(N), activate(XS)))
, 8: U42^#(tt(), N, XS) ->
c_6(afterNth^#(activate(N), activate(XS)))
, 9: afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
, 10: U62^#(tt(), N, X, XS) ->
c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))
, 11: U63^#(tt(), N, X, XS) ->
c_9(splitAt^#(activate(N), activate(XS))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ U81^#(tt(), N, XS) ->
c_10(U82^#(tt(), activate(N), activate(XS))) }
Weak DPs:
{ U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)))
, U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS)))
, splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS)))
, U61^#(tt(), N, X, XS) ->
c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))
, U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
, U62^#(tt(), N, X, XS) ->
c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))
, U63^#(tt(), N, X, XS) ->
c_9(splitAt^#(activate(N), activate(XS)))
, U82^#(tt(), N, XS) ->
c_11(splitAt^#(activate(N), activate(XS))) }
Weak Trs:
{ activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(X)
, natsFrom(N) -> cons(N, n__natsFrom(s(N)))
, natsFrom(X) -> n__natsFrom(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
We estimate the number of application of {1} by applications of
Pre({1}) = {}. Here rules are labeled as follows:
DPs:
{ 1: U81^#(tt(), N, XS) ->
c_10(U82^#(tt(), activate(N), activate(XS)))
, 2: U11^#(tt(), N, XS) ->
c_1(U12^#(tt(), activate(N), activate(XS)))
, 3: U12^#(tt(), N, XS) ->
c_2(splitAt^#(activate(N), activate(XS)))
, 4: splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS)))
, 5: U61^#(tt(), N, X, XS) ->
c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))
, 6: U41^#(tt(), N, XS) ->
c_5(U42^#(tt(), activate(N), activate(XS)))
, 7: U42^#(tt(), N, XS) ->
c_6(afterNth^#(activate(N), activate(XS)))
, 8: afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
, 9: U62^#(tt(), N, X, XS) ->
c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))
, 10: U63^#(tt(), N, X, XS) ->
c_9(splitAt^#(activate(N), activate(XS)))
, 11: U82^#(tt(), N, XS) ->
c_11(splitAt^#(activate(N), activate(XS))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak DPs:
{ U11^#(tt(), N, XS) -> c_1(U12^#(tt(), activate(N), activate(XS)))
, U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS)))
, splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS)))
, U61^#(tt(), N, X, XS) ->
c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))
, U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
, U62^#(tt(), N, X, XS) ->
c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))
, U63^#(tt(), N, X, XS) ->
c_9(splitAt^#(activate(N), activate(XS)))
, U81^#(tt(), N, XS) ->
c_10(U82^#(tt(), activate(N), activate(XS)))
, U82^#(tt(), N, XS) ->
c_11(splitAt^#(activate(N), activate(XS))) }
Weak Trs:
{ activate(X) -> X
, activate(n__natsFrom(X)) -> natsFrom(X)
, natsFrom(N) -> cons(N, n__natsFrom(s(N)))
, natsFrom(X) -> n__natsFrom(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)))
, U12^#(tt(), N, XS) -> c_2(splitAt^#(activate(N), activate(XS)))
, splitAt^#(s(N), cons(X, XS)) ->
c_3(U61^#(tt(), N, X, activate(XS)))
, U61^#(tt(), N, X, XS) ->
c_4(U62^#(tt(), activate(N), activate(X), activate(XS)))
, U41^#(tt(), N, XS) -> c_5(U42^#(tt(), activate(N), activate(XS)))
, U42^#(tt(), N, XS) -> c_6(afterNth^#(activate(N), activate(XS)))
, afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
, U62^#(tt(), N, X, XS) ->
c_8(U63^#(tt(), activate(N), activate(X), activate(XS)))
, U63^#(tt(), N, X, XS) ->
c_9(splitAt^#(activate(N), activate(XS)))
, U81^#(tt(), N, XS) ->
c_10(U82^#(tt(), activate(N), activate(XS)))
, U82^#(tt(), N, XS) ->
c_11(splitAt^#(activate(N), activate(XS))) }
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(X)
, natsFrom(N) -> cons(N, n__natsFrom(s(N)))
, natsFrom(X) -> n__natsFrom(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),O(n^1))