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