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:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(g) = {1}, Uargs(or) = {2}, Uargs(not) = {1},
Uargs(max') = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[f](x1, x2) = [1] x1 + [1] x2 + [0]
[nil] = [0]
[g](x1, x2) = [1] x1 + [1] x2 + [0]
[++](x1, x2) = [1] x1 + [1] x2 + [0]
[null](x1) = [0]
[true] = [0]
[false] = [0]
[mem](x1, x2) = [0]
[or](x1, x2) = [1] x1 + [1] x2 + [0]
[=](x1, x2) = [5]
[max](x1) = [1] x1 + [0]
[not](x1) = [1] x1 + [0]
[max'](x1, x2) = [1] x1 + [0]
[u] = [1]
The order satisfies the following ordering constraints:
[f(x, nil())] = [1] x + [0]
>= [1] x + [0]
= [g(nil(), x)]
[f(x, g(y, z))] = [1] x + [1] y + [1] z + [0]
>= [1] x + [1] y + [1] z + [0]
= [g(f(x, y), z)]
[++(x, nil())] = [1] x + [0]
>= [1] x + [0]
= [x]
[++(x, g(y, z))] = [1] x + [1] y + [1] z + [0]
>= [1] x + [1] y + [1] z + [0]
= [g(++(x, y), z)]
[null(nil())] = [0]
>= [0]
= [true()]
[null(g(x, y))] = [0]
>= [0]
= [false()]
[mem(x, max(x))] = [0]
>= [0]
= [not(null(x))]
[mem(nil(), y)] = [0]
>= [0]
= [false()]
[mem(g(x, y), z)] = [0]
? [5]
= [or(=(y, z), mem(x, z))]
[max(g(g(nil(), x), y))] = [1] x + [1] y + [0]
>= [1] x + [0]
= [max'(x, y)]
[max(g(g(g(x, y), z), u()))] = [1] x + [1] y + [1] z + [1]
> [1] x + [1] y + [1] z + [0]
= [max'(max(g(g(x, y), z)), u())]
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 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) }
Weak Trs:
{ max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u()) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(g) = {1}, Uargs(or) = {2}, Uargs(not) = {1},
Uargs(max') = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[f](x1, x2) = [1] x1 + [1] x2 + [0]
[nil] = [1]
[g](x1, x2) = [1] x1 + [1] x2 + [0]
[++](x1, x2) = [1] x1 + [1] x2 + [0]
[null](x1) = [1]
[true] = [0]
[false] = [0]
[mem](x1, x2) = [0]
[or](x1, x2) = [1] x1 + [1] x2 + [0]
[=](x1, x2) = [1]
[max](x1) = [1] x1 + [0]
[not](x1) = [1] x1 + [0]
[max'](x1, x2) = [1] x1 + [0]
[u] = [0]
The order satisfies the following ordering constraints:
[f(x, nil())] = [1] x + [1]
>= [1] x + [1]
= [g(nil(), x)]
[f(x, g(y, z))] = [1] x + [1] y + [1] z + [0]
>= [1] x + [1] y + [1] z + [0]
= [g(f(x, y), z)]
[++(x, nil())] = [1] x + [1]
> [1] x + [0]
= [x]
[++(x, g(y, z))] = [1] x + [1] y + [1] z + [0]
>= [1] x + [1] y + [1] z + [0]
= [g(++(x, y), z)]
[null(nil())] = [1]
> [0]
= [true()]
[null(g(x, y))] = [1]
> [0]
= [false()]
[mem(x, max(x))] = [0]
? [1]
= [not(null(x))]
[mem(nil(), y)] = [0]
>= [0]
= [false()]
[mem(g(x, y), z)] = [0]
? [1]
= [or(=(y, z), mem(x, z))]
[max(g(g(nil(), x), y))] = [1] x + [1] y + [1]
> [1] x + [0]
= [max'(x, y)]
[max(g(g(g(x, y), z), u()))] = [1] x + [1] y + [1] z + [0]
>= [1] x + [1] y + [1] z + [0]
= [max'(max(g(g(x, y), z)), u())]
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 Trs:
{ f(x, nil()) -> g(nil(), x)
, f(x, g(y, z)) -> g(f(x, y), z)
, ++(x, g(y, z)) -> g(++(x, y), z)
, mem(x, max(x)) -> not(null(x))
, mem(nil(), y) -> false()
, mem(g(x, y), z) -> or(=(y, z), mem(x, z)) }
Weak Trs:
{ ++(x, nil()) -> x
, null(nil()) -> true()
, null(g(x, y)) -> false()
, 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:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(g) = {1}, Uargs(or) = {2}, Uargs(not) = {1},
Uargs(max') = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[f](x1, x2) = [1] x1 + [1] x2 + [2]
[nil] = [4]
[g](x1, x2) = [1] x1 + [1] x2 + [0]
[++](x1, x2) = [1] x1 + [1] x2 + [0]
[null](x1) = [1]
[true] = [0]
[false] = [0]
[mem](x1, x2) = [1] x1 + [4]
[or](x1, x2) = [1] x1 + [1] x2 + [0]
[=](x1, x2) = [5]
[max](x1) = [1] x1 + [0]
[not](x1) = [1] x1 + [0]
[max'](x1, x2) = [1] x1 + [0]
[u] = [0]
The order satisfies the following ordering constraints:
[f(x, nil())] = [1] x + [6]
> [1] x + [4]
= [g(nil(), x)]
[f(x, g(y, z))] = [1] x + [1] y + [1] z + [2]
>= [1] x + [1] y + [1] z + [2]
= [g(f(x, y), z)]
[++(x, nil())] = [1] x + [4]
> [1] x + [0]
= [x]
[++(x, g(y, z))] = [1] x + [1] y + [1] z + [0]
>= [1] x + [1] y + [1] z + [0]
= [g(++(x, y), z)]
[null(nil())] = [1]
> [0]
= [true()]
[null(g(x, y))] = [1]
> [0]
= [false()]
[mem(x, max(x))] = [1] x + [4]
> [1]
= [not(null(x))]
[mem(nil(), y)] = [8]
> [0]
= [false()]
[mem(g(x, y), z)] = [1] x + [1] y + [4]
? [1] x + [9]
= [or(=(y, z), mem(x, z))]
[max(g(g(nil(), x), y))] = [1] x + [1] y + [4]
> [1] x + [0]
= [max'(x, y)]
[max(g(g(g(x, y), z), u()))] = [1] x + [1] y + [1] z + [0]
>= [1] x + [1] y + [1] z + [0]
= [max'(max(g(g(x, y), z)), u())]
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 Trs:
{ f(x, g(y, z)) -> g(f(x, y), z)
, ++(x, g(y, z)) -> g(++(x, y), z)
, mem(g(x, y), z) -> or(=(y, z), mem(x, z)) }
Weak Trs:
{ f(x, nil()) -> g(nil(), x)
, ++(x, nil()) -> x
, null(nil()) -> true()
, null(g(x, y)) -> false()
, mem(x, max(x)) -> not(null(x))
, mem(nil(), y) -> false()
, 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:
runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(g) = {1}, Uargs(or) = {2}, Uargs(not) = {1},
Uargs(max') = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[f](x1, x2) = [1] x1 + [1] x2 + [4]
[nil] = [3]
[g](x1, x2) = [1] x1 + [1] x2 + [1]
[++](x1, x2) = [1] x1 + [1] x2 + [2]
[null](x1) = [0]
[true] = [0]
[false] = [0]
[mem](x1, x2) = [1] x1 + [0]
[or](x1, x2) = [1] x1 + [1] x2 + [0]
[=](x1, x2) = [0]
[max](x1) = [1] x1 + [0]
[not](x1) = [1] x1 + [0]
[max'](x1, x2) = [1] x1 + [1] x2 + [0]
[u] = [1]
The order satisfies the following ordering constraints:
[f(x, nil())] = [1] x + [7]
> [1] x + [4]
= [g(nil(), x)]
[f(x, g(y, z))] = [1] x + [1] y + [1] z + [5]
>= [1] x + [1] y + [1] z + [5]
= [g(f(x, y), z)]
[++(x, nil())] = [1] x + [5]
> [1] x + [0]
= [x]
[++(x, g(y, z))] = [1] x + [1] y + [1] z + [3]
>= [1] x + [1] y + [1] z + [3]
= [g(++(x, y), z)]
[null(nil())] = [0]
>= [0]
= [true()]
[null(g(x, y))] = [0]
>= [0]
= [false()]
[mem(x, max(x))] = [1] x + [0]
>= [0]
= [not(null(x))]
[mem(nil(), y)] = [3]
> [0]
= [false()]
[mem(g(x, y), z)] = [1] x + [1] y + [1]
> [1] x + [0]
= [or(=(y, z), mem(x, z))]
[max(g(g(nil(), x), y))] = [1] x + [1] y + [5]
> [1] x + [1] y + [0]
= [max'(x, y)]
[max(g(g(g(x, y), z), u()))] = [1] x + [1] y + [1] z + [4]
> [1] x + [1] y + [1] z + [3]
= [max'(max(g(g(x, y), z)), u())]
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 Trs:
{ f(x, g(y, z)) -> g(f(x, y), z)
, ++(x, g(y, z)) -> g(++(x, y), z) }
Weak Trs:
{ f(x, nil()) -> g(nil(), x)
, ++(x, nil()) -> x
, 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:
runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs:
{ f(x, g(y, z)) -> g(f(x, y), z)
, ++(x, g(y, z)) -> g(++(x, y), z) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are usable:
Uargs(g) = {1}, Uargs(or) = {2}, Uargs(not) = {1},
Uargs(max') = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[f](x1, x2) = [2] x1 + [3] x2 + [0]
[nil] = [4]
[g](x1, x2) = [1] x1 + [1] x2 + [3]
[++](x1, x2) = [1] x1 + [3] x2 + [0]
[null](x1) = [0]
[true] = [0]
[false] = [0]
[mem](x1, x2) = [0]
[or](x1, x2) = [1] x1 + [1] x2 + [0]
[=](x1, x2) = [0]
[max](x1) = [1] x1 + [0]
[not](x1) = [1] x1 + [0]
[max'](x1, x2) = [1] x1 + [1] x2 + [0]
[u] = [2]
The order satisfies the following ordering constraints:
[f(x, nil())] = [2] x + [12]
> [1] x + [7]
= [g(nil(), x)]
[f(x, g(y, z))] = [2] x + [3] y + [3] z + [9]
> [2] x + [3] y + [1] z + [3]
= [g(f(x, y), z)]
[++(x, nil())] = [1] x + [12]
> [1] x + [0]
= [x]
[++(x, g(y, z))] = [1] x + [3] y + [3] z + [9]
> [1] x + [3] y + [1] z + [3]
= [g(++(x, y), z)]
[null(nil())] = [0]
>= [0]
= [true()]
[null(g(x, y))] = [0]
>= [0]
= [false()]
[mem(x, max(x))] = [0]
>= [0]
= [not(null(x))]
[mem(nil(), y)] = [0]
>= [0]
= [false()]
[mem(g(x, y), z)] = [0]
>= [0]
= [or(=(y, z), mem(x, z))]
[max(g(g(nil(), x), y))] = [1] x + [1] y + [10]
> [1] x + [1] y + [0]
= [max'(x, y)]
[max(g(g(g(x, y), z), u()))] = [1] x + [1] y + [1] z + [11]
> [1] x + [1] y + [1] z + [8]
= [max'(max(g(g(x, y), z)), u())]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak 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:
runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^1))