interpretations
YES(?,O(n^3))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^3)).
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:
innermost runtime complexity
Answer:
YES(?,O(n^3))
The following argument positions are usable:
Uargs(eq) = {}, Uargs(s) = {}, Uargs(rm) = {}, Uargs(add) = {2},
Uargs(ifrm) = {1}, Uargs(purge) = {1}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[0 0 0] [0 0 2] [2]
[eq](x1, x2) = [0 1 0] x1 + [0 0 1] x2 + [0]
[0 0 0] [0 0 1] [0]
[0]
[0] = [1]
[0]
[0]
[true] = [0]
[0]
[1 0 0] [2]
[s](x1) = [0 1 0] x1 + [0]
[0 0 1] [1]
[0]
[false] = [0]
[0]
[1 2 2] [2]
[rm](x1, x2) = [0 1 0] x2 + [0]
[0 0 1] [0]
[1]
[nil] = [0]
[0]
[0 2 2] [1 3 2] [2]
[add](x1, x2) = [0 0 1] x1 + [0 1 3] x2 + [2]
[0 0 1] [0 0 1] [2]
[1 0 0] [1 2 0] [0]
[ifrm](x1, x2, x3) = [0 0 0] x1 + [0 1 0] x3 + [0]
[0 0 0] [0 0 1] [0]
[3 1 2] [0]
[purge](x1) = [0 1 0] x1 + [1]
[0 0 1] [0]
This order satisfies following ordering constraints
[eq(0(), 0())] = [2]
[1]
[0]
> [0]
[0]
[0]
= [true()]
[eq(0(), s(X))] = [0 0 2] [4]
[0 0 1] X + [2]
[0 0 1] [1]
> [0]
[0]
[0]
= [false()]
[eq(s(X), 0())] = [0 0 0] [2]
[0 1 0] X + [0]
[0 0 0] [0]
> [0]
[0]
[0]
= [false()]
[eq(s(X), s(Y))] = [0 0 0] [0 0 2] [4]
[0 1 0] X + [0 0 1] Y + [1]
[0 0 0] [0 0 1] [1]
> [0 0 0] [0 0 2] [2]
[0 1 0] X + [0 0 1] Y + [0]
[0 0 0] [0 0 1] [0]
= [eq(X, Y)]
[rm(N, nil())] = [3]
[0]
[0]
> [1]
[0]
[0]
= [nil()]
[rm(N, add(M, X))] = [1 5 10] [0 2 6] [12]
[0 1 3] X + [0 0 1] M + [2]
[0 0 1] [0 0 1] [2]
> [1 5 8] [0 2 6] [8]
[0 1 3] X + [0 0 1] M + [2]
[0 0 1] [0 0 1] [2]
= [ifrm(eq(N, M), N, add(M, X))]
[ifrm(true(), N, add(M, X))] = [1 5 8] [0 2 4] [6]
[0 1 3] X + [0 0 1] M + [2]
[0 0 1] [0 0 1] [2]
> [1 2 2] [2]
[0 1 0] X + [0]
[0 0 1] [0]
= [rm(N, X)]
[ifrm(false(), N, add(M, X))] = [1 5 8] [0 2 4] [6]
[0 1 3] X + [0 0 1] M + [2]
[0 0 1] [0 0 1] [2]
> [1 5 4] [0 2 2] [4]
[0 1 3] X + [0 0 1] M + [2]
[0 0 1] [0 0 1] [2]
= [add(M, rm(N, X))]
[purge(nil())] = [3]
[1]
[0]
> [1]
[0]
[0]
= [nil()]
[purge(add(N, X))] = [3 10 11] [0 6 9] [12]
[0 1 3] X + [0 0 1] N + [3]
[0 0 1] [0 0 1] [2]
> [3 10 10] [0 2 2] [11]
[0 1 3] X + [0 0 1] N + [3]
[0 0 1] [0 0 1] [2]
= [add(N, purge(rm(N, X)))]
Hurray, we answered YES(?,O(n^3))
lmpo
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
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:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
mpo
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
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:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
popstar
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
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:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
popstar-ps
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
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:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..