YES(?,O(n^2))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict Trs:
{ a__f(X) -> f(X)
, a__f(0()) -> cons(0(), f(s(0())))
, a__f(s(0())) -> a__f(a__p(s(0())))
, a__p(X) -> p(X)
, a__p(s(0())) -> 0()
, mark(0()) -> 0()
, mark(cons(X1, X2)) -> cons(mark(X1), X2)
, mark(f(X)) -> a__f(mark(X))
, mark(s(X)) -> s(mark(X))
, mark(p(X)) -> a__p(mark(X)) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We add following dependency tuples:
Strict DPs:
{ a__f^#(X) -> c_1()
, a__f^#(0()) -> c_2()
, a__f^#(s(0())) -> c_3(a__f^#(a__p(s(0()))), a__p^#(s(0())))
, a__p^#(X) -> c_4()
, a__p^#(s(0())) -> c_5()
, mark^#(0()) -> c_6()
, mark^#(cons(X1, X2)) -> c_7(mark^#(X1))
, mark^#(f(X)) -> c_8(a__f^#(mark(X)), mark^#(X))
, mark^#(s(X)) -> c_9(mark^#(X))
, mark^#(p(X)) -> c_10(a__p^#(mark(X)), mark^#(X)) }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict DPs:
{ a__f^#(X) -> c_1()
, a__f^#(0()) -> c_2()
, a__f^#(s(0())) -> c_3(a__f^#(a__p(s(0()))), a__p^#(s(0())))
, a__p^#(X) -> c_4()
, a__p^#(s(0())) -> c_5()
, mark^#(0()) -> c_6()
, mark^#(cons(X1, X2)) -> c_7(mark^#(X1))
, mark^#(f(X)) -> c_8(a__f^#(mark(X)), mark^#(X))
, mark^#(s(X)) -> c_9(mark^#(X))
, mark^#(p(X)) -> c_10(a__p^#(mark(X)), mark^#(X)) }
Weak Trs:
{ a__f(X) -> f(X)
, a__f(0()) -> cons(0(), f(s(0())))
, a__f(s(0())) -> a__f(a__p(s(0())))
, a__p(X) -> p(X)
, a__p(s(0())) -> 0()
, mark(0()) -> 0()
, mark(cons(X1, X2)) -> cons(mark(X1), X2)
, mark(f(X)) -> a__f(mark(X))
, mark(s(X)) -> s(mark(X))
, mark(p(X)) -> a__p(mark(X)) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
We estimate the number of application of {1,2,4,5,6} by
applications of Pre({1,2,4,5,6}) = {3,7,8,9,10}. Here rules are
labeled as follows:
DPs:
{ 1: a__f^#(X) -> c_1()
, 2: a__f^#(0()) -> c_2()
, 3: a__f^#(s(0())) -> c_3(a__f^#(a__p(s(0()))), a__p^#(s(0())))
, 4: a__p^#(X) -> c_4()
, 5: a__p^#(s(0())) -> c_5()
, 6: mark^#(0()) -> c_6()
, 7: mark^#(cons(X1, X2)) -> c_7(mark^#(X1))
, 8: mark^#(f(X)) -> c_8(a__f^#(mark(X)), mark^#(X))
, 9: mark^#(s(X)) -> c_9(mark^#(X))
, 10: mark^#(p(X)) -> c_10(a__p^#(mark(X)), mark^#(X)) }
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict DPs:
{ a__f^#(s(0())) -> c_3(a__f^#(a__p(s(0()))), a__p^#(s(0())))
, mark^#(cons(X1, X2)) -> c_7(mark^#(X1))
, mark^#(f(X)) -> c_8(a__f^#(mark(X)), mark^#(X))
, mark^#(s(X)) -> c_9(mark^#(X))
, mark^#(p(X)) -> c_10(a__p^#(mark(X)), mark^#(X)) }
Weak DPs:
{ a__f^#(X) -> c_1()
, a__f^#(0()) -> c_2()
, a__p^#(X) -> c_4()
, a__p^#(s(0())) -> c_5()
, mark^#(0()) -> c_6() }
Weak Trs:
{ a__f(X) -> f(X)
, a__f(0()) -> cons(0(), f(s(0())))
, a__f(s(0())) -> a__f(a__p(s(0())))
, a__p(X) -> p(X)
, a__p(s(0())) -> 0()
, mark(0()) -> 0()
, mark(cons(X1, X2)) -> cons(mark(X1), X2)
, mark(f(X)) -> a__f(mark(X))
, mark(s(X)) -> s(mark(X))
, mark(p(X)) -> a__p(mark(X)) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ a__f^#(X) -> c_1()
, a__f^#(0()) -> c_2()
, a__p^#(X) -> c_4()
, a__p^#(s(0())) -> c_5()
, mark^#(0()) -> c_6() }
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict DPs:
{ a__f^#(s(0())) -> c_3(a__f^#(a__p(s(0()))), a__p^#(s(0())))
, mark^#(cons(X1, X2)) -> c_7(mark^#(X1))
, mark^#(f(X)) -> c_8(a__f^#(mark(X)), mark^#(X))
, mark^#(s(X)) -> c_9(mark^#(X))
, mark^#(p(X)) -> c_10(a__p^#(mark(X)), mark^#(X)) }
Weak Trs:
{ a__f(X) -> f(X)
, a__f(0()) -> cons(0(), f(s(0())))
, a__f(s(0())) -> a__f(a__p(s(0())))
, a__p(X) -> p(X)
, a__p(s(0())) -> 0()
, mark(0()) -> 0()
, mark(cons(X1, X2)) -> cons(mark(X1), X2)
, mark(f(X)) -> a__f(mark(X))
, mark(s(X)) -> s(mark(X))
, mark(p(X)) -> a__p(mark(X)) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ a__f^#(s(0())) -> c_3(a__f^#(a__p(s(0()))), a__p^#(s(0())))
, mark^#(p(X)) -> c_10(a__p^#(mark(X)), mark^#(X)) }
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict DPs:
{ a__f^#(s(0())) -> c_1(a__f^#(a__p(s(0()))))
, mark^#(cons(X1, X2)) -> c_2(mark^#(X1))
, mark^#(f(X)) -> c_3(a__f^#(mark(X)), mark^#(X))
, mark^#(s(X)) -> c_4(mark^#(X))
, mark^#(p(X)) -> c_5(mark^#(X)) }
Weak Trs:
{ a__f(X) -> f(X)
, a__f(0()) -> cons(0(), f(s(0())))
, a__f(s(0())) -> a__f(a__p(s(0())))
, a__p(X) -> p(X)
, a__p(s(0())) -> 0()
, mark(0()) -> 0()
, mark(cons(X1, X2)) -> cons(mark(X1), X2)
, mark(f(X)) -> a__f(mark(X))
, mark(s(X)) -> s(mark(X))
, mark(p(X)) -> a__p(mark(X)) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {1}, Uargs(c_5) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[a__f](x1) = [1 3] x1 + [0]
[0 0] [2]
[0] = [2]
[0]
[cons](x1, x2) = [1 2] x1 + [0]
[0 0] [1]
[f](x1) = [1 2] x1 + [0]
[0 0] [2]
[s](x1) = [1 2] x1 + [0]
[0 0] [1]
[a__p](x1) = [1 2] x1 + [1]
[0 0] [0]
[mark](x1) = [2 0] x1 + [0]
[0 1] [0]
[p](x1) = [1 2] x1 + [1]
[0 0] [0]
[a__f^#](x1) = [0 1] x1 + [0]
[0 0] [0]
[mark^#](x1) = [2 2] x1 + [0]
[0 1] [0]
[c_1](x1) = [2 0] x1 + [0]
[0 0] [0]
[c_2](x1) = [1 0] x1 + [1]
[0 0] [1]
[c_3](x1, x2) = [1 0] x1 + [1 1] x2 + [3]
[0 0] [0 0] [1]
[c_4](x1) = [1 0] x1 + [1]
[0 0] [1]
[c_5](x1) = [1 0] x1 + [1]
[0 0] [0]
This order satisfies following ordering constraints:
[a__f(X)] = [1 3] X + [0]
[0 0] [2]
>= [1 2] X + [0]
[0 0] [2]
= [f(X)]
[a__f(0())] = [2]
[2]
>= [2]
[1]
= [cons(0(), f(s(0())))]
[a__f(s(0()))] = [5]
[2]
>= [5]
[2]
= [a__f(a__p(s(0())))]
[a__p(X)] = [1 2] X + [1]
[0 0] [0]
>= [1 2] X + [1]
[0 0] [0]
= [p(X)]
[a__p(s(0()))] = [5]
[0]
> [2]
[0]
= [0()]
[mark(0())] = [4]
[0]
> [2]
[0]
= [0()]
[mark(cons(X1, X2))] = [2 4] X1 + [0]
[0 0] [1]
>= [2 2] X1 + [0]
[0 0] [1]
= [cons(mark(X1), X2)]
[mark(f(X))] = [2 4] X + [0]
[0 0] [2]
>= [2 3] X + [0]
[0 0] [2]
= [a__f(mark(X))]
[mark(s(X))] = [2 4] X + [0]
[0 0] [1]
>= [2 2] X + [0]
[0 0] [1]
= [s(mark(X))]
[mark(p(X))] = [2 4] X + [2]
[0 0] [0]
> [2 2] X + [1]
[0 0] [0]
= [a__p(mark(X))]
[a__f^#(s(0()))] = [1]
[0]
> [0]
[0]
= [c_1(a__f^#(a__p(s(0()))))]
[mark^#(cons(X1, X2))] = [2 4] X1 + [2]
[0 0] [1]
> [2 2] X1 + [1]
[0 0] [1]
= [c_2(mark^#(X1))]
[mark^#(f(X))] = [2 4] X + [4]
[0 0] [2]
> [2 4] X + [3]
[0 0] [1]
= [c_3(a__f^#(mark(X)), mark^#(X))]
[mark^#(s(X))] = [2 4] X + [2]
[0 0] [1]
> [2 2] X + [1]
[0 0] [1]
= [c_4(mark^#(X))]
[mark^#(p(X))] = [2 4] X + [2]
[0 0] [0]
> [2 2] X + [1]
[0 0] [0]
= [c_5(mark^#(X))]
Hurray, we answered YES(?,O(n^2))