interpretations
TIMEOUT
We are left with following problem, upon which TcT provides the
certificate TIMEOUT.
Strict Trs:
{ check(0()) -> zero()
, check(s(0())) -> odd()
, check(s(s(0()))) -> even()
, check(s(s(s(x)))) -> check(s(x))
, half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, plus(0(), y) -> y
, plus(s(x), y) -> s(plus(x, y))
, times(x, y) -> timesIter(x, y, 0())
, timesIter(x, y, z) -> if(check(x), x, y, z, plus(z, y))
, if(zero(), x, y, z, u) -> z
, if(odd(), x, y, z, u) -> timesIter(p(x), y, u)
, if(even(), x, y, z, u) ->
plus(timesIter(half(x), y, half(z)),
timesIter(half(x), y, half(s(z))))
, p(0()) -> 0()
, p(s(x)) -> x }
Obligation:
innermost runtime complexity
Answer:
TIMEOUT
Computation stopped due to timeout after 20.0 seconds.
Arrrr..
lmpo
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ check(0()) -> zero()
, check(s(0())) -> odd()
, check(s(s(0()))) -> even()
, check(s(s(s(x)))) -> check(s(x))
, half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, plus(0(), y) -> y
, plus(s(x), y) -> s(plus(x, y))
, times(x, y) -> timesIter(x, y, 0())
, timesIter(x, y, z) -> if(check(x), x, y, z, plus(z, y))
, p(s(x)) -> x
, p(0()) -> 0()
, if(zero(), x, y, z, u) -> z
, if(odd(), x, y, z, u) -> timesIter(p(x), y, u)
, if(even(), x, y, z, u) ->
plus(timesIter(half(x), y, half(z)),
timesIter(half(x), y, half(s(z)))) }
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:
{ check(0()) -> zero()
, check(s(0())) -> odd()
, check(s(s(0()))) -> even()
, check(s(s(s(x)))) -> check(s(x))
, half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, plus(0(), y) -> y
, plus(s(x), y) -> s(plus(x, y))
, times(x, y) -> timesIter(x, y, 0())
, timesIter(x, y, z) -> if(check(x), x, y, z, plus(z, y))
, p(s(x)) -> x
, p(0()) -> 0()
, if(zero(), x, y, z, u) -> z
, if(odd(), x, y, z, u) -> timesIter(p(x), y, u)
, if(even(), x, y, z, u) ->
plus(timesIter(half(x), y, half(z)),
timesIter(half(x), y, half(s(z)))) }
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:
{ check(0()) -> zero()
, check(s(0())) -> odd()
, check(s(s(0()))) -> even()
, check(s(s(s(x)))) -> check(s(x))
, half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, plus(0(), y) -> y
, plus(s(x), y) -> s(plus(x, y))
, times(x, y) -> timesIter(x, y, 0())
, timesIter(x, y, z) -> if(check(x), x, y, z, plus(z, y))
, p(s(x)) -> x
, p(0()) -> 0()
, if(zero(), x, y, z, u) -> z
, if(odd(), x, y, z, u) -> timesIter(p(x), y, u)
, if(even(), x, y, z, u) ->
plus(timesIter(half(x), y, half(z)),
timesIter(half(x), y, half(s(z)))) }
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:
{ check(0()) -> zero()
, check(s(0())) -> odd()
, check(s(s(0()))) -> even()
, check(s(s(s(x)))) -> check(s(x))
, half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, plus(0(), y) -> y
, plus(s(x), y) -> s(plus(x, y))
, times(x, y) -> timesIter(x, y, 0())
, timesIter(x, y, z) -> if(check(x), x, y, z, plus(z, y))
, p(s(x)) -> x
, p(0()) -> 0()
, if(zero(), x, y, z, u) -> z
, if(odd(), x, y, z, u) -> timesIter(p(x), y, u)
, if(even(), x, y, z, u) ->
plus(timesIter(half(x), y, half(z)),
timesIter(half(x), y, half(s(z)))) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..