interpretations
YES(?,O(n^1))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict Trs:
{ is_empty(nil()) -> true()
, is_empty(cons(x, l)) -> false()
, hd(cons(x, l)) -> x
, tl(cons(x, l)) -> l
, append(l1, l2) -> ifappend(l1, l2, l1)
, ifappend(l1, l2, nil()) -> l2
, ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2)) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^1))
The following argument positions are usable:
Uargs(is_empty) = {}, Uargs(cons) = {2}, Uargs(hd) = {},
Uargs(tl) = {}, Uargs(append) = {}, Uargs(ifappend) = {}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[is_empty](x1) = [2] x1 + [0]
[nil] = [2]
[true] = [0]
[cons](x1, x2) = [1] x1 + [1] x2 + [2]
[false] = [0]
[hd](x1) = [2] x1 + [0]
[tl](x1) = [2] x1 + [0]
[append](x1, x2) = [2] x1 + [1] x2 + [1]
[ifappend](x1, x2, x3) = [1] x2 + [2] x3 + [0]
This order satisfies following ordering constraints
[is_empty(nil())] = [4]
> [0]
= [true()]
[is_empty(cons(x, l))] = [2] x + [2] l + [4]
> [0]
= [false()]
[hd(cons(x, l))] = [2] x + [2] l + [4]
> [1] x + [0]
= [x]
[tl(cons(x, l))] = [2] x + [2] l + [4]
> [1] l + [0]
= [l]
[append(l1, l2)] = [2] l1 + [1] l2 + [1]
> [2] l1 + [1] l2 + [0]
= [ifappend(l1, l2, l1)]
[ifappend(l1, l2, nil())] = [1] l2 + [4]
> [1] l2 + [0]
= [l2]
[ifappend(l1, l2, cons(x, l))] = [2] x + [2] l + [1] l2 + [4]
> [1] x + [2] l + [1] l2 + [3]
= [cons(x, append(l, l2))]
Hurray, we answered YES(?,O(n^1))
lmpo
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ is_empty(nil()) -> true()
, is_empty(cons(x, l)) -> false()
, hd(cons(x, l)) -> x
, tl(cons(x, l)) -> l
, append(l1, l2) -> ifappend(l1, l2, l1)
, ifappend(l1, l2, nil()) -> l2
, ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2)) }
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:
{ is_empty(nil()) -> true()
, is_empty(cons(x, l)) -> false()
, hd(cons(x, l)) -> x
, tl(cons(x, l)) -> l
, append(l1, l2) -> ifappend(l1, l2, l1)
, ifappend(l1, l2, nil()) -> l2
, ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2)) }
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:
{ is_empty(nil()) -> true()
, is_empty(cons(x, l)) -> false()
, hd(cons(x, l)) -> x
, tl(cons(x, l)) -> l
, append(l1, l2) -> ifappend(l1, l2, l1)
, ifappend(l1, l2, nil()) -> l2
, ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2)) }
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:
{ is_empty(nil()) -> true()
, is_empty(cons(x, l)) -> false()
, hd(cons(x, l)) -> x
, tl(cons(x, l)) -> l
, append(l1, l2) -> ifappend(l1, l2, l1)
, ifappend(l1, l2, nil()) -> l2
, ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2)) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..