Tool CaT
stdout:
YES(?,O(n^1))
Problem:
p(m,n,s(r)) -> p(m,r,n)
p(m,s(n),0()) -> p(0(),n,m)
p(m,0(),0()) -> m
Proof:
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {3}
transitions:
p1(1,1,1) -> 3*
p1(2,2,1) -> 3*
p1(1,1,2) -> 3*
p1(2,2,2) -> 3*
p1(1,2,1) -> 3*
p1(2,1,1) -> 3*
p1(1,2,2) -> 3*
p1(2,1,2) -> 3*
01() -> 1*
p0(1,1,1) -> 3*
p0(2,2,1) -> 3*
p0(1,1,2) -> 3*
p0(2,2,2) -> 3*
p0(1,2,1) -> 3*
p0(2,1,1) -> 3*
p0(1,2,2) -> 3*
p0(2,1,2) -> 3*
s0(2) -> 1*
s0(1) -> 1*
00() -> 2*
1 -> 3*
2 -> 3*
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:
{ p(m, n, s(r)) -> p(m, r, n)
, p(m, s(n), 0()) -> p(0(), n, m)
, p(m, 0(), 0()) -> m}
Proof Output:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with minimal-enrichment and initial automaton 'match''
--------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ p(m, n, s(r)) -> p(m, r, n)
, p(m, s(n), 0()) -> p(0(), n, m)
, p(m, 0(), 0()) -> m}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ p_0(2, 2, 2) -> 1
, p_1(2, 2, 2) -> 1
, s_0(2) -> 1
, s_0(2) -> 2
, 0_0() -> 1
, 0_0() -> 2
, 0_1() -> 1
, 0_1() -> 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:
{ p(m, n, s(r)) -> p(m, r, n)
, p(m, s(n), 0()) -> p(0(), n, m)
, p(m, 0(), 0()) -> m}
Proof Output:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with minimal-enrichment and initial automaton 'match''
--------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ p(m, n, s(r)) -> p(m, r, n)
, p(m, s(n), 0()) -> p(0(), n, m)
, p(m, 0(), 0()) -> m}
Proof Output:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ p_0(2, 2, 2) -> 1
, p_1(2, 2, 2) -> 1
, s_0(2) -> 1
, s_0(2) -> 2
, 0_0() -> 1
, 0_0() -> 2
, 0_1() -> 1
, 0_1() -> 2}