MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ natsFrom(N) -> cons(N, natsFrom(s(N)))
, fst(pair(XS, YS)) -> XS
, snd(pair(XS, YS)) -> YS
, splitAt(s(N), cons(X, XS)) -> u(splitAt(N, XS), N, X, XS)
, splitAt(0(), XS) -> pair(nil(), XS)
, u(pair(YS, ZS), N, X, XS) -> pair(cons(X, YS), ZS)
, head(cons(N, XS)) -> N
, tail(cons(N, XS)) -> XS
, sel(N, XS) -> head(afterNth(N, XS))
, afterNth(N, XS) -> snd(splitAt(N, XS))
, take(N, XS) -> fst(splitAt(N, XS)) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
We add following weak dependency pairs:
Strict DPs:
{ natsFrom^#(N) -> c_1(natsFrom^#(s(N)))
, fst^#(pair(XS, YS)) -> c_2()
, snd^#(pair(XS, YS)) -> c_3()
, splitAt^#(s(N), cons(X, XS)) ->
c_4(u^#(splitAt(N, XS), N, X, XS))
, splitAt^#(0(), XS) -> c_5()
, u^#(pair(YS, ZS), N, X, XS) -> c_6()
, head^#(cons(N, XS)) -> c_7()
, tail^#(cons(N, XS)) -> c_8()
, sel^#(N, XS) -> c_9(head^#(afterNth(N, XS)))
, afterNth^#(N, XS) -> c_10(snd^#(splitAt(N, XS)))
, take^#(N, XS) -> c_11(fst^#(splitAt(N, XS))) }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ natsFrom^#(N) -> c_1(natsFrom^#(s(N)))
, fst^#(pair(XS, YS)) -> c_2()
, snd^#(pair(XS, YS)) -> c_3()
, splitAt^#(s(N), cons(X, XS)) ->
c_4(u^#(splitAt(N, XS), N, X, XS))
, splitAt^#(0(), XS) -> c_5()
, u^#(pair(YS, ZS), N, X, XS) -> c_6()
, head^#(cons(N, XS)) -> c_7()
, tail^#(cons(N, XS)) -> c_8()
, sel^#(N, XS) -> c_9(head^#(afterNth(N, XS)))
, afterNth^#(N, XS) -> c_10(snd^#(splitAt(N, XS)))
, take^#(N, XS) -> c_11(fst^#(splitAt(N, XS))) }
Strict Trs:
{ natsFrom(N) -> cons(N, natsFrom(s(N)))
, fst(pair(XS, YS)) -> XS
, snd(pair(XS, YS)) -> YS
, splitAt(s(N), cons(X, XS)) -> u(splitAt(N, XS), N, X, XS)
, splitAt(0(), XS) -> pair(nil(), XS)
, u(pair(YS, ZS), N, X, XS) -> pair(cons(X, YS), ZS)
, head(cons(N, XS)) -> N
, tail(cons(N, XS)) -> XS
, sel(N, XS) -> head(afterNth(N, XS))
, afterNth(N, XS) -> snd(splitAt(N, XS))
, take(N, XS) -> fst(splitAt(N, XS)) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
We replace rewrite rules by usable rules:
Strict Usable Rules:
{ snd(pair(XS, YS)) -> YS
, splitAt(s(N), cons(X, XS)) -> u(splitAt(N, XS), N, X, XS)
, splitAt(0(), XS) -> pair(nil(), XS)
, u(pair(YS, ZS), N, X, XS) -> pair(cons(X, YS), ZS)
, afterNth(N, XS) -> snd(splitAt(N, XS)) }
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ natsFrom^#(N) -> c_1(natsFrom^#(s(N)))
, fst^#(pair(XS, YS)) -> c_2()
, snd^#(pair(XS, YS)) -> c_3()
, splitAt^#(s(N), cons(X, XS)) ->
c_4(u^#(splitAt(N, XS), N, X, XS))
, splitAt^#(0(), XS) -> c_5()
, u^#(pair(YS, ZS), N, X, XS) -> c_6()
, head^#(cons(N, XS)) -> c_7()
, tail^#(cons(N, XS)) -> c_8()
, sel^#(N, XS) -> c_9(head^#(afterNth(N, XS)))
, afterNth^#(N, XS) -> c_10(snd^#(splitAt(N, XS)))
, take^#(N, XS) -> c_11(fst^#(splitAt(N, XS))) }
Strict Trs:
{ snd(pair(XS, YS)) -> YS
, splitAt(s(N), cons(X, XS)) -> u(splitAt(N, XS), N, X, XS)
, splitAt(0(), XS) -> pair(nil(), XS)
, u(pair(YS, ZS), N, X, XS) -> pair(cons(X, YS), ZS)
, afterNth(N, XS) -> snd(splitAt(N, XS)) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The weightgap principle applies (using the following constant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(snd) = {1}, Uargs(u) = {1}, Uargs(c_1) = {1},
Uargs(fst^#) = {1}, Uargs(snd^#) = {1}, Uargs(c_4) = {1},
Uargs(u^#) = {1}, Uargs(head^#) = {1}, Uargs(c_9) = {1},
Uargs(c_10) = {1}, Uargs(c_11) = {1}
TcT has computed following constructor-restricted matrix
interpretation.
[cons](x1, x2) = [1] x1 + [1] x2 + [0]
[s](x1) = [1] x1 + [2]
[pair](x1, x2) = [1] x2 + [2]
[snd](x1) = [1] x1 + [1]
[splitAt](x1, x2) = [2] x1 + [2] x2 + [0]
[0] = [2]
[nil] = [2]
[u](x1, x2, x3, x4) = [1] x1 + [1] x3 + [2]
[afterNth](x1, x2) = [2] x1 + [2] x2 + [2]
[natsFrom^#](x1) = [1] x1 + [1]
[c_1](x1) = [1] x1 + [1]
[fst^#](x1) = [1] x1 + [2]
[c_2] = [1]
[snd^#](x1) = [1] x1 + [2]
[c_3] = [1]
[splitAt^#](x1, x2) = [2] x1 + [2] x2 + [2]
[c_4](x1) = [1] x1 + [2]
[u^#](x1, x2, x3, x4) = [1] x1 + [2] x3 + [2]
[c_5] = [1]
[c_6] = [1]
[head^#](x1) = [1] x1 + [2]
[c_7] = [1]
[tail^#](x1) = [2] x1 + [2]
[c_8] = [1]
[sel^#](x1, x2) = [2] x1 + [2] x2 + [1]
[c_9](x1) = [1] x1 + [2]
[afterNth^#](x1, x2) = [2] x1 + [2] x2 + [1]
[c_10](x1) = [1] x1 + [2]
[take^#](x1, x2) = [2] x1 + [2] x2 + [1]
[c_11](x1) = [1] x1 + [2]
This order satisfies following ordering constraints:
[snd(pair(XS, YS))] = [1] YS + [3]
> [1] YS + [0]
= [YS]
[splitAt(s(N), cons(X, XS))] = [2] N + [2] XS + [2] X + [4]
> [2] N + [2] XS + [1] X + [2]
= [u(splitAt(N, XS), N, X, XS)]
[splitAt(0(), XS)] = [2] XS + [4]
> [1] XS + [2]
= [pair(nil(), XS)]
[u(pair(YS, ZS), N, X, XS)] = [1] X + [1] ZS + [4]
> [1] ZS + [2]
= [pair(cons(X, YS), ZS)]
[afterNth(N, XS)] = [2] N + [2] XS + [2]
> [2] N + [2] XS + [1]
= [snd(splitAt(N, XS))]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ natsFrom^#(N) -> c_1(natsFrom^#(s(N)))
, sel^#(N, XS) -> c_9(head^#(afterNth(N, XS)))
, afterNth^#(N, XS) -> c_10(snd^#(splitAt(N, XS)))
, take^#(N, XS) -> c_11(fst^#(splitAt(N, XS))) }
Weak DPs:
{ fst^#(pair(XS, YS)) -> c_2()
, snd^#(pair(XS, YS)) -> c_3()
, splitAt^#(s(N), cons(X, XS)) ->
c_4(u^#(splitAt(N, XS), N, X, XS))
, splitAt^#(0(), XS) -> c_5()
, u^#(pair(YS, ZS), N, X, XS) -> c_6()
, head^#(cons(N, XS)) -> c_7()
, tail^#(cons(N, XS)) -> c_8() }
Weak Trs:
{ snd(pair(XS, YS)) -> YS
, splitAt(s(N), cons(X, XS)) -> u(splitAt(N, XS), N, X, XS)
, splitAt(0(), XS) -> pair(nil(), XS)
, u(pair(YS, ZS), N, X, XS) -> pair(cons(X, YS), ZS)
, afterNth(N, XS) -> snd(splitAt(N, XS)) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
We estimate the number of application of {2,3,4} by applications of
Pre({2,3,4}) = {}. Here rules are labeled as follows:
DPs:
{ 1: natsFrom^#(N) -> c_1(natsFrom^#(s(N)))
, 2: sel^#(N, XS) -> c_9(head^#(afterNth(N, XS)))
, 3: afterNth^#(N, XS) -> c_10(snd^#(splitAt(N, XS)))
, 4: take^#(N, XS) -> c_11(fst^#(splitAt(N, XS)))
, 5: fst^#(pair(XS, YS)) -> c_2()
, 6: snd^#(pair(XS, YS)) -> c_3()
, 7: splitAt^#(s(N), cons(X, XS)) ->
c_4(u^#(splitAt(N, XS), N, X, XS))
, 8: splitAt^#(0(), XS) -> c_5()
, 9: u^#(pair(YS, ZS), N, X, XS) -> c_6()
, 10: head^#(cons(N, XS)) -> c_7()
, 11: tail^#(cons(N, XS)) -> c_8() }
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs: { natsFrom^#(N) -> c_1(natsFrom^#(s(N))) }
Weak DPs:
{ fst^#(pair(XS, YS)) -> c_2()
, snd^#(pair(XS, YS)) -> c_3()
, splitAt^#(s(N), cons(X, XS)) ->
c_4(u^#(splitAt(N, XS), N, X, XS))
, splitAt^#(0(), XS) -> c_5()
, u^#(pair(YS, ZS), N, X, XS) -> c_6()
, head^#(cons(N, XS)) -> c_7()
, tail^#(cons(N, XS)) -> c_8()
, sel^#(N, XS) -> c_9(head^#(afterNth(N, XS)))
, afterNth^#(N, XS) -> c_10(snd^#(splitAt(N, XS)))
, take^#(N, XS) -> c_11(fst^#(splitAt(N, XS))) }
Weak Trs:
{ snd(pair(XS, YS)) -> YS
, splitAt(s(N), cons(X, XS)) -> u(splitAt(N, XS), N, X, XS)
, splitAt(0(), XS) -> pair(nil(), XS)
, u(pair(YS, ZS), N, X, XS) -> pair(cons(X, YS), ZS)
, afterNth(N, XS) -> snd(splitAt(N, XS)) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ fst^#(pair(XS, YS)) -> c_2()
, snd^#(pair(XS, YS)) -> c_3()
, splitAt^#(s(N), cons(X, XS)) ->
c_4(u^#(splitAt(N, XS), N, X, XS))
, splitAt^#(0(), XS) -> c_5()
, u^#(pair(YS, ZS), N, X, XS) -> c_6()
, head^#(cons(N, XS)) -> c_7()
, tail^#(cons(N, XS)) -> c_8()
, sel^#(N, XS) -> c_9(head^#(afterNth(N, XS)))
, afterNth^#(N, XS) -> c_10(snd^#(splitAt(N, XS)))
, take^#(N, XS) -> c_11(fst^#(splitAt(N, XS))) }
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs: { natsFrom^#(N) -> c_1(natsFrom^#(s(N))) }
Weak Trs:
{ snd(pair(XS, YS)) -> YS
, splitAt(s(N), cons(X, XS)) -> u(splitAt(N, XS), N, X, XS)
, splitAt(0(), XS) -> pair(nil(), XS)
, u(pair(YS, ZS), N, X, XS) -> pair(cons(X, YS), ZS)
, afterNth(N, XS) -> snd(splitAt(N, XS)) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
No rule is usable, rules are removed from the input problem.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs: { natsFrom^#(N) -> c_1(natsFrom^#(s(N))) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrices' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix interpretation of dimension 4' failed due to the
following reason:
The input cannot be shown compatible
2) 'matrix interpretation of dimension 3' failed due to the
following reason:
The input cannot be shown compatible
3) 'matrix interpretation of dimension 3' failed due to the
following reason:
The input cannot be shown compatible
4) 'matrix interpretation of dimension 2' failed due to the
following reason:
The input cannot be shown compatible
5) 'matrix interpretation of dimension 2' failed due to the
following reason:
The input cannot be shown compatible
6) 'matrix interpretation of dimension 1' failed due to the
following reason:
The input cannot be shown compatible
2) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
Arrrr..