interpretations
YES(?,O(n^2))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict Trs:
{ U11(tt(), M, N) -> U12(tt(), M, N)
, U12(tt(), M, N) -> s(plus(N, M))
, plus(N, s(M)) -> U11(tt(), M, N)
, plus(N, 0()) -> N
, U21(tt(), M, N) -> U22(tt(), M, N)
, U22(tt(), M, N) -> plus(x(N, M), N)
, x(N, s(M)) -> U21(tt(), M, N)
, x(N, 0()) -> 0() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
The following argument positions are usable:
Uargs(U11) = {}, Uargs(U12) = {}, Uargs(s) = {1},
Uargs(plus) = {1}, Uargs(U21) = {}, Uargs(U22) = {}, Uargs(x) = {}
TcT has computed following constructor-restricted polynomial
interpretation.
[U11](x1, x2, x3) = 3 + 3*x1 + 3*x1^2 + 3*x2 + x3
[tt]() = 1
[U12](x1, x2, x3) = 3 + x1 + x1^2 + 3*x2 + x3
[s](x1) = 3 + x1
[plus](x1, x2) = 1 + x1 + 3*x2
[U21](x1, x2, x3) = 3 + 2*x1 + x1*x3 + x2 + 2*x2*x3 + 3*x2^2 + 3*x3
[U22](x1, x2, x3) = 1 + 3*x1 + x1*x3 + x2 + 2*x2*x3 + 3*x2^2 + 3*x3
[x](x1, x2) = 1 + 2*x1*x2 + 3*x2^2
[0]() = 2
This order satisfies following ordering constraints
[U11(tt(), M, N)] = 9 + 3*M + N
> 5 + 3*M + N
= [U12(tt(), M, N)]
[U12(tt(), M, N)] = 5 + 3*M + N
> 4 + N + 3*M
= [s(plus(N, M))]
[plus(N, s(M))] = 10 + N + 3*M
> 9 + 3*M + N
= [U11(tt(), M, N)]
[plus(N, 0())] = 7 + N
> N
= [N]
[U21(tt(), M, N)] = 5 + 4*N + M + 2*M*N + 3*M^2
> 4 + 4*N + M + 2*M*N + 3*M^2
= [U22(tt(), M, N)]
[U22(tt(), M, N)] = 4 + 4*N + M + 2*M*N + 3*M^2
> 2 + 2*N*M + 3*M^2 + 3*N
= [plus(x(N, M), N)]
[x(N, s(M))] = 28 + 6*N + 2*N*M + 18*M + 3*M^2
> 5 + 4*N + M + 2*M*N + 3*M^2
= [U21(tt(), M, N)]
[x(N, 0())] = 13 + 4*N
> 2
= [0()]
Hurray, we answered YES(?,O(n^2))
lmpo
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ U11(tt(), M, N) -> U12(tt(), M, N)
, U12(tt(), M, N) -> s(plus(N, M))
, U21(tt(), M, N) -> U22(tt(), M, N)
, U22(tt(), M, N) -> plus(x(N, M), N)
, plus(N, 0()) -> N
, plus(N, s(M)) -> U11(tt(), M, N)
, x(N, 0()) -> 0()
, x(N, s(M)) -> U21(tt(), M, N) }
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:
{ U11(tt(), M, N) -> U12(tt(), M, N)
, U12(tt(), M, N) -> s(plus(N, M))
, U21(tt(), M, N) -> U22(tt(), M, N)
, U22(tt(), M, N) -> plus(x(N, M), N)
, plus(N, 0()) -> N
, plus(N, s(M)) -> U11(tt(), M, N)
, x(N, 0()) -> 0()
, x(N, s(M)) -> U21(tt(), M, N) }
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:
{ U11(tt(), M, N) -> U12(tt(), M, N)
, U12(tt(), M, N) -> s(plus(N, M))
, U21(tt(), M, N) -> U22(tt(), M, N)
, U22(tt(), M, N) -> plus(x(N, M), N)
, plus(N, 0()) -> N
, plus(N, s(M)) -> U11(tt(), M, N)
, x(N, 0()) -> 0()
, x(N, s(M)) -> U21(tt(), M, N) }
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:
{ U11(tt(), M, N) -> U12(tt(), M, N)
, U12(tt(), M, N) -> s(plus(N, M))
, U21(tt(), M, N) -> U22(tt(), M, N)
, U22(tt(), M, N) -> plus(x(N, M), N)
, plus(N, 0()) -> N
, plus(N, s(M)) -> U11(tt(), M, N)
, x(N, 0()) -> 0()
, x(N, s(M)) -> U21(tt(), M, N) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..