Tool CaT
stdout:
YES(?,O(n^1))
Problem:
concat(leaf(),Y) -> Y
concat(cons(U,V),Y) -> cons(U,concat(V,Y))
lessleaves(X,leaf()) -> false()
lessleaves(leaf(),cons(W,Z)) -> true()
lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
Proof:
Bounds Processor:
bound: 2
enrichment: match
automaton:
final states: {6,5}
transitions:
lessleaves1(7,7) -> 6*
lessleaves1(7,9) -> 6*
lessleaves1(9,7) -> 6*
lessleaves1(9,9) -> 6*
concat1(3,1) -> 7*
concat1(3,3) -> 7*
concat1(3,7) -> 7*
concat1(3,9) -> 7*
concat1(4,2) -> 7*
concat1(4,4) -> 9*
concat1(1,2) -> 7*
concat1(1,4) -> 7*
concat1(2,1) -> 7*
concat1(2,3) -> 7*
concat1(2,7) -> 7*
concat1(2,9) -> 7*
concat1(3,2) -> 7*
concat1(3,4) -> 7*
concat1(4,1) -> 7*
concat1(4,3) -> 7*
concat1(4,7) -> 7*
concat1(4,9) -> 7*
concat1(1,1) -> 7*
concat1(1,3) -> 7*
concat1(1,7) -> 7*
concat1(1,9) -> 7*
concat1(2,2) -> 7*
concat1(2,4) -> 9*
true1() -> 6*
false1() -> 6*
cons1(3,7) -> 7,9,5
cons1(3,9) -> 9,5
cons1(2,7) -> 7,9,5
cons1(2,9) -> 9,5
cons1(4,7) -> 7,9,5
cons1(4,9) -> 9,5
cons1(1,7) -> 7,9,5
cons1(1,9) -> 9,5
lessleaves2(16,16) -> 6*
lessleaves2(11,16) -> 6*
lessleaves2(12,11) -> 6*
lessleaves2(16,11) -> 6*
lessleaves2(11,11) -> 6*
concat2(3,7) -> 11*
concat2(3,9) -> 12,11
concat2(2,7) -> 11*
concat2(2,9) -> 16*
concat2(4,7) -> 11*
concat2(4,9) -> 16*
concat2(1,7) -> 11*
concat2(1,9) -> 16*
concat0(3,1) -> 5*
concat0(3,3) -> 5*
concat0(4,2) -> 5*
concat0(4,4) -> 5*
concat0(1,2) -> 5*
concat0(1,4) -> 5*
concat0(2,1) -> 5*
concat0(2,3) -> 5*
concat0(3,2) -> 5*
concat0(3,4) -> 5*
concat0(4,1) -> 5*
concat0(4,3) -> 5*
concat0(1,1) -> 5*
concat0(1,3) -> 5*
concat0(2,2) -> 5*
concat0(2,4) -> 5*
leaf0() -> 1*
cons0(3,1) -> 2*
cons0(3,3) -> 2*
cons0(4,2) -> 2*
cons0(4,4) -> 2*
cons0(1,2) -> 2*
cons0(1,4) -> 2*
cons0(2,1) -> 2*
cons0(2,3) -> 2*
cons0(3,2) -> 2*
cons0(3,4) -> 2*
cons0(4,1) -> 2*
cons0(4,3) -> 2*
cons0(1,1) -> 2*
cons0(1,3) -> 2*
cons0(2,2) -> 2*
cons0(2,4) -> 2*
lessleaves0(3,1) -> 6*
lessleaves0(3,3) -> 6*
lessleaves0(4,2) -> 6*
lessleaves0(4,4) -> 6*
lessleaves0(1,2) -> 6*
lessleaves0(1,4) -> 6*
lessleaves0(2,1) -> 6*
lessleaves0(2,3) -> 6*
lessleaves0(3,2) -> 6*
lessleaves0(3,4) -> 6*
lessleaves0(4,1) -> 6*
lessleaves0(4,3) -> 6*
lessleaves0(1,1) -> 6*
lessleaves0(1,3) -> 6*
lessleaves0(2,2) -> 6*
lessleaves0(2,4) -> 6*
false0() -> 3*
true0() -> 4*
1 -> 7,5
2 -> 7,5
3 -> 7,5
4 -> 7,5
7 -> 11*
9 -> 7,16
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:
{ concat(leaf(), Y) -> Y
, concat(cons(U, V), Y) -> cons(U, concat(V, Y))
, lessleaves(X, leaf()) -> false()
, lessleaves(leaf(), cons(W, Z)) -> true()
, lessleaves(cons(U, V), cons(W, Z)) ->
lessleaves(concat(U, V), concat(W, Z))}
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:
{ concat(leaf(), Y) -> Y
, concat(cons(U, V), Y) -> cons(U, concat(V, Y))
, lessleaves(X, leaf()) -> false()
, lessleaves(leaf(), cons(W, Z)) -> true()
, lessleaves(cons(U, V), cons(W, Z)) ->
lessleaves(concat(U, V), concat(W, Z))}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ concat_0(2, 2) -> 1
, concat_1(2, 2) -> 3
, concat_1(2, 2) -> 4
, concat_1(2, 2) -> 5
, concat_1(2, 3) -> 3
, concat_1(2, 3) -> 4
, concat_1(2, 3) -> 5
, concat_2(2, 3) -> 4
, concat_2(2, 3) -> 5
, leaf_0() -> 1
, leaf_0() -> 2
, leaf_0() -> 3
, leaf_0() -> 4
, leaf_0() -> 5
, cons_0(2, 2) -> 1
, cons_0(2, 2) -> 2
, cons_0(2, 2) -> 3
, cons_0(2, 2) -> 4
, cons_0(2, 2) -> 5
, cons_1(2, 3) -> 1
, cons_1(2, 3) -> 3
, cons_1(2, 3) -> 4
, cons_1(2, 3) -> 5
, lessleaves_0(2, 2) -> 1
, lessleaves_1(3, 3) -> 1
, lessleaves_2(4, 5) -> 1
, false_0() -> 1
, false_0() -> 2
, false_0() -> 3
, false_0() -> 4
, false_0() -> 5
, false_1() -> 1
, true_0() -> 1
, true_0() -> 2
, true_0() -> 3
, true_0() -> 4
, true_0() -> 5
, true_1() -> 1}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:
{ concat(leaf(), Y) -> Y
, concat(cons(U, V), Y) -> cons(U, concat(V, Y))
, lessleaves(X, leaf()) -> false()
, lessleaves(leaf(), cons(W, Z)) -> true()
, lessleaves(cons(U, V), cons(W, Z)) ->
lessleaves(concat(U, V), concat(W, Z))}
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:
{ concat(leaf(), Y) -> Y
, concat(cons(U, V), Y) -> cons(U, concat(V, Y))
, lessleaves(X, leaf()) -> false()
, lessleaves(leaf(), cons(W, Z)) -> true()
, lessleaves(cons(U, V), cons(W, Z)) ->
lessleaves(concat(U, V), concat(W, Z))}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ concat_0(2, 2) -> 1
, concat_1(2, 2) -> 3
, concat_1(2, 2) -> 4
, concat_1(2, 2) -> 5
, concat_1(2, 3) -> 3
, concat_1(2, 3) -> 4
, concat_1(2, 3) -> 5
, concat_2(2, 3) -> 4
, concat_2(2, 3) -> 5
, leaf_0() -> 1
, leaf_0() -> 2
, leaf_0() -> 3
, leaf_0() -> 4
, leaf_0() -> 5
, cons_0(2, 2) -> 1
, cons_0(2, 2) -> 2
, cons_0(2, 2) -> 3
, cons_0(2, 2) -> 4
, cons_0(2, 2) -> 5
, cons_1(2, 3) -> 1
, cons_1(2, 3) -> 3
, cons_1(2, 3) -> 4
, cons_1(2, 3) -> 5
, lessleaves_0(2, 2) -> 1
, lessleaves_1(3, 3) -> 1
, lessleaves_2(4, 5) -> 1
, false_0() -> 1
, false_0() -> 2
, false_0() -> 3
, false_0() -> 4
, false_0() -> 5
, false_1() -> 1
, true_0() -> 1
, true_0() -> 2
, true_0() -> 3
, true_0() -> 4
, true_0() -> 5
, true_1() -> 1}