YES(?,O(n^1))

Problem:
 rev(ls) -> r1(ls,empty())
 r1(empty(),a) -> a
 r1(cons(x,k),a) -> r1(k,cons(x,a))

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {4,3}
   transitions:
    r11(1,10) -> 4*
    r11(2,5) -> 3*
    r11(2,7) -> 4*
    r11(1,5) -> 3*
    r11(1,7) -> 4*
    r11(2,10) -> 4*
    cons1(1,2) -> 7*
    cons1(1,10) -> 7*
    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*
    empty1() -> 5*
    rev0(2) -> 3*
    rev0(1) -> 3*
    r10(1,2) -> 4*
    r10(2,1) -> 4*
    r10(1,1) -> 4*
    r10(2,2) -> 4*
    empty0() -> 1*
    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*
  problem:
   
  Qed