Tool CaT
stdout:
MAYBE
Problem:
car(cons(x,l)) -> x
cddr(nil()) -> nil()
cddr(cons(x,nil())) -> nil()
cddr(cons(x,cons(y,l))) -> l
cadr(cons(x,cons(y,l))) -> y
isZero(0()) -> true()
isZero(s(x)) -> false()
plus(x,y) -> ifplus(isZero(x),x,y)
ifplus(true(),x,y) -> y
ifplus(false(),x,y) -> s(plus(p(x),y))
times(x,y) -> iftimes(isZero(x),x,y)
iftimes(true(),x,y) -> 0()
iftimes(false(),x,y) -> plus(y,times(p(x),y))
p(s(x)) -> x
p(0()) -> 0()
shorter(nil(),y) -> true()
shorter(cons(x,l),0()) -> false()
shorter(cons(x,l),s(y)) -> shorter(l,y)
prod(l) -> if(shorter(l,0()),shorter(l,s(0())),l)
if(true(),b,l) -> s(0())
if(false(),b,l) -> if2(b,l)
if2(true(),l) -> car(l)
if2(false(),l) -> prod(cons(times(car(l),cadr(l)),cddr(l)))
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:
{ car(cons(x, l)) -> x
, cddr(nil()) -> nil()
, cddr(cons(x, nil())) -> nil()
, cddr(cons(x, cons(y, l))) -> l
, cadr(cons(x, cons(y, l))) -> y
, isZero(0()) -> true()
, isZero(s(x)) -> false()
, plus(x, y) -> ifplus(isZero(x), x, y)
, ifplus(true(), x, y) -> y
, ifplus(false(), x, y) -> s(plus(p(x), y))
, times(x, y) -> iftimes(isZero(x), x, y)
, iftimes(true(), x, y) -> 0()
, iftimes(false(), x, y) -> plus(y, times(p(x), y))
, p(s(x)) -> x
, p(0()) -> 0()
, shorter(nil(), y) -> true()
, shorter(cons(x, l), 0()) -> false()
, shorter(cons(x, l), s(y)) -> shorter(l, y)
, prod(l) -> if(shorter(l, 0()), shorter(l, s(0())), l)
, if(true(), b, l) -> s(0())
, if(false(), b, l) -> if2(b, l)
, if2(true(), l) -> car(l)
, if2(false(), l) -> prod(cons(times(car(l), cadr(l)), cddr(l)))}
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:
{ car(cons(x, l)) -> x
, cddr(nil()) -> nil()
, cddr(cons(x, nil())) -> nil()
, cddr(cons(x, cons(y, l))) -> l
, cadr(cons(x, cons(y, l))) -> y
, isZero(0()) -> true()
, isZero(s(x)) -> false()
, plus(x, y) -> ifplus(isZero(x), x, y)
, ifplus(true(), x, y) -> y
, ifplus(false(), x, y) -> s(plus(p(x), y))
, times(x, y) -> iftimes(isZero(x), x, y)
, iftimes(true(), x, y) -> 0()
, iftimes(false(), x, y) -> plus(y, times(p(x), y))
, p(s(x)) -> x
, p(0()) -> 0()
, shorter(nil(), y) -> true()
, shorter(cons(x, l), 0()) -> false()
, shorter(cons(x, l), s(y)) -> shorter(l, y)
, prod(l) -> if(shorter(l, 0()), shorter(l, s(0())), l)
, if(true(), b, l) -> s(0())
, if(false(), b, l) -> if2(b, l)
, if2(true(), l) -> car(l)
, if2(false(), l) -> prod(cons(times(car(l), cadr(l)), cddr(l)))}
Proof Output:
Computation stopped due to timeout after 60.0 seconds