interpretations
Execution Time (secs) | - |
Answer | YES(?,O(n^1)) |
Input | SK90 2.44 |
YES(?,O(n^1))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict Trs:
{ del(.(x, .(y, z))) -> f(=(x, y), x, y, z)
, f(true(), x, y, z) -> del(.(y, z))
, f(false(), x, y, z) -> .(x, del(.(y, z)))
, =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v()))
, =(.(x, y), nil()) -> false()
, =(nil(), .(y, z)) -> false()
, =(nil(), nil()) -> true() }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^1))
The following argument positions are usable:
Uargs(del) = {}, Uargs(.) = {2}, Uargs(f) = {1}, Uargs(=) = {},
Uargs(and) = {}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[del](x1) = [3] x1 + [0]
[.](x1, x2) = [1] x1 + [1] x2 + [2]
[f](x1, x2, x3, x4) = [2] x1 + [1] x2 + [3] x3 + [3] x4 + [3]
[=](x1, x2) = [1] x1 + [2]
[true] = [2]
[false] = [3]
[nil] = [2]
[u] = [0]
[v] = [0]
[and](x1, x2) = [3]
This order satisfies following ordering constraints
[del(.(x, .(y, z)))] = [3] x + [3] y + [3] z + [12]
> [3] x + [3] y + [3] z + [7]
= [f(=(x, y), x, y, z)]
[f(true(), x, y, z)] = [1] x + [3] y + [3] z + [7]
> [3] y + [3] z + [6]
= [del(.(y, z))]
[f(false(), x, y, z)] = [1] x + [3] y + [3] z + [9]
> [1] x + [3] y + [3] z + [8]
= [.(x, del(.(y, z)))]
[=(.(x, y), .(u(), v()))] = [1] x + [1] y + [4]
> [3]
= [and(=(x, u()), =(y, v()))]
[=(.(x, y), nil())] = [1] x + [1] y + [4]
> [3]
= [false()]
[=(nil(), .(y, z))] = [4]
> [3]
= [false()]
[=(nil(), nil())] = [4]
> [2]
= [true()]
Hurray, we answered YES(?,O(n^1))
lmpo
Execution Time (secs) | - |
Answer | MAYBE |
Input | SK90 2.44 |
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ del(.(x, .(y, z))) -> f(=(x, y), x, y, z)
, f(true(), x, y, z) -> del(.(y, z))
, f(false(), x, y, z) -> .(x, del(.(y, z)))
, =(nil(), nil()) -> true()
, =(.(x, y), nil()) -> false()
, =(nil(), .(y, z)) -> false()
, =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v())) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
mpo
Execution Time (secs) | - |
Answer | MAYBE |
Input | SK90 2.44 |
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ del(.(x, .(y, z))) -> f(=(x, y), x, y, z)
, f(true(), x, y, z) -> del(.(y, z))
, f(false(), x, y, z) -> .(x, del(.(y, z)))
, =(nil(), nil()) -> true()
, =(.(x, y), nil()) -> false()
, =(nil(), .(y, z)) -> false()
, =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v())) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
popstar
Execution Time (secs) | 0.301 |
Answer | MAYBE |
Input | SK90 2.44 |
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ del(.(x, .(y, z))) -> f(=(x, y), x, y, z)
, f(true(), x, y, z) -> del(.(y, z))
, f(false(), x, y, z) -> .(x, del(.(y, z)))
, =(nil(), nil()) -> true()
, =(.(x, y), nil()) -> false()
, =(nil(), .(y, z)) -> false()
, =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v())) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
popstar-ps
Execution Time (secs) | 0.279 |
Answer | MAYBE |
Input | SK90 2.44 |
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ del(.(x, .(y, z))) -> f(=(x, y), x, y, z)
, f(true(), x, y, z) -> del(.(y, z))
, f(false(), x, y, z) -> .(x, del(.(y, z)))
, =(nil(), nil()) -> true()
, =(.(x, y), nil()) -> false()
, =(nil(), .(y, z)) -> false()
, =(.(x, y), .(u(), v())) -> and(=(x, u()), =(y, v())) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..