We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ merge(Cons(x', xs'), Cons(x, xs)) ->
merge[Ite](<=(x', x), Cons(x', xs'), Cons(x, xs))
, merge(Cons(x, xs), Nil()) -> Cons(x, xs)
, merge(Nil(), ys) -> ys
, goal(xs, ys) -> merge(xs, ys) }
Weak Trs:
{ <=(S(x), S(y)) -> <=(x, y)
, <=(S(x), 0()) -> False()
, <=(0(), y) -> True()
, merge[Ite](True(), Cons(x, xs), ys) -> Cons(x, merge(xs, ys))
, merge[Ite](False(), xs', Cons(x, xs)) ->
Cons(x, merge(xs', xs)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We add the following weak dependency pairs:
Strict DPs:
{ merge^#(Cons(x', xs'), Cons(x, xs)) ->
c_1(merge[Ite]^#(<=(x', x), Cons(x', xs'), Cons(x, xs)))
, merge^#(Cons(x, xs), Nil()) -> c_2()
, merge^#(Nil(), ys) -> c_3()
, goal^#(xs, ys) -> c_4(merge^#(xs, ys)) }
Weak DPs:
{ merge[Ite]^#(True(), Cons(x, xs), ys) -> c_8(merge^#(xs, ys))
, merge[Ite]^#(False(), xs', Cons(x, xs)) -> c_9(merge^#(xs', xs))
, <=^#(S(x), S(y)) -> c_5(<=^#(x, y))
, <=^#(S(x), 0()) -> c_6()
, <=^#(0(), y) -> c_7() }
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:
{ merge^#(Cons(x', xs'), Cons(x, xs)) ->
c_1(merge[Ite]^#(<=(x', x), Cons(x', xs'), Cons(x, xs)))
, merge^#(Cons(x, xs), Nil()) -> c_2()
, merge^#(Nil(), ys) -> c_3()
, goal^#(xs, ys) -> c_4(merge^#(xs, ys)) }
Strict Trs:
{ merge(Cons(x', xs'), Cons(x, xs)) ->
merge[Ite](<=(x', x), Cons(x', xs'), Cons(x, xs))
, merge(Cons(x, xs), Nil()) -> Cons(x, xs)
, merge(Nil(), ys) -> ys
, goal(xs, ys) -> merge(xs, ys) }
Weak DPs:
{ merge[Ite]^#(True(), Cons(x, xs), ys) -> c_8(merge^#(xs, ys))
, merge[Ite]^#(False(), xs', Cons(x, xs)) -> c_9(merge^#(xs', xs))
, <=^#(S(x), S(y)) -> c_5(<=^#(x, y))
, <=^#(S(x), 0()) -> c_6()
, <=^#(0(), y) -> c_7() }
Weak Trs:
{ <=(S(x), S(y)) -> <=(x, y)
, <=(S(x), 0()) -> False()
, <=(0(), y) -> True()
, merge[Ite](True(), Cons(x, xs), ys) -> Cons(x, merge(xs, ys))
, merge[Ite](False(), xs', Cons(x, xs)) ->
Cons(x, merge(xs', xs)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We replace rewrite rules by usable rules:
Weak Usable Rules:
{ <=(S(x), S(y)) -> <=(x, y)
, <=(S(x), 0()) -> False()
, <=(0(), y) -> True() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ merge^#(Cons(x', xs'), Cons(x, xs)) ->
c_1(merge[Ite]^#(<=(x', x), Cons(x', xs'), Cons(x, xs)))
, merge^#(Cons(x, xs), Nil()) -> c_2()
, merge^#(Nil(), ys) -> c_3()
, goal^#(xs, ys) -> c_4(merge^#(xs, ys)) }
Weak DPs:
{ merge[Ite]^#(True(), Cons(x, xs), ys) -> c_8(merge^#(xs, ys))
, merge[Ite]^#(False(), xs', Cons(x, xs)) -> c_9(merge^#(xs', xs))
, <=^#(S(x), S(y)) -> c_5(<=^#(x, y))
, <=^#(S(x), 0()) -> c_6()
, <=^#(0(), y) -> c_7() }
Weak Trs:
{ <=(S(x), S(y)) -> <=(x, y)
, <=(S(x), 0()) -> False()
, <=(0(), y) -> True() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following constant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(merge[Ite]^#) = {1}, Uargs(c_4) = {1},
Uargs(c_5) = {1}, Uargs(c_8) = {1}, Uargs(c_9) = {1}
TcT has computed the following constructor-restricted matrix
interpretation.
[<=](x1, x2) = [0]
[0]
[True] = [0]
[0]
[S](x1) = [1 0] x1 + [0]
[0 0] [0]
[Cons](x1, x2) = [0]
[0]
[Nil] = [0]
[0]
[0] = [0]
[0]
[False] = [0]
[0]
[merge^#](x1, x2) = [0]
[0]
[c_1](x1) = [1 0] x1 + [2]
[0 1] [0]
[merge[Ite]^#](x1, x2, x3) = [2 0] x1 + [0]
[0 0] [0]
[c_2] = [0]
[0]
[c_3] = [0]
[0]
[goal^#](x1, x2) = [2 1] x1 + [1 2] x2 + [2]
[1 1] [1 1] [2]
[c_4](x1) = [1 0] x1 + [0]
[0 1] [0]
[<=^#](x1, x2) = [0]
[0]
[c_5](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_6] = [0]
[0]
[c_7] = [0]
[0]
[c_8](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_9](x1) = [1 0] x1 + [0]
[0 1] [0]
The order satisfies the following ordering constraints:
[<=(S(x), S(y))] = [0]
[0]
>= [0]
[0]
= [<=(x, y)]
[<=(S(x), 0())] = [0]
[0]
>= [0]
[0]
= [False()]
[<=(0(), y)] = [0]
[0]
>= [0]
[0]
= [True()]
[merge^#(Cons(x', xs'), Cons(x, xs))] = [0]
[0]
? [2]
[0]
= [c_1(merge[Ite]^#(<=(x', x), Cons(x', xs'), Cons(x, xs)))]
[merge^#(Cons(x, xs), Nil())] = [0]
[0]
>= [0]
[0]
= [c_2()]
[merge^#(Nil(), ys)] = [0]
[0]
>= [0]
[0]
= [c_3()]
[merge[Ite]^#(True(), Cons(x, xs), ys)] = [0]
[0]
>= [0]
[0]
= [c_8(merge^#(xs, ys))]
[merge[Ite]^#(False(), xs', Cons(x, xs))] = [0]
[0]
>= [0]
[0]
= [c_9(merge^#(xs', xs))]
[goal^#(xs, ys)] = [2 1] xs + [1 2] ys + [2]
[1 1] [1 1] [2]
> [0]
[0]
= [c_4(merge^#(xs, ys))]
[<=^#(S(x), S(y))] = [0]
[0]
>= [0]
[0]
= [c_5(<=^#(x, y))]
[<=^#(S(x), 0())] = [0]
[0]
>= [0]
[0]
= [c_6()]
[<=^#(0(), y)] = [0]
[0]
>= [0]
[0]
= [c_7()]
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 YES(O(1),O(n^1)).
Strict DPs:
{ merge^#(Cons(x', xs'), Cons(x, xs)) ->
c_1(merge[Ite]^#(<=(x', x), Cons(x', xs'), Cons(x, xs)))
, merge^#(Cons(x, xs), Nil()) -> c_2()
, merge^#(Nil(), ys) -> c_3() }
Weak DPs:
{ merge[Ite]^#(True(), Cons(x, xs), ys) -> c_8(merge^#(xs, ys))
, merge[Ite]^#(False(), xs', Cons(x, xs)) -> c_9(merge^#(xs', xs))
, goal^#(xs, ys) -> c_4(merge^#(xs, ys))
, <=^#(S(x), S(y)) -> c_5(<=^#(x, y))
, <=^#(S(x), 0()) -> c_6()
, <=^#(0(), y) -> c_7() }
Weak Trs:
{ <=(S(x), S(y)) -> <=(x, y)
, <=(S(x), 0()) -> False()
, <=(0(), y) -> True() }
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.
{ <=^#(S(x), S(y)) -> c_5(<=^#(x, y))
, <=^#(S(x), 0()) -> c_6()
, <=^#(0(), y) -> c_7() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ merge^#(Cons(x', xs'), Cons(x, xs)) ->
c_1(merge[Ite]^#(<=(x', x), Cons(x', xs'), Cons(x, xs)))
, merge^#(Cons(x, xs), Nil()) -> c_2()
, merge^#(Nil(), ys) -> c_3() }
Weak DPs:
{ merge[Ite]^#(True(), Cons(x, xs), ys) -> c_8(merge^#(xs, ys))
, merge[Ite]^#(False(), xs', Cons(x, xs)) -> c_9(merge^#(xs', xs))
, goal^#(xs, ys) -> c_4(merge^#(xs, ys)) }
Weak Trs:
{ <=(S(x), S(y)) -> <=(x, y)
, <=(S(x), 0()) -> False()
, <=(0(), y) -> True() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
Consider the dependency graph
1: merge^#(Cons(x', xs'), Cons(x, xs)) ->
c_1(merge[Ite]^#(<=(x', x), Cons(x', xs'), Cons(x, xs)))
-->_1 merge[Ite]^#(False(), xs', Cons(x, xs)) ->
c_9(merge^#(xs', xs)) :5
-->_1 merge[Ite]^#(True(), Cons(x, xs), ys) ->
c_8(merge^#(xs, ys)) :4
2: merge^#(Cons(x, xs), Nil()) -> c_2()
3: merge^#(Nil(), ys) -> c_3()
4: merge[Ite]^#(True(), Cons(x, xs), ys) -> c_8(merge^#(xs, ys))
-->_1 merge^#(Nil(), ys) -> c_3() :3
-->_1 merge^#(Cons(x, xs), Nil()) -> c_2() :2
-->_1 merge^#(Cons(x', xs'), Cons(x, xs)) ->
c_1(merge[Ite]^#(<=(x', x), Cons(x', xs'), Cons(x, xs))) :1
5: merge[Ite]^#(False(), xs', Cons(x, xs)) -> c_9(merge^#(xs', xs))
-->_1 merge^#(Nil(), ys) -> c_3() :3
-->_1 merge^#(Cons(x, xs), Nil()) -> c_2() :2
-->_1 merge^#(Cons(x', xs'), Cons(x, xs)) ->
c_1(merge[Ite]^#(<=(x', x), Cons(x', xs'), Cons(x, xs))) :1
6: goal^#(xs, ys) -> c_4(merge^#(xs, ys))
-->_1 merge^#(Nil(), ys) -> c_3() :3
-->_1 merge^#(Cons(x, xs), Nil()) -> c_2() :2
-->_1 merge^#(Cons(x', xs'), Cons(x, xs)) ->
c_1(merge[Ite]^#(<=(x', x), Cons(x', xs'), Cons(x, xs))) :1
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).
{ goal^#(xs, ys) -> c_4(merge^#(xs, ys)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ merge^#(Cons(x', xs'), Cons(x, xs)) ->
c_1(merge[Ite]^#(<=(x', x), Cons(x', xs'), Cons(x, xs)))
, merge^#(Cons(x, xs), Nil()) -> c_2()
, merge^#(Nil(), ys) -> c_3() }
Weak DPs:
{ merge[Ite]^#(True(), Cons(x, xs), ys) -> c_8(merge^#(xs, ys))
, merge[Ite]^#(False(), xs', Cons(x, xs)) ->
c_9(merge^#(xs', xs)) }
Weak Trs:
{ <=(S(x), S(y)) -> <=(x, y)
, <=(S(x), 0()) -> False()
, <=(0(), y) -> True() }
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: merge^#(Cons(x, xs), Nil()) -> c_2()
, 3: merge^#(Nil(), ys) -> c_3() }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_8) = {1}, Uargs(c_9) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[<=](x1, x2) = [0]
[True] = [0]
[S](x1) = [1] x1 + [0]
[Cons](x1, x2) = [1] x1 + [1] x2 + [0]
[Nil] = [0]
[0] = [0]
[False] = [0]
[merge^#](x1, x2) = [1]
[c_1](x1) = [1] x1 + [0]
[merge[Ite]^#](x1, x2, x3) = [1]
[c_2] = [0]
[c_3] = [0]
[c_8](x1) = [1] x1 + [0]
[c_9](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[<=(S(x), S(y))] = [0]
>= [0]
= [<=(x, y)]
[<=(S(x), 0())] = [0]
>= [0]
= [False()]
[<=(0(), y)] = [0]
>= [0]
= [True()]
[merge^#(Cons(x', xs'), Cons(x, xs))] = [1]
>= [1]
= [c_1(merge[Ite]^#(<=(x', x), Cons(x', xs'), Cons(x, xs)))]
[merge^#(Cons(x, xs), Nil())] = [1]
> [0]
= [c_2()]
[merge^#(Nil(), ys)] = [1]
> [0]
= [c_3()]
[merge[Ite]^#(True(), Cons(x, xs), ys)] = [1]
>= [1]
= [c_8(merge^#(xs, ys))]
[merge[Ite]^#(False(), xs', Cons(x, xs))] = [1]
>= [1]
= [c_9(merge^#(xs', xs))]
The strictly oriented rules are moved into the weak component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ merge^#(Cons(x', xs'), Cons(x, xs)) ->
c_1(merge[Ite]^#(<=(x', x), Cons(x', xs'), Cons(x, xs))) }
Weak DPs:
{ merge^#(Cons(x, xs), Nil()) -> c_2()
, merge^#(Nil(), ys) -> c_3()
, merge[Ite]^#(True(), Cons(x, xs), ys) -> c_8(merge^#(xs, ys))
, merge[Ite]^#(False(), xs', Cons(x, xs)) ->
c_9(merge^#(xs', xs)) }
Weak Trs:
{ <=(S(x), S(y)) -> <=(x, y)
, <=(S(x), 0()) -> False()
, <=(0(), y) -> True() }
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.
{ merge^#(Cons(x, xs), Nil()) -> c_2()
, merge^#(Nil(), ys) -> c_3() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ merge^#(Cons(x', xs'), Cons(x, xs)) ->
c_1(merge[Ite]^#(<=(x', x), Cons(x', xs'), Cons(x, xs))) }
Weak DPs:
{ merge[Ite]^#(True(), Cons(x, xs), ys) -> c_8(merge^#(xs, ys))
, merge[Ite]^#(False(), xs', Cons(x, xs)) ->
c_9(merge^#(xs', xs)) }
Weak Trs:
{ <=(S(x), S(y)) -> <=(x, y)
, <=(S(x), 0()) -> False()
, <=(0(), y) -> True() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 1: merge^#(Cons(x', xs'), Cons(x, xs)) ->
c_1(merge[Ite]^#(<=(x', x), Cons(x', xs'), Cons(x, xs)))
, 2: merge[Ite]^#(True(), Cons(x, xs), ys) -> c_8(merge^#(xs, ys))
, 3: merge[Ite]^#(False(), xs', Cons(x, xs)) ->
c_9(merge^#(xs', xs)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_8) = {1}, Uargs(c_9) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[<=](x1, x2) = [0]
[True] = [0]
[S](x1) = [1] x1 + [0]
[Cons](x1, x2) = [1] x2 + [2]
[Nil] = [0]
[0] = [2]
[False] = [0]
[merge^#](x1, x2) = [4] x1 + [2] x2 + [1]
[c_1](x1) = [1] x1 + [0]
[merge[Ite]^#](x1, x2, x3) = [1] x1 + [4] x2 + [2] x3 + [0]
[c_2] = [0]
[c_3] = [0]
[c_8](x1) = [1] x1 + [2]
[c_9](x1) = [1] x1 + [2]
The order satisfies the following ordering constraints:
[<=(S(x), S(y))] = [0]
>= [0]
= [<=(x, y)]
[<=(S(x), 0())] = [0]
>= [0]
= [False()]
[<=(0(), y)] = [0]
>= [0]
= [True()]
[merge^#(Cons(x', xs'), Cons(x, xs))] = [2] xs + [4] xs' + [13]
> [2] xs + [4] xs' + [12]
= [c_1(merge[Ite]^#(<=(x', x), Cons(x', xs'), Cons(x, xs)))]
[merge[Ite]^#(True(), Cons(x, xs), ys)] = [4] xs + [2] ys + [8]
> [4] xs + [2] ys + [3]
= [c_8(merge^#(xs, ys))]
[merge[Ite]^#(False(), xs', Cons(x, xs))] = [2] xs + [4] xs' + [4]
> [2] xs + [4] xs' + [3]
= [c_9(merge^#(xs', xs))]
The strictly oriented rules are moved into the weak component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak DPs:
{ merge^#(Cons(x', xs'), Cons(x, xs)) ->
c_1(merge[Ite]^#(<=(x', x), Cons(x', xs'), Cons(x, xs)))
, merge[Ite]^#(True(), Cons(x, xs), ys) -> c_8(merge^#(xs, ys))
, merge[Ite]^#(False(), xs', Cons(x, xs)) ->
c_9(merge^#(xs', xs)) }
Weak Trs:
{ <=(S(x), S(y)) -> <=(x, y)
, <=(S(x), 0()) -> False()
, <=(0(), y) -> True() }
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.
{ merge^#(Cons(x', xs'), Cons(x, xs)) ->
c_1(merge[Ite]^#(<=(x', x), Cons(x', xs'), Cons(x, xs)))
, merge[Ite]^#(True(), Cons(x, xs), ys) -> c_8(merge^#(xs, ys))
, merge[Ite]^#(False(), xs', Cons(x, xs)) ->
c_9(merge^#(xs', xs)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ <=(S(x), S(y)) -> <=(x, y)
, <=(S(x), 0()) -> False()
, <=(0(), y) -> True() }
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))