Problem Transformed CSR 04 Ex4 7 77 Bor03 FR

Tool CaT

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

stdout:

YES(?,O(n^1))

Problem:
zeros() -> cons(0(),n__zeros())
tail(cons(X,XS)) -> activate(XS)
zeros() -> n__zeros()
activate(n__zeros()) -> zeros()
activate(X) -> X

Proof:
Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {6,5,4}
   transitions:
    zeros1() -> 5,6
    n__zeros1() -> 4,7
    activate1(2) -> 5*
    activate1(1) -> 5*
    activate1(3) -> 5*
    cons1(8,7) -> 4*
    01() -> 8*
    n__zeros2() -> 5,6,13
    cons2(14,6) -> 5*
    cons2(14,13) -> 6*
    zeros0() -> 4*
    02() -> 14*
    cons0(3,1) -> 1*
    cons0(3,3) -> 1*
    cons0(1,2) -> 1*
    cons0(2,1) -> 1*
    cons0(2,3) -> 1*
    cons0(3,2) -> 1*
    cons0(1,1) -> 1*
    cons0(1,3) -> 1*
    cons0(2,2) -> 1*
    00() -> 2*
    n__zeros0() -> 3*
    tail0(2) -> 5*
    tail0(1) -> 5*
    tail0(3) -> 5*
    activate0(2) -> 6*
    activate0(1) -> 6*
    activate0(3) -> 6*
    1 -> 5,6
    2 -> 5,6
    3 -> 5,6
  problem:

  Qed

Tool IRC1

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

stdout:

YES(?,O(n^1))

Tool IRC2

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

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:
    {  zeros() -> cons(0(), n__zeros())
     , tail(cons(X, XS)) -> activate(XS)
     , zeros() -> n__zeros()
     , activate(n__zeros()) -> zeros()
     , activate(X) -> X}

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:
         {  zeros() -> cons(0(), n__zeros())
          , tail(cons(X, XS)) -> activate(XS)
          , zeros() -> n__zeros()
          , activate(n__zeros()) -> zeros()
          , activate(X) -> X}

     Proof Output:
       The problem is match-bounded by 2.
       The enriched problem is compatible with the following automaton:
       {  zeros_0() -> 1
        , zeros_1() -> 1
        , cons_0(2, 2) -> 1
        , cons_0(2, 2) -> 2
        , cons_1(3, 4) -> 1
        , cons_2(5, 6) -> 1
        , 0_0() -> 1
        , 0_0() -> 2
        , 0_1() -> 3
        , 0_2() -> 5
        , n__zeros_0() -> 1
        , n__zeros_0() -> 2
        , n__zeros_1() -> 1
        , n__zeros_1() -> 4
        , n__zeros_2() -> 1
        , n__zeros_2() -> 6
        , tail_0(2) -> 1
        , activate_0(2) -> 1
        , activate_1(2) -> 1}

Tool RC1

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

stdout:

YES(?,O(n^1))

Tool RC2

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

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    runtime-complexity with respect to
  Rules:
    {  zeros() -> cons(0(), n__zeros())
     , tail(cons(X, XS)) -> activate(XS)
     , zeros() -> n__zeros()
     , activate(n__zeros()) -> zeros()
     , activate(X) -> X}

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:
         {  zeros() -> cons(0(), n__zeros())
          , tail(cons(X, XS)) -> activate(XS)
          , zeros() -> n__zeros()
          , activate(n__zeros()) -> zeros()
          , activate(X) -> X}

     Proof Output:
       The problem is match-bounded by 2.
       The enriched problem is compatible with the following automaton:
       {  zeros_0() -> 1
        , zeros_1() -> 1
        , cons_0(2, 2) -> 1
        , cons_0(2, 2) -> 2
        , cons_1(3, 4) -> 1
        , cons_2(5, 6) -> 1
        , 0_0() -> 1
        , 0_0() -> 2
        , 0_1() -> 3
        , 0_2() -> 5
        , n__zeros_0() -> 1
        , n__zeros_0() -> 2
        , n__zeros_1() -> 1
        , n__zeros_1() -> 4
        , n__zeros_2() -> 1
        , n__zeros_2() -> 6
        , tail_0(2) -> 1
        , activate_0(2) -> 1
        , activate_1(2) -> 1}