Tool CaT
stdout:
YES(?,O(n^1))
Problem:
f(s(X),X) -> f(X,a(X))
f(X,c(X)) -> f(s(X),X)
f(X,X) -> c(X)
Proof:
Bounds Processor:
bound: 3
enrichment: match
automaton:
final states: {19,4}
transitions:
f0(3,1) -> 4*
f0(3,3) -> 4*
f0(19,2) -> 4*
f0(3,19) -> 4*
f0(1,2) -> 4*
f0(2,1) -> 4*
f0(2,3) -> 4*
f0(2,19) -> 4*
f0(3,2) -> 4*
f0(19,1) -> 4*
f0(19,3) -> 4*
f0(19,19) -> 4*
f0(1,1) -> 4*
f0(1,3) -> 4*
f0(1,19) -> 4*
f0(2,2) -> 4*
s0(2) -> 1*
s0(19) -> 1*
s0(1) -> 1*
s0(3) -> 1*
a0(2) -> 2*
a0(19) -> 2*
a0(1) -> 2*
a0(3) -> 2*
c0(2) -> 3*
c0(19) -> 3*
c0(1) -> 3*
c0(3) -> 3*
c1(2) -> 19*,3,4
c1(19) -> 4,3,19*
c1(1) -> 19*,3,4
c1(3) -> 19*,3,4
f1(19,2) -> 4*
f1(1,2) -> 4*
f1(3,2) -> 4*
f1(1,1) -> 4*
f1(1,3) -> 4*
f1(1,19) -> 4*
f1(2,2) -> 4*
s1(2) -> 1*
s1(19) -> 1*
s1(1) -> 1*
s1(3) -> 1*
a1(2) -> 2*
a1(19) -> 2*
a1(1) -> 2*
a1(3) -> 2*
c2(2) -> 3,19*,4
c2(1) -> 3,19*,4
f2(19,2) -> 4*
f2(1,2) -> 4*
f2(3,2) -> 4*
f2(1,1) -> 4*
f2(2,2) -> 4*
s2(1) -> 1*
a2(2) -> 2*
a2(19) -> 2*
a2(1) -> 2*
a2(3) -> 2*
c3(2) -> 19*,3,4
c3(1) -> 19*,3,4
f3(1,2) -> 4*
a3(1) -> 2*
problem:
QedTool IRC1
stdout:
YES(?,O(n^1))
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:
{ f(s(X), X) -> f(X, a(X))
, f(X, c(X)) -> f(s(X), X)
, f(X, X) -> c(X)}
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:
{ f(s(X), X) -> f(X, a(X))
, f(X, c(X)) -> f(s(X), X)
, f(X, X) -> c(X)}
Proof Output:
The following argument positions are usable:
Uargs(f) = {}, Uargs(s) = {}, Uargs(a) = {}, Uargs(c) = {}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
f(x1, x2) = [2] x1 + [3] x2 + [3]
s(x1) = [0] x1 + [2]
a(x1) = [0] x1 + [0]
c(x1) = [1] x1 + [2]Tool RC1
stdout:
YES(?,O(n^1))
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:
{ f(s(X), X) -> f(X, a(X))
, f(X, c(X)) -> f(s(X), X)
, f(X, X) -> c(X)}
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:
{ f(s(X), X) -> f(X, a(X))
, f(X, c(X)) -> f(s(X), X)
, f(X, X) -> c(X)}
Proof Output:
The following argument positions are usable:
Uargs(f) = {}, Uargs(s) = {}, Uargs(a) = {}, Uargs(c) = {}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
f(x1, x2) = [2] x1 + [3] x2 + [3]
s(x1) = [0] x1 + [2]
a(x1) = [0] x1 + [0]
c(x1) = [1] x1 + [2]