Tool CaT
stdout:
YES(?,O(n^1))
Problem:
active(f(x)) -> mark(x)
top(active(c())) -> top(mark(c()))
top(mark(x)) -> top(check(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X()),x))
match(f(x),f(y)) -> f(match(x,y))
match(X(),x) -> proper(x)
proper(c()) -> ok(c())
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
start(ok(x)) -> found(x)
f(found(x)) -> found(f(x))
top(found(x)) -> top(active(x))
active(f(x)) -> f(active(x))
f(mark(x)) -> mark(f(x))
Proof:
Bounds Processor:
bound: 3
enrichment: match
automaton:
final states: {12,11,10,9,8,7,6}
transitions:
mark1(22) -> 13*
mark1(23) -> 23,11
f1(5) -> 23*
f1(2) -> 23*
f1(4) -> 23*
f1(1) -> 23*
f1(18) -> 19*
f1(3) -> 23*
top1(13) -> 7*
active1(5) -> 13*
active1(2) -> 13*
active1(4) -> 13*
active1(1) -> 13*
active1(3) -> 13*
found1(5) -> 12*
found1(2) -> 12*
found1(4) -> 12*
found1(1) -> 12*
found1(23) -> 23,11
found1(3) -> 12*
ok1(22) -> 9,10
ok1(23) -> 23,11
c1() -> 22*
proper1(5) -> 9*
proper1(2) -> 9*
proper1(4) -> 9*
proper1(1) -> 9*
proper1(3) -> 9*
start1(20) -> 8*
match1(19,2) -> 20*
match1(19,4) -> 20*
match1(19,1) -> 20*
match1(19,3) -> 20*
match1(19,5) -> 20*
X1() -> 18*
check1(5) -> 13*
check1(2) -> 13*
check1(4) -> 13*
check1(1) -> 13*
check1(3) -> 13*
start2(27) -> 13*
active0(5) -> 6*
active0(2) -> 6*
active0(4) -> 6*
active0(1) -> 6*
active0(3) -> 6*
match2(26,2) -> 27*
match2(26,4) -> 27*
match2(26,1) -> 27*
match2(26,3) -> 27*
match2(26,5) -> 27*
f0(5) -> 11*
f0(2) -> 11*
f0(4) -> 11*
f0(1) -> 11*
f0(3) -> 11*
f2(25) -> 26*
mark0(5) -> 1*
mark0(2) -> 1*
mark0(4) -> 1*
mark0(1) -> 1*
mark0(3) -> 1*
X2() -> 25*
top0(5) -> 7*
top0(2) -> 7*
top0(4) -> 7*
top0(1) -> 7*
top0(3) -> 7*
top2(32) -> 7*
c0() -> 2*
check2(22) -> 32*
check0(5) -> 8*
check0(2) -> 8*
check0(4) -> 8*
check0(1) -> 8*
check0(3) -> 8*
start3(35) -> 32*
start0(5) -> 12*
start0(2) -> 12*
start0(4) -> 12*
start0(1) -> 12*
start0(3) -> 12*
match3(34,22) -> 35*
match0(3,1) -> 9*
match0(3,3) -> 9*
match0(3,5) -> 9*
match0(4,2) -> 9*
match0(4,4) -> 9*
match0(5,1) -> 9*
match0(5,3) -> 9*
match0(5,5) -> 9*
match0(1,2) -> 9*
match0(1,4) -> 9*
match0(2,1) -> 9*
match0(2,3) -> 9*
match0(2,5) -> 9*
match0(3,2) -> 9*
match0(3,4) -> 9*
match0(4,1) -> 9*
match0(4,3) -> 9*
match0(4,5) -> 9*
match0(5,2) -> 9*
match0(5,4) -> 9*
match0(1,1) -> 9*
match0(1,3) -> 9*
match0(1,5) -> 9*
match0(2,2) -> 9*
match0(2,4) -> 9*
f3(33) -> 34*
X0() -> 3*
X3() -> 33*
proper0(5) -> 10*
proper0(2) -> 10*
proper0(4) -> 10*
proper0(1) -> 10*
proper0(3) -> 10*
ok0(5) -> 4*
ok0(2) -> 4*
ok0(4) -> 4*
ok0(1) -> 4*
ok0(3) -> 4*
found0(5) -> 5*
found0(2) -> 5*
found0(4) -> 5*
found0(1) -> 5*
found0(3) -> 5*
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:
{ active(f(x)) -> mark(x)
, top(active(c())) -> top(mark(c()))
, top(mark(x)) -> top(check(x))
, check(f(x)) -> f(check(x))
, check(x) -> start(match(f(X()), x))
, match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, start(ok(x)) -> found(x)
, f(found(x)) -> found(f(x))
, top(found(x)) -> top(active(x))
, active(f(x)) -> f(active(x))
, f(mark(x)) -> mark(f(x))}
Proof Output:
'Bounds with perSymbol-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with perSymbol-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with perSymbol-enrichment and initial automaton 'match''
----------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(f(x)) -> mark(x)
, top(active(c())) -> top(mark(c()))
, top(mark(x)) -> top(check(x))
, check(f(x)) -> f(check(x))
, check(x) -> start(match(f(X()), x))
, match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, start(ok(x)) -> found(x)
, f(found(x)) -> found(f(x))
, top(found(x)) -> top(active(x))
, active(f(x)) -> f(active(x))
, f(mark(x)) -> mark(f(x))}
Proof Output:
The problem is match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ active_0(3) -> 1
, active_0(5) -> 1
, active_0(9) -> 1
, active_0(11) -> 1
, active_0(12) -> 1
, active_1(3) -> 13
, active_1(5) -> 13
, active_1(9) -> 13
, active_1(11) -> 13
, active_1(12) -> 13
, f_0(3) -> 2
, f_0(5) -> 2
, f_0(9) -> 2
, f_0(11) -> 2
, f_0(12) -> 2
, f_1(3) -> 21
, f_1(5) -> 21
, f_1(9) -> 21
, f_1(11) -> 21
, f_1(12) -> 21
, f_1(16) -> 15
, f_2(19) -> 18
, f_3(25) -> 24
, mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(9) -> 3
, mark_0(11) -> 3
, mark_0(12) -> 3
, mark_1(20) -> 13
, mark_1(21) -> 2
, mark_1(21) -> 21
, top_0(3) -> 4
, top_0(5) -> 4
, top_0(9) -> 4
, top_0(11) -> 4
, top_0(12) -> 4
, top_1(13) -> 4
, top_2(22) -> 4
, c_0() -> 5
, c_1() -> 20
, check_0(3) -> 6
, check_0(5) -> 6
, check_0(9) -> 6
, check_0(11) -> 6
, check_0(12) -> 6
, check_1(3) -> 13
, check_1(5) -> 13
, check_1(9) -> 13
, check_1(11) -> 13
, check_1(12) -> 13
, check_2(20) -> 22
, start_0(3) -> 7
, start_0(5) -> 7
, start_0(9) -> 7
, start_0(11) -> 7
, start_0(12) -> 7
, start_1(14) -> 6
, start_2(17) -> 13
, start_3(23) -> 22
, match_0(3, 3) -> 8
, match_0(3, 5) -> 8
, match_0(3, 9) -> 8
, match_0(3, 11) -> 8
, match_0(3, 12) -> 8
, match_0(5, 3) -> 8
, match_0(5, 5) -> 8
, match_0(5, 9) -> 8
, match_0(5, 11) -> 8
, match_0(5, 12) -> 8
, match_0(9, 3) -> 8
, match_0(9, 5) -> 8
, match_0(9, 9) -> 8
, match_0(9, 11) -> 8
, match_0(9, 12) -> 8
, match_0(11, 3) -> 8
, match_0(11, 5) -> 8
, match_0(11, 9) -> 8
, match_0(11, 11) -> 8
, match_0(11, 12) -> 8
, match_0(12, 3) -> 8
, match_0(12, 5) -> 8
, match_0(12, 9) -> 8
, match_0(12, 11) -> 8
, match_0(12, 12) -> 8
, match_1(15, 3) -> 14
, match_1(15, 5) -> 14
, match_1(15, 9) -> 14
, match_1(15, 11) -> 14
, match_1(15, 12) -> 14
, match_2(18, 3) -> 17
, match_2(18, 5) -> 17
, match_2(18, 9) -> 17
, match_2(18, 11) -> 17
, match_2(18, 12) -> 17
, match_3(24, 20) -> 23
, X_0() -> 9
, X_1() -> 16
, X_2() -> 19
, X_3() -> 25
, proper_0(3) -> 10
, proper_0(5) -> 10
, proper_0(9) -> 10
, proper_0(11) -> 10
, proper_0(12) -> 10
, proper_1(3) -> 8
, proper_1(5) -> 8
, proper_1(9) -> 8
, proper_1(11) -> 8
, proper_1(12) -> 8
, ok_0(3) -> 11
, ok_0(5) -> 11
, ok_0(9) -> 11
, ok_0(11) -> 11
, ok_0(12) -> 11
, ok_1(20) -> 8
, ok_1(20) -> 10
, ok_1(21) -> 2
, ok_1(21) -> 21
, found_0(3) -> 12
, found_0(5) -> 12
, found_0(9) -> 12
, found_0(11) -> 12
, found_0(12) -> 12
, found_1(3) -> 7
, found_1(5) -> 7
, found_1(9) -> 7
, found_1(11) -> 7
, found_1(12) -> 7
, found_1(21) -> 2
, found_1(21) -> 21}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:
{ active(f(x)) -> mark(x)
, top(active(c())) -> top(mark(c()))
, top(mark(x)) -> top(check(x))
, check(f(x)) -> f(check(x))
, check(x) -> start(match(f(X()), x))
, match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, start(ok(x)) -> found(x)
, f(found(x)) -> found(f(x))
, top(found(x)) -> top(active(x))
, active(f(x)) -> f(active(x))
, f(mark(x)) -> mark(f(x))}
Proof Output:
'Bounds with perSymbol-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with perSymbol-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with perSymbol-enrichment and initial automaton 'match''
----------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ active(f(x)) -> mark(x)
, top(active(c())) -> top(mark(c()))
, top(mark(x)) -> top(check(x))
, check(f(x)) -> f(check(x))
, check(x) -> start(match(f(X()), x))
, match(f(x), f(y)) -> f(match(x, y))
, match(X(), x) -> proper(x)
, proper(c()) -> ok(c())
, proper(f(x)) -> f(proper(x))
, f(ok(x)) -> ok(f(x))
, start(ok(x)) -> found(x)
, f(found(x)) -> found(f(x))
, top(found(x)) -> top(active(x))
, active(f(x)) -> f(active(x))
, f(mark(x)) -> mark(f(x))}
Proof Output:
The problem is match-bounded by 3.
The enriched problem is compatible with the following automaton:
{ active_0(3) -> 1
, active_0(5) -> 1
, active_0(9) -> 1
, active_0(11) -> 1
, active_0(12) -> 1
, active_1(3) -> 13
, active_1(5) -> 13
, active_1(9) -> 13
, active_1(11) -> 13
, active_1(12) -> 13
, f_0(3) -> 2
, f_0(5) -> 2
, f_0(9) -> 2
, f_0(11) -> 2
, f_0(12) -> 2
, f_1(3) -> 21
, f_1(5) -> 21
, f_1(9) -> 21
, f_1(11) -> 21
, f_1(12) -> 21
, f_1(16) -> 15
, f_2(19) -> 18
, f_3(25) -> 24
, mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(9) -> 3
, mark_0(11) -> 3
, mark_0(12) -> 3
, mark_1(20) -> 13
, mark_1(21) -> 2
, mark_1(21) -> 21
, top_0(3) -> 4
, top_0(5) -> 4
, top_0(9) -> 4
, top_0(11) -> 4
, top_0(12) -> 4
, top_1(13) -> 4
, top_2(22) -> 4
, c_0() -> 5
, c_1() -> 20
, check_0(3) -> 6
, check_0(5) -> 6
, check_0(9) -> 6
, check_0(11) -> 6
, check_0(12) -> 6
, check_1(3) -> 13
, check_1(5) -> 13
, check_1(9) -> 13
, check_1(11) -> 13
, check_1(12) -> 13
, check_2(20) -> 22
, start_0(3) -> 7
, start_0(5) -> 7
, start_0(9) -> 7
, start_0(11) -> 7
, start_0(12) -> 7
, start_1(14) -> 6
, start_2(17) -> 13
, start_3(23) -> 22
, match_0(3, 3) -> 8
, match_0(3, 5) -> 8
, match_0(3, 9) -> 8
, match_0(3, 11) -> 8
, match_0(3, 12) -> 8
, match_0(5, 3) -> 8
, match_0(5, 5) -> 8
, match_0(5, 9) -> 8
, match_0(5, 11) -> 8
, match_0(5, 12) -> 8
, match_0(9, 3) -> 8
, match_0(9, 5) -> 8
, match_0(9, 9) -> 8
, match_0(9, 11) -> 8
, match_0(9, 12) -> 8
, match_0(11, 3) -> 8
, match_0(11, 5) -> 8
, match_0(11, 9) -> 8
, match_0(11, 11) -> 8
, match_0(11, 12) -> 8
, match_0(12, 3) -> 8
, match_0(12, 5) -> 8
, match_0(12, 9) -> 8
, match_0(12, 11) -> 8
, match_0(12, 12) -> 8
, match_1(15, 3) -> 14
, match_1(15, 5) -> 14
, match_1(15, 9) -> 14
, match_1(15, 11) -> 14
, match_1(15, 12) -> 14
, match_2(18, 3) -> 17
, match_2(18, 5) -> 17
, match_2(18, 9) -> 17
, match_2(18, 11) -> 17
, match_2(18, 12) -> 17
, match_3(24, 20) -> 23
, X_0() -> 9
, X_1() -> 16
, X_2() -> 19
, X_3() -> 25
, proper_0(3) -> 10
, proper_0(5) -> 10
, proper_0(9) -> 10
, proper_0(11) -> 10
, proper_0(12) -> 10
, proper_1(3) -> 8
, proper_1(5) -> 8
, proper_1(9) -> 8
, proper_1(11) -> 8
, proper_1(12) -> 8
, ok_0(3) -> 11
, ok_0(5) -> 11
, ok_0(9) -> 11
, ok_0(11) -> 11
, ok_0(12) -> 11
, ok_1(20) -> 8
, ok_1(20) -> 10
, ok_1(21) -> 2
, ok_1(21) -> 21
, found_0(3) -> 12
, found_0(5) -> 12
, found_0(9) -> 12
, found_0(11) -> 12
, found_0(12) -> 12
, found_1(3) -> 7
, found_1(5) -> 7
, found_1(9) -> 7
, found_1(11) -> 7
, found_1(12) -> 7
, found_1(21) -> 2
, found_1(21) -> 21}