We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ and(tt(), X) -> activate(X)
, activate(X) -> X
, plus(N, 0()) -> N
, plus(N, s(M)) -> s(plus(N, M))
, x(N, 0()) -> 0()
, x(N, s(M)) -> plus(x(N, M), N) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs:
{ and(tt(), X) -> activate(X)
, activate(X) -> X }
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(plus) = {1}, Uargs(s) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[and](x1, x2) = [7] x2 + [6]
[tt] = [0]
[activate](x1) = [1] x1 + [5]
[plus](x1, x2) = [1] x1 + [0]
[0] = [0]
[s](x1) = [1] x1 + [0]
[x](x1, x2) = [0]
The order satisfies the following ordering constraints:
[and(tt(), X)] = [7] X + [6]
> [1] X + [5]
= [activate(X)]
[activate(X)] = [1] X + [5]
> [1] X + [0]
= [X]
[plus(N, 0())] = [1] N + [0]
>= [1] N + [0]
= [N]
[plus(N, s(M))] = [1] N + [0]
>= [1] N + [0]
= [s(plus(N, M))]
[x(N, 0())] = [0]
>= [0]
= [0()]
[x(N, s(M))] = [0]
>= [0]
= [plus(x(N, M), N)]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ plus(N, 0()) -> N
, plus(N, s(M)) -> s(plus(N, M))
, x(N, 0()) -> 0()
, x(N, s(M)) -> plus(x(N, M), N) }
Weak Trs:
{ and(tt(), X) -> activate(X)
, activate(X) -> X }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
Trs: { x(N, 0()) -> 0() }
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(plus) = {1}, Uargs(s) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[and](x1, x2) = [1] x1 + [7] x2 + [0]
[tt] = [1]
[activate](x1) = [1] x1 + [0]
[plus](x1, x2) = [1] x1 + [0]
[0] = [0]
[s](x1) = [1] x1 + [0]
[x](x1, x2) = [1]
The order satisfies the following ordering constraints:
[and(tt(), X)] = [7] X + [1]
> [1] X + [0]
= [activate(X)]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[plus(N, 0())] = [1] N + [0]
>= [1] N + [0]
= [N]
[plus(N, s(M))] = [1] N + [0]
>= [1] N + [0]
= [s(plus(N, M))]
[x(N, 0())] = [1]
> [0]
= [0()]
[x(N, s(M))] = [1]
>= [1]
= [plus(x(N, M), N)]
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ plus(N, 0()) -> N
, plus(N, s(M)) -> s(plus(N, M))
, x(N, s(M)) -> plus(x(N, M), N) }
Weak Trs:
{ and(tt(), X) -> activate(X)
, activate(X) -> X
, x(N, 0()) -> 0() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(plus) = {1}, Uargs(s) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[and](x1, x2) = [1] x1 + [1] x2 + [1]
[tt] = [0]
[activate](x1) = [1] x1 + [0]
[plus](x1, x2) = [1] x1 + [4]
[0] = [0]
[s](x1) = [1] x1 + [4]
[x](x1, x2) = [1] x2 + [1]
The order satisfies the following ordering constraints:
[and(tt(), X)] = [1] X + [1]
> [1] X + [0]
= [activate(X)]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[plus(N, 0())] = [1] N + [4]
> [1] N + [0]
= [N]
[plus(N, s(M))] = [1] N + [4]
? [1] N + [8]
= [s(plus(N, M))]
[x(N, 0())] = [1]
> [0]
= [0()]
[x(N, s(M))] = [1] M + [5]
>= [1] M + [5]
= [plus(x(N, M), N)]
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^2)).
Strict Trs:
{ plus(N, s(M)) -> s(plus(N, M))
, x(N, s(M)) -> plus(x(N, M), N) }
Weak Trs:
{ and(tt(), X) -> activate(X)
, activate(X) -> X
, plus(N, 0()) -> N
, x(N, 0()) -> 0() }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(plus) = {1}, Uargs(s) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[and](x1, x2) = [1] x1 + [1] x2 + [1]
[tt] = [0]
[activate](x1) = [1] x1 + [0]
[plus](x1, x2) = [1] x1 + [0]
[0] = [0]
[s](x1) = [1] x1 + [4]
[x](x1, x2) = [1] x2 + [0]
The order satisfies the following ordering constraints:
[and(tt(), X)] = [1] X + [1]
> [1] X + [0]
= [activate(X)]
[activate(X)] = [1] X + [0]
>= [1] X + [0]
= [X]
[plus(N, 0())] = [1] N + [0]
>= [1] N + [0]
= [N]
[plus(N, s(M))] = [1] N + [0]
? [1] N + [4]
= [s(plus(N, M))]
[x(N, 0())] = [0]
>= [0]
= [0()]
[x(N, s(M))] = [1] M + [4]
> [1] M + [0]
= [plus(x(N, M), N)]
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^2)).
Strict Trs: { plus(N, s(M)) -> s(plus(N, M)) }
Weak Trs:
{ and(tt(), X) -> activate(X)
, activate(X) -> X
, plus(N, 0()) -> N
, x(N, 0()) -> 0()
, x(N, s(M)) -> plus(x(N, M), N) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.
Trs: { plus(N, s(M)) -> s(plus(N, M)) }
The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).
Sub-proof:
----------
The following argument positions are considered usable:
Uargs(plus) = {1}, Uargs(s) = {1}
TcT has computed the following constructor-restricted polynomial
interpretation.
[and](x1, x2) = 2*x2 + 2*x2^2
[tt]() = 0
[activate](x1) = x1
[plus](x1, x2) = 1 + x1 + 2*x2
[0]() = 0
[s](x1) = 2 + x1
[x](x1, x2) = 1 + 2*x1*x2 + 2*x2
This order satisfies the following ordering constraints.
[and(tt(), X)] = 2*X + 2*X^2
>= X
= [activate(X)]
[activate(X)] = X
>= X
= [X]
[plus(N, 0())] = 1 + N
> N
= [N]
[plus(N, s(M))] = 5 + N + 2*M
> 3 + N + 2*M
= [s(plus(N, M))]
[x(N, 0())] = 1
>
= [0()]
[x(N, s(M))] = 5 + 4*N + 2*N*M + 2*M
> 2 + 2*N*M + 2*M + 2*N
= [plus(x(N, M), N)]
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:
{ and(tt(), X) -> activate(X)
, activate(X) -> X
, plus(N, 0()) -> N
, plus(N, s(M)) -> s(plus(N, M))
, x(N, 0()) -> 0()
, x(N, s(M)) -> plus(x(N, M), N) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^2))