Problem Transformed CSR 04 Ex4 7 77 Bor03 C

Tool CaT

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex4 7 77 Bor03 C

stdout:

YES(?,O(n^1))

Problem:
active(zeros()) -> mark(cons(0(),zeros()))
active(tail(cons(X,XS))) -> mark(XS)
active(cons(X1,X2)) -> cons(active(X1),X2)
active(tail(X)) -> tail(active(X))
cons(mark(X1),X2) -> mark(cons(X1,X2))
tail(mark(X)) -> mark(tail(X))
proper(zeros()) -> ok(zeros())
proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
proper(0()) -> ok(0())
proper(tail(X)) -> tail(proper(X))
cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
tail(ok(X)) -> ok(tail(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))

Proof:
Bounds Processor:
  bound: 5
  enrichment: match
  automaton:
   final states: {9,8,7,6,5}
   transitions:
    ok3(45) -> 37*
    ok3(42) -> 36*
    ok3(41) -> 22*
    cons3(37,36) -> 35*
    cons3(28,27) -> 41*
    active3(41) -> 35*
    03() -> 45*
    zeros3() -> 42*
    ok4(48) -> 35*
    cons4(47,27) -> 35*
    cons4(45,42) -> 48*
    active4(48) -> 51*
    active4(28) -> 47*
    top4(51) -> 9*
    cons5(52,42) -> 51*
    active0(2) -> 5*
    active0(4) -> 5*
    active0(1) -> 5*
    active0(3) -> 5*
    active5(45) -> 52*
    zeros0() -> 1*
    mark0(2) -> 2*
    mark0(4) -> 2*
    mark0(1) -> 2*
    mark0(3) -> 2*
    cons0(3,1) -> 6*
    cons0(3,3) -> 6*
    cons0(4,2) -> 6*
    cons0(4,4) -> 6*
    cons0(1,2) -> 6*
    cons0(1,4) -> 6*
    cons0(2,1) -> 6*
    cons0(2,3) -> 6*
    cons0(3,2) -> 6*
    cons0(3,4) -> 6*
    cons0(4,1) -> 6*
    cons0(4,3) -> 6*
    cons0(1,1) -> 6*
    cons0(1,3) -> 6*
    cons0(2,2) -> 6*
    cons0(2,4) -> 6*
    00() -> 3*
    tail0(2) -> 7*
    tail0(4) -> 7*
    tail0(1) -> 7*
    tail0(3) -> 7*
    proper0(2) -> 8*
    proper0(4) -> 8*
    proper0(1) -> 8*
    proper0(3) -> 8*
    ok0(2) -> 4*
    ok0(4) -> 4*
    ok0(1) -> 4*
    ok0(3) -> 4*
    top0(2) -> 9*
    top0(4) -> 9*
    top0(1) -> 9*
    top0(3) -> 9*
    top1(21) -> 9*
    active1(2) -> 21*
    active1(4) -> 21*
    active1(1) -> 21*
    active1(3) -> 21*
    proper1(2) -> 21*
    proper1(4) -> 21*
    proper1(1) -> 21*
    proper1(3) -> 21*
    ok1(10) -> 21,8
    ok1(17) -> 17,6
    ok1(19) -> 19,7
    ok1(11) -> 21,8
    tail1(2) -> 19*
    tail1(4) -> 19*
    tail1(1) -> 19*
    tail1(3) -> 19*
    cons1(3,1) -> 17*
    cons1(3,3) -> 17*
    cons1(4,2) -> 17*
    cons1(4,4) -> 17*
    cons1(1,2) -> 17*
    cons1(1,4) -> 17*
    cons1(11,10) -> 12*
    cons1(2,1) -> 17*
    cons1(2,3) -> 17*
    cons1(3,2) -> 17*
    cons1(3,4) -> 17*
    cons1(4,1) -> 17*
    cons1(4,3) -> 17*
    cons1(1,1) -> 17*
    cons1(1,3) -> 17*
    cons1(2,2) -> 17*
    cons1(2,4) -> 17*
    01() -> 11*
    zeros1() -> 10*
    mark1(17) -> 17,6
    mark1(12) -> 21,5
    mark1(19) -> 19,7
    top2(22) -> 9*
    active2(10) -> 22*
    active2(11) -> 22*
    proper2(10) -> 30*
    proper2(12) -> 22*
    proper2(11) -> 31*
    cons2(28,27) -> 29*
    cons2(31,30) -> 22*
    mark2(29) -> 22*
    02() -> 28*
    zeros2() -> 27*
    top3(35) -> 9*
    proper3(27) -> 36*
    proper3(29) -> 35*
    proper3(28) -> 37*
    ok2(27) -> 30*
    ok2(28) -> 31*
  problem:

  Qed

Tool IRC1

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex4 7 77 Bor03 C

stdout:

YES(?,O(n^1))

Tool IRC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex4 7 77 Bor03 C

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(zeros()) -> mark(cons(0(), zeros()))
     , active(tail(cons(X, XS))) -> mark(XS)
     , active(cons(X1, X2)) -> cons(active(X1), X2)
     , active(tail(X)) -> tail(active(X))
     , cons(mark(X1), X2) -> mark(cons(X1, X2))
     , tail(mark(X)) -> mark(tail(X))
     , proper(zeros()) -> ok(zeros())
     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
     , proper(0()) -> ok(0())
     , proper(tail(X)) -> tail(proper(X))
     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
     , tail(ok(X)) -> ok(tail(X))
     , top(mark(X)) -> top(proper(X))
     , top(ok(X)) -> top(active(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(zeros()) -> mark(cons(0(), zeros()))
          , active(tail(cons(X, XS))) -> mark(XS)
          , active(cons(X1, X2)) -> cons(active(X1), X2)
          , active(tail(X)) -> tail(active(X))
          , cons(mark(X1), X2) -> mark(cons(X1, X2))
          , tail(mark(X)) -> mark(tail(X))
          , proper(zeros()) -> ok(zeros())
          , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
          , proper(0()) -> ok(0())
          , proper(tail(X)) -> tail(proper(X))
          , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
          , tail(ok(X)) -> ok(tail(X))
          , top(mark(X)) -> top(proper(X))
          , top(ok(X)) -> top(active(X))}

     Proof Output:
       The problem is match-bounded by 5.
       The enriched problem is compatible with the following automaton:
       {  active_0(2) -> 1
        , active_0(3) -> 1
        , active_0(5) -> 1
        , active_0(8) -> 1
        , active_1(2) -> 15
        , active_1(3) -> 15
        , active_1(5) -> 15
        , active_1(8) -> 15
        , active_2(11) -> 16
        , active_2(12) -> 16
        , active_3(26) -> 22
        , active_4(18) -> 27
        , active_4(29) -> 30
        , active_5(25) -> 31
        , zeros_0() -> 2
        , zeros_1() -> 12
        , zeros_2() -> 19
        , zeros_3() -> 28
        , mark_0(2) -> 3
        , mark_0(3) -> 3
        , mark_0(5) -> 3
        , mark_0(8) -> 3
        , mark_1(10) -> 1
        , mark_1(10) -> 15
        , mark_1(13) -> 4
        , mark_1(13) -> 13
        , mark_1(14) -> 6
        , mark_1(14) -> 14
        , mark_2(17) -> 16
        , cons_0(2, 2) -> 4
        , cons_0(2, 3) -> 4
        , cons_0(2, 5) -> 4
        , cons_0(2, 8) -> 4
        , cons_0(3, 2) -> 4
        , cons_0(3, 3) -> 4
        , cons_0(3, 5) -> 4
        , cons_0(3, 8) -> 4
        , cons_0(5, 2) -> 4
        , cons_0(5, 3) -> 4
        , cons_0(5, 5) -> 4
        , cons_0(5, 8) -> 4
        , cons_0(8, 2) -> 4
        , cons_0(8, 3) -> 4
        , cons_0(8, 5) -> 4
        , cons_0(8, 8) -> 4
        , cons_1(2, 2) -> 13
        , cons_1(2, 3) -> 13
        , cons_1(2, 5) -> 13
        , cons_1(2, 8) -> 13
        , cons_1(3, 2) -> 13
        , cons_1(3, 3) -> 13
        , cons_1(3, 5) -> 13
        , cons_1(3, 8) -> 13
        , cons_1(5, 2) -> 13
        , cons_1(5, 3) -> 13
        , cons_1(5, 5) -> 13
        , cons_1(5, 8) -> 13
        , cons_1(8, 2) -> 13
        , cons_1(8, 3) -> 13
        , cons_1(8, 5) -> 13
        , cons_1(8, 8) -> 13
        , cons_1(11, 12) -> 10
        , cons_2(18, 19) -> 17
        , cons_2(20, 21) -> 16
        , cons_3(18, 19) -> 26
        , cons_3(23, 24) -> 22
        , cons_4(25, 28) -> 29
        , cons_4(27, 19) -> 22
        , cons_5(31, 28) -> 30
        , 0_0() -> 5
        , 0_1() -> 11
        , 0_2() -> 18
        , 0_3() -> 25
        , tail_0(2) -> 6
        , tail_0(3) -> 6
        , tail_0(5) -> 6
        , tail_0(8) -> 6
        , tail_1(2) -> 14
        , tail_1(3) -> 14
        , tail_1(5) -> 14
        , tail_1(8) -> 14
        , proper_0(2) -> 7
        , proper_0(3) -> 7
        , proper_0(5) -> 7
        , proper_0(8) -> 7
        , proper_1(2) -> 15
        , proper_1(3) -> 15
        , proper_1(5) -> 15
        , proper_1(8) -> 15
        , proper_2(10) -> 16
        , proper_2(11) -> 20
        , proper_2(12) -> 21
        , proper_3(17) -> 22
        , proper_3(18) -> 23
        , proper_3(19) -> 24
        , ok_0(2) -> 8
        , ok_0(3) -> 8
        , ok_0(5) -> 8
        , ok_0(8) -> 8
        , ok_1(11) -> 7
        , ok_1(11) -> 15
        , ok_1(12) -> 7
        , ok_1(12) -> 15
        , ok_1(13) -> 4
        , ok_1(13) -> 13
        , ok_1(14) -> 6
        , ok_1(14) -> 14
        , ok_2(18) -> 20
        , ok_2(19) -> 21
        , ok_3(25) -> 23
        , ok_3(26) -> 16
        , ok_3(28) -> 24
        , ok_4(29) -> 22
        , top_0(2) -> 9
        , top_0(3) -> 9
        , top_0(5) -> 9
        , top_0(8) -> 9
        , top_1(15) -> 9
        , top_2(16) -> 9
        , top_3(22) -> 9
        , top_4(30) -> 9}

Tool RC1

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex4 7 77 Bor03 C

stdout:

YES(?,O(n^1))

Tool RC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex4 7 77 Bor03 C

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(zeros()) -> mark(cons(0(), zeros()))
     , active(tail(cons(X, XS))) -> mark(XS)
     , active(cons(X1, X2)) -> cons(active(X1), X2)
     , active(tail(X)) -> tail(active(X))
     , cons(mark(X1), X2) -> mark(cons(X1, X2))
     , tail(mark(X)) -> mark(tail(X))
     , proper(zeros()) -> ok(zeros())
     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
     , proper(0()) -> ok(0())
     , proper(tail(X)) -> tail(proper(X))
     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
     , tail(ok(X)) -> ok(tail(X))
     , top(mark(X)) -> top(proper(X))
     , top(ok(X)) -> top(active(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(zeros()) -> mark(cons(0(), zeros()))
          , active(tail(cons(X, XS))) -> mark(XS)
          , active(cons(X1, X2)) -> cons(active(X1), X2)
          , active(tail(X)) -> tail(active(X))
          , cons(mark(X1), X2) -> mark(cons(X1, X2))
          , tail(mark(X)) -> mark(tail(X))
          , proper(zeros()) -> ok(zeros())
          , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
          , proper(0()) -> ok(0())
          , proper(tail(X)) -> tail(proper(X))
          , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
          , tail(ok(X)) -> ok(tail(X))
          , top(mark(X)) -> top(proper(X))
          , top(ok(X)) -> top(active(X))}

     Proof Output:
       The problem is match-bounded by 5.
       The enriched problem is compatible with the following automaton:
       {  active_0(2) -> 1
        , active_0(3) -> 1
        , active_0(5) -> 1
        , active_0(8) -> 1
        , active_1(2) -> 15
        , active_1(3) -> 15
        , active_1(5) -> 15
        , active_1(8) -> 15
        , active_2(11) -> 16
        , active_2(12) -> 16
        , active_3(26) -> 22
        , active_4(18) -> 27
        , active_4(29) -> 30
        , active_5(25) -> 31
        , zeros_0() -> 2
        , zeros_1() -> 12
        , zeros_2() -> 19
        , zeros_3() -> 28
        , mark_0(2) -> 3
        , mark_0(3) -> 3
        , mark_0(5) -> 3
        , mark_0(8) -> 3
        , mark_1(10) -> 1
        , mark_1(10) -> 15
        , mark_1(13) -> 4
        , mark_1(13) -> 13
        , mark_1(14) -> 6
        , mark_1(14) -> 14
        , mark_2(17) -> 16
        , cons_0(2, 2) -> 4
        , cons_0(2, 3) -> 4
        , cons_0(2, 5) -> 4
        , cons_0(2, 8) -> 4
        , cons_0(3, 2) -> 4
        , cons_0(3, 3) -> 4
        , cons_0(3, 5) -> 4
        , cons_0(3, 8) -> 4
        , cons_0(5, 2) -> 4
        , cons_0(5, 3) -> 4
        , cons_0(5, 5) -> 4
        , cons_0(5, 8) -> 4
        , cons_0(8, 2) -> 4
        , cons_0(8, 3) -> 4
        , cons_0(8, 5) -> 4
        , cons_0(8, 8) -> 4
        , cons_1(2, 2) -> 13
        , cons_1(2, 3) -> 13
        , cons_1(2, 5) -> 13
        , cons_1(2, 8) -> 13
        , cons_1(3, 2) -> 13
        , cons_1(3, 3) -> 13
        , cons_1(3, 5) -> 13
        , cons_1(3, 8) -> 13
        , cons_1(5, 2) -> 13
        , cons_1(5, 3) -> 13
        , cons_1(5, 5) -> 13
        , cons_1(5, 8) -> 13
        , cons_1(8, 2) -> 13
        , cons_1(8, 3) -> 13
        , cons_1(8, 5) -> 13
        , cons_1(8, 8) -> 13
        , cons_1(11, 12) -> 10
        , cons_2(18, 19) -> 17
        , cons_2(20, 21) -> 16
        , cons_3(18, 19) -> 26
        , cons_3(23, 24) -> 22
        , cons_4(25, 28) -> 29
        , cons_4(27, 19) -> 22
        , cons_5(31, 28) -> 30
        , 0_0() -> 5
        , 0_1() -> 11
        , 0_2() -> 18
        , 0_3() -> 25
        , tail_0(2) -> 6
        , tail_0(3) -> 6
        , tail_0(5) -> 6
        , tail_0(8) -> 6
        , tail_1(2) -> 14
        , tail_1(3) -> 14
        , tail_1(5) -> 14
        , tail_1(8) -> 14
        , proper_0(2) -> 7
        , proper_0(3) -> 7
        , proper_0(5) -> 7
        , proper_0(8) -> 7
        , proper_1(2) -> 15
        , proper_1(3) -> 15
        , proper_1(5) -> 15
        , proper_1(8) -> 15
        , proper_2(10) -> 16
        , proper_2(11) -> 20
        , proper_2(12) -> 21
        , proper_3(17) -> 22
        , proper_3(18) -> 23
        , proper_3(19) -> 24
        , ok_0(2) -> 8
        , ok_0(3) -> 8
        , ok_0(5) -> 8
        , ok_0(8) -> 8
        , ok_1(11) -> 7
        , ok_1(11) -> 15
        , ok_1(12) -> 7
        , ok_1(12) -> 15
        , ok_1(13) -> 4
        , ok_1(13) -> 13
        , ok_1(14) -> 6
        , ok_1(14) -> 14
        , ok_2(18) -> 20
        , ok_2(19) -> 21
        , ok_3(25) -> 23
        , ok_3(26) -> 16
        , ok_3(28) -> 24
        , ok_4(29) -> 22
        , top_0(2) -> 9
        , top_0(3) -> 9
        , top_0(5) -> 9
        , top_0(8) -> 9
        , top_1(15) -> 9
        , top_2(16) -> 9
        , top_3(22) -> 9
        , top_4(30) -> 9}