We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, rm(N, nil()) -> nil()
, rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
, ifrm(true(), N, add(M, X)) -> rm(N, X)
, ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
, purge(nil()) -> nil()
, purge(add(N, X)) -> add(N, purge(rm(N, 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:
{ eq(0(), 0()) -> true()
, rm(N, nil()) -> nil()
, ifrm(true(), N, add(M, X)) -> rm(N, X)
, purge(nil()) -> nil()
, purge(add(N, X)) -> add(N, purge(rm(N, 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(rm) = {2}, Uargs(add) = {2}, Uargs(ifrm) = {1, 3},
Uargs(purge) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[eq](x1, x2) = [2]
[0] = [2]
[true] = [0]
[s](x1) = [1] x1 + [0]
[false] = [2]
[rm](x1, x2) = [1] x2 + [2]
[nil] = [0]
[add](x1, x2) = [1] x1 + [1] x2 + [3]
[ifrm](x1, x2, x3) = [1] x1 + [1] x3 + [0]
[purge](x1) = [4] x1 + [3]
The order satisfies the following ordering constraints:
[eq(0(), 0())] = [2]
> [0]
= [true()]
[eq(0(), s(X))] = [2]
>= [2]
= [false()]
[eq(s(X), 0())] = [2]
>= [2]
= [false()]
[eq(s(X), s(Y))] = [2]
>= [2]
= [eq(X, Y)]
[rm(N, nil())] = [2]
> [0]
= [nil()]
[rm(N, add(M, X))] = [1] X + [1] M + [5]
>= [1] X + [1] M + [5]
= [ifrm(eq(N, M), N, add(M, X))]
[ifrm(true(), N, add(M, X))] = [1] X + [1] M + [3]
> [1] X + [2]
= [rm(N, X)]
[ifrm(false(), N, add(M, X))] = [1] X + [1] M + [5]
>= [1] X + [1] M + [5]
= [add(M, rm(N, X))]
[purge(nil())] = [3]
> [0]
= [nil()]
[purge(add(N, X))] = [4] X + [4] N + [15]
> [4] X + [1] N + [14]
= [add(N, purge(rm(N, X)))]
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:
{ eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
, ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) }
Weak Trs:
{ eq(0(), 0()) -> true()
, rm(N, nil()) -> nil()
, ifrm(true(), N, add(M, X)) -> rm(N, X)
, purge(nil()) -> nil()
, purge(add(N, X)) -> add(N, purge(rm(N, X))) }
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(rm) = {2}, Uargs(add) = {2}, Uargs(ifrm) = {1, 3},
Uargs(purge) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[eq](x1, x2) = [4]
[0] = [0]
[true] = [4]
[s](x1) = [1] x1 + [0]
[false] = [0]
[rm](x1, x2) = [1] x2 + [0]
[nil] = [0]
[add](x1, x2) = [1] x2 + [0]
[ifrm](x1, x2, x3) = [1] x1 + [1] x3 + [0]
[purge](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[eq(0(), 0())] = [4]
>= [4]
= [true()]
[eq(0(), s(X))] = [4]
> [0]
= [false()]
[eq(s(X), 0())] = [4]
> [0]
= [false()]
[eq(s(X), s(Y))] = [4]
>= [4]
= [eq(X, Y)]
[rm(N, nil())] = [0]
>= [0]
= [nil()]
[rm(N, add(M, X))] = [1] X + [0]
? [1] X + [4]
= [ifrm(eq(N, M), N, add(M, X))]
[ifrm(true(), N, add(M, X))] = [1] X + [4]
> [1] X + [0]
= [rm(N, X)]
[ifrm(false(), N, add(M, X))] = [1] X + [0]
>= [1] X + [0]
= [add(M, rm(N, X))]
[purge(nil())] = [0]
>= [0]
= [nil()]
[purge(add(N, X))] = [1] X + [0]
>= [1] X + [0]
= [add(N, purge(rm(N, X)))]
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:
{ eq(s(X), s(Y)) -> eq(X, Y)
, rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
, ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) }
Weak Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, rm(N, nil()) -> nil()
, ifrm(true(), N, add(M, X)) -> rm(N, X)
, purge(nil()) -> nil()
, purge(add(N, X)) -> add(N, purge(rm(N, X))) }
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(rm) = {2}, Uargs(add) = {2}, Uargs(ifrm) = {1, 3},
Uargs(purge) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[eq](x1, x2) = [4]
[0] = [0]
[true] = [4]
[s](x1) = [1] x1 + [0]
[false] = [1]
[rm](x1, x2) = [1] x2 + [0]
[nil] = [0]
[add](x1, x2) = [1] x2 + [0]
[ifrm](x1, x2, x3) = [1] x1 + [1] x3 + [0]
[purge](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[eq(0(), 0())] = [4]
>= [4]
= [true()]
[eq(0(), s(X))] = [4]
> [1]
= [false()]
[eq(s(X), 0())] = [4]
> [1]
= [false()]
[eq(s(X), s(Y))] = [4]
>= [4]
= [eq(X, Y)]
[rm(N, nil())] = [0]
>= [0]
= [nil()]
[rm(N, add(M, X))] = [1] X + [0]
? [1] X + [4]
= [ifrm(eq(N, M), N, add(M, X))]
[ifrm(true(), N, add(M, X))] = [1] X + [4]
> [1] X + [0]
= [rm(N, X)]
[ifrm(false(), N, add(M, X))] = [1] X + [1]
> [1] X + [0]
= [add(M, rm(N, X))]
[purge(nil())] = [0]
>= [0]
= [nil()]
[purge(add(N, X))] = [1] X + [0]
>= [1] X + [0]
= [add(N, purge(rm(N, X)))]
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:
{ eq(s(X), s(Y)) -> eq(X, Y)
, rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) }
Weak Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, rm(N, nil()) -> nil()
, ifrm(true(), N, add(M, X)) -> rm(N, X)
, ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
, purge(nil()) -> nil()
, purge(add(N, X)) -> add(N, purge(rm(N, X))) }
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(rm) = {2}, Uargs(add) = {2}, Uargs(ifrm) = {1, 3},
Uargs(purge) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[eq](x1, x2) = [0 2] x2 + [0]
[0 1] [0]
[0] = [4]
[4]
[true] = [0]
[1]
[s](x1) = [1 0] x1 + [2]
[0 1] [3]
[false] = [3]
[3]
[rm](x1, x2) = [1 7] x2 + [0]
[0 0] [0]
[nil] = [0]
[0]
[add](x1, x2) = [0 3] x1 + [1 7] x2 + [1]
[0 1] [0 0] [1]
[ifrm](x1, x2, x3) = [1 2] x1 + [1 0] x3 + [1]
[0 0] [0 1] [5]
[purge](x1) = [1 0] x1 + [5]
[0 1] [0]
The order satisfies the following ordering constraints:
[eq(0(), 0())] = [8]
[4]
> [0]
[1]
= [true()]
[eq(0(), s(X))] = [0 2] X + [6]
[0 1] [3]
> [3]
[3]
= [false()]
[eq(s(X), 0())] = [8]
[4]
> [3]
[3]
= [false()]
[eq(s(X), s(Y))] = [0 2] Y + [6]
[0 1] [3]
> [0 2] Y + [0]
[0 1] [0]
= [eq(X, Y)]
[rm(N, nil())] = [0]
[0]
>= [0]
[0]
= [nil()]
[rm(N, add(M, X))] = [1 7] X + [0 10] M + [8]
[0 0] [0 0] [0]
? [1 7] X + [0 7] M + [2]
[0 0] [0 1] [6]
= [ifrm(eq(N, M), N, add(M, X))]
[ifrm(true(), N, add(M, X))] = [1 7] X + [0 3] M + [4]
[0 0] [0 1] [6]
> [1 7] X + [0]
[0 0] [0]
= [rm(N, X)]
[ifrm(false(), N, add(M, X))] = [1 7] X + [0 3] M + [11]
[0 0] [0 1] [6]
> [1 7] X + [0 3] M + [1]
[0 0] [0 1] [1]
= [add(M, rm(N, X))]
[purge(nil())] = [5]
[0]
> [0]
[0]
= [nil()]
[purge(add(N, X))] = [1 7] X + [0 3] N + [6]
[0 0] [0 1] [1]
>= [1 7] X + [0 3] N + [6]
[0 0] [0 1] [1]
= [add(N, purge(rm(N, X)))]
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: { rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) }
Weak Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, rm(N, nil()) -> nil()
, ifrm(true(), N, add(M, X)) -> rm(N, X)
, ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
, purge(nil()) -> nil()
, purge(add(N, X)) -> add(N, purge(rm(N, X))) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
Trs: { rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) }
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 usable:
Uargs(rm) = {2}, Uargs(add) = {2}, Uargs(ifrm) = {1, 3},
Uargs(purge) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[eq](x1, x2) = [0]
[0]
[0] = [3]
[0]
[true] = [0]
[0]
[s](x1) = [1 0] x1 + [3]
[0 1] [3]
[false] = [0]
[0]
[rm](x1, x2) = [1 1] x2 + [1]
[0 1] [0]
[nil] = [0]
[0]
[add](x1, x2) = [0 3] x1 + [1 4] x2 + [2]
[0 1] [0 1] [7]
[ifrm](x1, x2, x3) = [5 1] x1 + [1 1] x3 + [0]
[0 0] [0 1] [0]
[purge](x1) = [3 0] x1 + [2]
[0 2] [0]
The order satisfies the following ordering constraints:
[eq(0(), 0())] = [0]
[0]
>= [0]
[0]
= [true()]
[eq(0(), s(X))] = [0]
[0]
>= [0]
[0]
= [false()]
[eq(s(X), 0())] = [0]
[0]
>= [0]
[0]
= [false()]
[eq(s(X), s(Y))] = [0]
[0]
>= [0]
[0]
= [eq(X, Y)]
[rm(N, nil())] = [1]
[0]
> [0]
[0]
= [nil()]
[rm(N, add(M, X))] = [1 5] X + [0 4] M + [10]
[0 1] [0 1] [7]
> [1 5] X + [0 4] M + [9]
[0 1] [0 1] [7]
= [ifrm(eq(N, M), N, add(M, X))]
[ifrm(true(), N, add(M, X))] = [1 5] X + [0 4] M + [9]
[0 1] [0 1] [7]
> [1 1] X + [1]
[0 1] [0]
= [rm(N, X)]
[ifrm(false(), N, add(M, X))] = [1 5] X + [0 4] M + [9]
[0 1] [0 1] [7]
> [1 5] X + [0 3] M + [3]
[0 1] [0 1] [7]
= [add(M, rm(N, X))]
[purge(nil())] = [2]
[0]
> [0]
[0]
= [nil()]
[purge(add(N, X))] = [3 12] X + [0 9] N + [8]
[0 2] [0 2] [14]
> [3 11] X + [0 3] N + [7]
[0 2] [0 1] [7]
= [add(N, purge(rm(N, X)))]
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:
{ eq(0(), 0()) -> true()
, eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, rm(N, nil()) -> nil()
, rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
, ifrm(true(), N, add(M, X)) -> rm(N, X)
, ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
, purge(nil()) -> nil()
, purge(add(N, X)) -> add(N, purge(rm(N, X))) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^2))