Tool CaT
stdout:
MAYBE
Problem:
isEmpty(empty()) -> true()
isEmpty(node(l,x,r)) -> false()
left(empty()) -> empty()
left(node(l,x,r)) -> l
right(empty()) -> empty()
right(node(l,x,r)) -> r
elem(node(l,x,r)) -> x
append(nil(),x) -> cons(x,nil())
append(cons(y(),ys),x) -> cons(y(),append(ys,x))
listify(n,xs) ->
if(isEmpty(n),isEmpty(left(n)),right(n),node(left(left(n)),elem(left(n)),
node(right(left(n)),elem(n),right(n))),
xs,append(xs,n))
if(true(),b,n,m,xs,ys) -> xs
if(false(),false(),n,m,xs,ys) -> listify(m,xs)
if(false(),true(),n,m,xs,ys) -> listify(n,ys)
toList(n) -> listify(n,nil())
Proof:
OpenTool IRC1
stdout:
MAYBE
Tool IRC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: innermost runtime-complexity with respect to
Rules:
{ isEmpty(empty()) -> true()
, isEmpty(node(l, x, r)) -> false()
, left(empty()) -> empty()
, left(node(l, x, r)) -> l
, right(empty()) -> empty()
, right(node(l, x, r)) -> r
, elem(node(l, x, r)) -> x
, append(nil(), x) -> cons(x, nil())
, append(cons(y(), ys), x) -> cons(y(), append(ys, x))
, listify(n, xs) ->
if(isEmpty(n),
isEmpty(left(n)),
right(n),
node(left(left(n)),
elem(left(n)),
node(right(left(n)), elem(n), right(n))),
xs,
append(xs, n))
, if(true(), b, n, m, xs, ys) -> xs
, if(false(), false(), n, m, xs, ys) -> listify(m, xs)
, if(false(), true(), n, m, xs, ys) -> listify(n, ys)
, toList(n) -> listify(n, nil())}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool RC1
stdout:
MAYBE
Tool RC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: runtime-complexity with respect to
Rules:
{ isEmpty(empty()) -> true()
, isEmpty(node(l, x, r)) -> false()
, left(empty()) -> empty()
, left(node(l, x, r)) -> l
, right(empty()) -> empty()
, right(node(l, x, r)) -> r
, elem(node(l, x, r)) -> x
, append(nil(), x) -> cons(x, nil())
, append(cons(y(), ys), x) -> cons(y(), append(ys, x))
, listify(n, xs) ->
if(isEmpty(n),
isEmpty(left(n)),
right(n),
node(left(left(n)),
elem(left(n)),
node(right(left(n)), elem(n), right(n))),
xs,
append(xs, n))
, if(true(), b, n, m, xs, ys) -> xs
, if(false(), false(), n, m, xs, ys) -> listify(m, xs)
, if(false(), true(), n, m, xs, ys) -> listify(n, ys)
, toList(n) -> listify(n, nil())}
Proof Output:
Computation stopped due to timeout after 60.0 seconds