We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ f(x, nil()) -> g(nil(), x)
, f(x, g(y, z)) -> g(f(x, y), z)
, ++(x, nil()) -> x
, ++(x, g(y, z)) -> g(++(x, y), z)
, null(nil()) -> true()
, null(g(x, y)) -> false()
, mem(x, max(x)) -> not(null(x))
, mem(nil(), y) -> false()
, mem(g(x, y), z) -> or(=(y, z), mem(x, z))
, max(g(g(nil(), x), y)) -> max'(x, y)
, max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u()) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We add the following weak dependency pairs:
Strict DPs:
{ f^#(x, nil()) -> c_1()
, f^#(x, g(y, z)) -> c_2(f^#(x, y))
, ++^#(x, nil()) -> c_3()
, ++^#(x, g(y, z)) -> c_4(++^#(x, y))
, null^#(nil()) -> c_5()
, null^#(g(x, y)) -> c_6()
, mem^#(x, max(x)) -> c_7(null^#(x))
, mem^#(nil(), y) -> c_8()
, mem^#(g(x, y), z) -> c_9(mem^#(x, z))
, max^#(g(g(nil(), x), y)) -> c_10()
, max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) }
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:
{ f^#(x, nil()) -> c_1()
, f^#(x, g(y, z)) -> c_2(f^#(x, y))
, ++^#(x, nil()) -> c_3()
, ++^#(x, g(y, z)) -> c_4(++^#(x, y))
, null^#(nil()) -> c_5()
, null^#(g(x, y)) -> c_6()
, mem^#(x, max(x)) -> c_7(null^#(x))
, mem^#(nil(), y) -> c_8()
, mem^#(g(x, y), z) -> c_9(mem^#(x, z))
, max^#(g(g(nil(), x), y)) -> c_10()
, max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) }
Strict Trs:
{ f(x, nil()) -> g(nil(), x)
, f(x, g(y, z)) -> g(f(x, y), z)
, ++(x, nil()) -> x
, ++(x, g(y, z)) -> g(++(x, y), z)
, null(nil()) -> true()
, null(g(x, y)) -> false()
, mem(x, max(x)) -> not(null(x))
, mem(nil(), y) -> false()
, mem(g(x, y), z) -> or(=(y, z), mem(x, z))
, max(g(g(nil(), x), y)) -> max'(x, y)
, max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u()) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^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(n^1)).
Strict DPs:
{ f^#(x, nil()) -> c_1()
, f^#(x, g(y, z)) -> c_2(f^#(x, y))
, ++^#(x, nil()) -> c_3()
, ++^#(x, g(y, z)) -> c_4(++^#(x, y))
, null^#(nil()) -> c_5()
, null^#(g(x, y)) -> c_6()
, mem^#(x, max(x)) -> c_7(null^#(x))
, mem^#(nil(), y) -> c_8()
, mem^#(g(x, y), z) -> c_9(mem^#(x, z))
, max^#(g(g(nil(), x), y)) -> c_10()
, max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) }
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_2) = {1}, Uargs(c_4) = {1}, Uargs(c_7) = {1},
Uargs(c_9) = {1}, Uargs(c_11) = {1}
TcT has computed the following constructor-restricted matrix
interpretation.
[nil] = [0]
[0]
[g](x1, x2) = [0]
[0]
[max](x1) = [0]
[0]
[u] = [0]
[0]
[f^#](x1, x2) = [0]
[0]
[c_1] = [0]
[0]
[c_2](x1) = [1 0] x1 + [0]
[0 1] [0]
[++^#](x1, x2) = [0]
[0]
[c_3] = [0]
[0]
[c_4](x1) = [1 0] x1 + [0]
[0 1] [2]
[null^#](x1) = [1]
[0]
[c_5] = [0]
[0]
[c_6] = [0]
[0]
[mem^#](x1, x2) = [0]
[0]
[c_7](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_8] = [0]
[0]
[c_9](x1) = [1 0] x1 + [0]
[0 1] [0]
[max^#](x1) = [0]
[0]
[c_10] = [0]
[0]
[c_11](x1) = [1 0] x1 + [0]
[0 1] [0]
The order satisfies the following ordering constraints:
[f^#(x, nil())] = [0]
[0]
>= [0]
[0]
= [c_1()]
[f^#(x, g(y, z))] = [0]
[0]
>= [0]
[0]
= [c_2(f^#(x, y))]
[++^#(x, nil())] = [0]
[0]
>= [0]
[0]
= [c_3()]
[++^#(x, g(y, z))] = [0]
[0]
? [0]
[2]
= [c_4(++^#(x, y))]
[null^#(nil())] = [1]
[0]
> [0]
[0]
= [c_5()]
[null^#(g(x, y))] = [1]
[0]
> [0]
[0]
= [c_6()]
[mem^#(x, max(x))] = [0]
[0]
? [1]
[0]
= [c_7(null^#(x))]
[mem^#(nil(), y)] = [0]
[0]
>= [0]
[0]
= [c_8()]
[mem^#(g(x, y), z)] = [0]
[0]
>= [0]
[0]
= [c_9(mem^#(x, z))]
[max^#(g(g(nil(), x), y))] = [0]
[0]
>= [0]
[0]
= [c_10()]
[max^#(g(g(g(x, y), z), u()))] = [0]
[0]
>= [0]
[0]
= [c_11(max^#(g(g(x, y), z)))]
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:
{ f^#(x, nil()) -> c_1()
, f^#(x, g(y, z)) -> c_2(f^#(x, y))
, ++^#(x, nil()) -> c_3()
, ++^#(x, g(y, z)) -> c_4(++^#(x, y))
, mem^#(x, max(x)) -> c_7(null^#(x))
, mem^#(nil(), y) -> c_8()
, mem^#(g(x, y), z) -> c_9(mem^#(x, z))
, max^#(g(g(nil(), x), y)) -> c_10()
, max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) }
Weak DPs:
{ null^#(nil()) -> c_5()
, null^#(g(x, y)) -> c_6() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of {1,3,5,6,8} by
applications of Pre({1,3,5,6,8}) = {2,4,7,9}. Here rules are
labeled as follows:
DPs:
{ 1: f^#(x, nil()) -> c_1()
, 2: f^#(x, g(y, z)) -> c_2(f^#(x, y))
, 3: ++^#(x, nil()) -> c_3()
, 4: ++^#(x, g(y, z)) -> c_4(++^#(x, y))
, 5: mem^#(x, max(x)) -> c_7(null^#(x))
, 6: mem^#(nil(), y) -> c_8()
, 7: mem^#(g(x, y), z) -> c_9(mem^#(x, z))
, 8: max^#(g(g(nil(), x), y)) -> c_10()
, 9: max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z)))
, 10: null^#(nil()) -> c_5()
, 11: null^#(g(x, y)) -> c_6() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ f^#(x, g(y, z)) -> c_2(f^#(x, y))
, ++^#(x, g(y, z)) -> c_4(++^#(x, y))
, mem^#(g(x, y), z) -> c_9(mem^#(x, z))
, max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) }
Weak DPs:
{ f^#(x, nil()) -> c_1()
, ++^#(x, nil()) -> c_3()
, null^#(nil()) -> c_5()
, null^#(g(x, y)) -> c_6()
, mem^#(x, max(x)) -> c_7(null^#(x))
, mem^#(nil(), y) -> c_8()
, max^#(g(g(nil(), x), y)) -> c_10() }
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.
{ f^#(x, nil()) -> c_1()
, ++^#(x, nil()) -> c_3()
, null^#(nil()) -> c_5()
, null^#(g(x, y)) -> c_6()
, mem^#(x, max(x)) -> c_7(null^#(x))
, mem^#(nil(), y) -> c_8()
, max^#(g(g(nil(), x), y)) -> c_10() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ f^#(x, g(y, z)) -> c_2(f^#(x, y))
, ++^#(x, g(y, z)) -> c_4(++^#(x, y))
, mem^#(g(x, y), z) -> c_9(mem^#(x, z))
, max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
to orient following rules strictly.
DPs:
{ 1: f^#(x, g(y, z)) -> c_2(f^#(x, y))
, 2: ++^#(x, g(y, z)) -> c_4(++^#(x, y))
, 3: mem^#(g(x, y), z) -> c_9(mem^#(x, z))
, 4: max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) }
Sub-proof:
----------
The input was oriented with the instance of 'Small Polynomial Path
Order (PS,1-bounded)' as induced by the safe mapping
safe(g) = {1, 2}, safe(u) = {}, safe(f^#) = {1}, safe(c_2) = {},
safe(++^#) = {1}, safe(c_4) = {}, safe(mem^#) = {2},
safe(c_9) = {}, safe(max^#) = {}, safe(c_11) = {}
and precedence
empty .
Following symbols are considered recursive:
{f^#, ++^#, mem^#, max^#}
The recursion depth is 1.
Further, following argument filtering is employed:
pi(g) = [1, 2], pi(u) = [], pi(f^#) = [2], pi(c_2) = [1],
pi(++^#) = [2], pi(c_4) = [1], pi(mem^#) = [1], pi(c_9) = [1],
pi(max^#) = [1], pi(c_11) = [1]
Usable defined function symbols are a subset of:
{f^#, ++^#, mem^#, max^#}
For your convenience, here are the satisfied ordering constraints:
pi(f^#(x, g(y, z))) = f^#(g(; y, z);)
> c_2(f^#(y;);)
= pi(c_2(f^#(x, y)))
pi(++^#(x, g(y, z))) = ++^#(g(; y, z);)
> c_4(++^#(y;);)
= pi(c_4(++^#(x, y)))
pi(mem^#(g(x, y), z)) = mem^#(g(; x, y);)
> c_9(mem^#(x;);)
= pi(c_9(mem^#(x, z)))
pi(max^#(g(g(g(x, y), z), u()))) = max^#(g(; g(; g(; x, y), z), u());)
> c_11(max^#(g(; g(; x, y), z););)
= pi(c_11(max^#(g(g(x, y), z))))
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:
{ f^#(x, g(y, z)) -> c_2(f^#(x, y))
, ++^#(x, g(y, z)) -> c_4(++^#(x, y))
, mem^#(g(x, y), z) -> c_9(mem^#(x, z))
, max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) }
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.
{ f^#(x, g(y, z)) -> c_2(f^#(x, y))
, ++^#(x, g(y, z)) -> c_4(++^#(x, y))
, mem^#(g(x, y), z) -> c_9(mem^#(x, z))
, max^#(g(g(g(x, y), z), u())) -> c_11(max^#(g(g(x, y), z))) }
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))