Tool CaT
stdout:
MAYBE
Problem:
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))
Proof:
OpenTool IRC1
stdout:
MAYBE
Tool IRC2
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ 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))}
Proof Output:
'matrix-interpretation of dimension 1' proved the best result:
Details:
--------
'matrix-interpretation of dimension 1' succeeded with the following output:
'matrix-interpretation of dimension 1'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ 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))}
Proof Output:
The following argument positions are usable:
Uargs(is_empty) = {}, Uargs(cons) = {2}, Uargs(hd) = {},
Uargs(tl) = {}, Uargs(append) = {}, Uargs(ifappend) = {}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
is_empty(x1) = [0] x1 + [1]
nil() = [2]
true() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [4]
false() = [0]
hd(x1) = [3] x1 + [3]
tl(x1) = [3] x1 + [3]
append(x1, x2) = [2] x1 + [7] x2 + [4]
ifappend(x1, x2, x3) = [0] x1 + [7] x2 + [2] x3 + [1]Tool RC1
stdout:
MAYBE
Tool RC2
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ 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))}
Proof Output:
'matrix-interpretation of dimension 1' proved the best result:
Details:
--------
'matrix-interpretation of dimension 1' succeeded with the following output:
'matrix-interpretation of dimension 1'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ 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))}
Proof Output:
The following argument positions are usable:
Uargs(is_empty) = {}, Uargs(cons) = {2}, Uargs(hd) = {},
Uargs(tl) = {}, Uargs(append) = {}, Uargs(ifappend) = {}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
is_empty(x1) = [0] x1 + [1]
nil() = [2]
true() = [0]
cons(x1, x2) = [1] x1 + [1] x2 + [4]
false() = [0]
hd(x1) = [3] x1 + [3]
tl(x1) = [3] x1 + [3]
append(x1, x2) = [2] x1 + [7] x2 + [4]
ifappend(x1, x2, x3) = [0] x1 + [7] x2 + [2] x3 + [1]