Tool CaT
stdout:
YES(?,O(n^1))
Problem:
f(a,empty()) -> g(a,empty())
f(a,cons(x,k)) -> f(cons(x,a),k)
g(empty(),d) -> d
g(cons(x,k),d) -> g(k,cons(x,d))
Proof:
Bounds Processor:
bound: 2
enrichment: match
automaton:
final states: {4,3}
transitions:
g1(10,5) -> 3*
g1(1,10) -> 4*
g1(7,5) -> 3*
g1(2,5) -> 3*
g1(2,7) -> 4*
g1(1,5) -> 3*
g1(1,7) -> 4*
g1(2,10) -> 4*
cons1(2,12) -> 5*
cons1(2,14) -> 5*
cons1(1,2) -> 7*
cons1(1,10) -> 7*
cons1(1,12) -> 5*
cons1(1,14) -> 5*
cons1(2,1) -> 7*
cons1(2,5) -> 5*
cons1(2,7) -> 7*
cons1(1,1) -> 7*
cons1(1,5) -> 5*
cons1(1,7) -> 7*
cons1(2,2) -> 10*
cons1(2,10) -> 7*
f1(10,1) -> 3*
f1(7,1) -> 3*
f1(10,2) -> 3*
f1(7,2) -> 3*
empty1() -> 5*
g2(7,12) -> 3*
g2(2,12) -> 3*
g2(7,14) -> 3*
g2(2,14) -> 3*
g2(1,12) -> 3*
g2(1,14) -> 3*
g2(10,12) -> 3*
g2(10,14) -> 3*
f0(1,2) -> 3*
f0(2,1) -> 3*
f0(1,1) -> 3*
f0(2,2) -> 3*
cons2(2,12) -> 12*
cons2(2,14) -> 12*
cons2(1,12) -> 12*
cons2(1,14) -> 12*
cons2(2,5) -> 14*
cons2(1,5) -> 12*
empty0() -> 1*
g0(1,2) -> 4*
g0(2,1) -> 4*
g0(1,1) -> 4*
g0(2,2) -> 4*
cons0(1,2) -> 2*
cons0(2,1) -> 2*
cons0(1,1) -> 2*
cons0(2,2) -> 2*
1 -> 4*
2 -> 4*
5 -> 3*
7 -> 4*
10 -> 4*
12 -> 3*
14 -> 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:
{ f(a, empty()) -> g(a, empty())
, f(a, cons(x, k)) -> f(cons(x, a), k)
, g(empty(), d) -> d
, g(cons(x, k), d) -> g(k, cons(x, d))}
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:
{ f(a, empty()) -> g(a, empty())
, f(a, cons(x, k)) -> f(cons(x, a), k)
, g(empty(), d) -> d
, g(cons(x, k), d) -> g(k, cons(x, d))}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ f_0(2, 2) -> 1
, f_1(4, 2) -> 1
, empty_0() -> 1
, empty_0() -> 2
, empty_1() -> 1
, empty_1() -> 3
, g_0(2, 2) -> 1
, g_1(2, 3) -> 1
, g_1(2, 4) -> 1
, g_1(4, 3) -> 1
, g_2(2, 5) -> 1
, g_2(4, 5) -> 1
, cons_0(2, 2) -> 1
, cons_0(2, 2) -> 2
, cons_1(2, 2) -> 1
, cons_1(2, 2) -> 4
, cons_1(2, 3) -> 1
, cons_1(2, 3) -> 3
, cons_1(2, 4) -> 1
, cons_1(2, 4) -> 4
, cons_1(2, 5) -> 1
, cons_1(2, 5) -> 3
, cons_2(2, 3) -> 1
, cons_2(2, 3) -> 5
, cons_2(2, 5) -> 1
, cons_2(2, 5) -> 5}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(a, empty()) -> g(a, empty())
, f(a, cons(x, k)) -> f(cons(x, a), k)
, g(empty(), d) -> d
, g(cons(x, k), d) -> g(k, cons(x, d))}
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:
{ f(a, empty()) -> g(a, empty())
, f(a, cons(x, k)) -> f(cons(x, a), k)
, g(empty(), d) -> d
, g(cons(x, k), d) -> g(k, cons(x, d))}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ f_0(2, 2) -> 1
, f_1(4, 2) -> 1
, empty_0() -> 1
, empty_0() -> 2
, empty_1() -> 1
, empty_1() -> 3
, g_0(2, 2) -> 1
, g_1(2, 3) -> 1
, g_1(2, 4) -> 1
, g_1(4, 3) -> 1
, g_2(2, 5) -> 1
, g_2(4, 5) -> 1
, cons_0(2, 2) -> 1
, cons_0(2, 2) -> 2
, cons_1(2, 2) -> 1
, cons_1(2, 2) -> 4
, cons_1(2, 3) -> 1
, cons_1(2, 3) -> 3
, cons_1(2, 4) -> 1
, cons_1(2, 4) -> 4
, cons_1(2, 5) -> 1
, cons_1(2, 5) -> 3
, cons_2(2, 3) -> 1
, cons_2(2, 3) -> 5
, cons_2(2, 5) -> 1
, cons_2(2, 5) -> 5}