Tool CaT
stdout:
MAYBE
Problem:
perfectp(0()) -> false()
perfectp(s(x)) -> f(x,s(0()),s(x),s(x))
f(0(),y,0(),u) -> true()
f(0(),y,s(z),u) -> false()
f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u)
f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
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:
{ perfectp(0()) -> false()
, perfectp(s(x)) -> f(x, s(0()), s(x), s(x))
, f(0(), y, 0(), u) -> true()
, f(0(), y, s(z), u) -> false()
, f(s(x), 0(), z, u) -> f(x, u, minus(z, s(x)), u)
, f(s(x), s(y), z, u) ->
if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))}
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:
{ perfectp(0()) -> false()
, perfectp(s(x)) -> f(x, s(0()), s(x), s(x))
, f(0(), y, 0(), u) -> true()
, f(0(), y, s(z), u) -> false()
, f(s(x), 0(), z, u) -> f(x, u, minus(z, s(x)), u)
, f(s(x), s(y), z, u) ->
if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))}
Proof Output:
The following argument positions are usable:
Uargs(perfectp) = {}, Uargs(s) = {}, Uargs(f) = {},
Uargs(minus) = {}, Uargs(if) = {3}, Uargs(le) = {}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
perfectp(x1) = [7] x1 + [1]
0() = [2]
false() = [0]
s(x1) = [1] x1 + [2]
f(x1, x2, x3, x4) = [2] x1 + [0] x2 + [1] x3 + [3] x4 + [5]
true() = [0]
minus(x1, x2) = [1] x1 + [0] x2 + [3]
if(x1, x2, x3) = [1] x1 + [0] x2 + [1] x3 + [0]
le(x1, x2) = [0] x1 + [0] x2 + [3]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:
{ perfectp(0()) -> false()
, perfectp(s(x)) -> f(x, s(0()), s(x), s(x))
, f(0(), y, 0(), u) -> true()
, f(0(), y, s(z), u) -> false()
, f(s(x), 0(), z, u) -> f(x, u, minus(z, s(x)), u)
, f(s(x), s(y), z, u) ->
if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))}
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:
{ perfectp(0()) -> false()
, perfectp(s(x)) -> f(x, s(0()), s(x), s(x))
, f(0(), y, 0(), u) -> true()
, f(0(), y, s(z), u) -> false()
, f(s(x), 0(), z, u) -> f(x, u, minus(z, s(x)), u)
, f(s(x), s(y), z, u) ->
if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))}
Proof Output:
The following argument positions are usable:
Uargs(perfectp) = {}, Uargs(s) = {}, Uargs(f) = {},
Uargs(minus) = {}, Uargs(if) = {3}, Uargs(le) = {}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
perfectp(x1) = [7] x1 + [1]
0() = [2]
false() = [0]
s(x1) = [1] x1 + [2]
f(x1, x2, x3, x4) = [2] x1 + [0] x2 + [1] x3 + [3] x4 + [5]
true() = [0]
minus(x1, x2) = [1] x1 + [0] x2 + [3]
if(x1, x2, x3) = [1] x1 + [0] x2 + [1] x3 + [0]
le(x1, x2) = [0] x1 + [0] x2 + [3]