interpretations
Execution Time (secs) | - |
Answer | YES(?,O(n^1)) |
Input | SK90 2.45 |
YES(?,O(n^1))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict Trs:
{ admit(x, nil()) -> nil()
, admit(x, .(u, .(v, .(w(), z)))) ->
cond(=(sum(x, u, v), w()),
.(u, .(v, .(w(), admit(carry(x, u, v), z)))))
, cond(true(), y) -> y }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^1))
The following argument positions are usable:
Uargs(admit) = {}, Uargs(.) = {2}, Uargs(cond) = {2},
Uargs(=) = {}, Uargs(sum) = {}, Uargs(carry) = {}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[admit](x1, x2) = [2] x2 + [1]
[nil] = [0]
[.](x1, x2) = [1] x1 + [1] x2 + [0]
[w] = [2]
[cond](x1, x2) = [1] x1 + [1] x2 + [0]
[=](x1, x2) = [1] x1 + [0]
[sum](x1, x2, x3) = [1]
[carry](x1, x2, x3) = [1]
[true] = [2]
This order satisfies following ordering constraints
[admit(x, nil())] = [1]
> [0]
= [nil()]
[admit(x, .(u, .(v, .(w(), z))))] = [2] u + [2] v + [2] z + [5]
> [1] u + [1] v + [2] z + [4]
= [cond(=(sum(x, u, v), w()),
.(u, .(v, .(w(), admit(carry(x, u, v), z)))))]
[cond(true(), y)] = [1] y + [2]
> [1] y + [0]
= [y]
Hurray, we answered YES(?,O(n^1))
lmpo
Execution Time (secs) | - |
Answer | MAYBE |
Input | SK90 2.45 |
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ admit(x, nil()) -> nil()
, admit(x, .(u, .(v, .(w(), z)))) ->
cond(=(sum(x, u, v), w()),
.(u, .(v, .(w(), admit(carry(x, u, v), z)))))
, cond(true(), y) -> y }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
mpo
Execution Time (secs) | - |
Answer | MAYBE |
Input | SK90 2.45 |
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ admit(x, nil()) -> nil()
, admit(x, .(u, .(v, .(w(), z)))) ->
cond(=(sum(x, u, v), w()),
.(u, .(v, .(w(), admit(carry(x, u, v), z)))))
, cond(true(), y) -> y }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
popstar
Execution Time (secs) | 0.349 |
Answer | MAYBE |
Input | SK90 2.45 |
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ admit(x, nil()) -> nil()
, admit(x, .(u, .(v, .(w(), z)))) ->
cond(=(sum(x, u, v), w()),
.(u, .(v, .(w(), admit(carry(x, u, v), z)))))
, cond(true(), y) -> y }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
popstar-ps
Execution Time (secs) | 0.564 |
Answer | YES(?,POLY) |
Input | SK90 2.45 |
YES(?,POLY)
We are left with following problem, upon which TcT provides the
certificate YES(?,POLY).
Strict Trs:
{ admit(x, nil()) -> nil()
, admit(x, .(u, .(v, .(w(), z)))) ->
cond(=(sum(x, u, v), w()),
.(u, .(v, .(w(), admit(carry(x, u, v), z)))))
, cond(true(), y) -> y }
Obligation:
innermost runtime complexity
Answer:
YES(?,POLY)
The input was oriented with the instance of 'Polynomial Path Order
(PS)' as induced by the safe mapping
safe(admit) = {1}, safe(nil) = {}, safe(.) = {1, 2}, safe(w) = {},
safe(cond) = {1, 2}, safe(=) = {1, 2}, safe(sum) = {1, 2, 3},
safe(carry) = {1, 2, 3}, safe(true) = {}
and precedence
admit > cond .
Following symbols are considered recursive:
{admit, cond}
The recursion depth is 2.
For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:
Strict DPs:
Weak DPs :
Strict Trs:
{ admit(nil(); x) -> nil()
, admit(.(; u, .(; v, .(; w(), z))); x) ->
cond(; =(; sum(; x, u, v), w()),
.(; u, .(; v, .(; w(), admit(z; carry(; x, u, v))))))
, cond(; true(), y) -> y }
Weak Trs :
Hurray, we answered YES(?,POLY)