YES(?,O(n^1))

Problem:
 rev(xs) -> revtl(xs,nil())
 revtl(nil(),ys) -> ys
 revtl(cons(x,xs),ys) -> revtl(xs,cons(x,ys))

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {4,3}
   transitions:
    revtl1(1,10) -> 4*
    revtl1(2,5) -> 3*
    revtl1(2,7) -> 4*
    revtl1(1,5) -> 3*
    revtl1(1,7) -> 4*
    revtl1(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*
    nil1() -> 5*
    rev0(2) -> 3*
    rev0(1) -> 3*
    revtl0(1,2) -> 4*
    revtl0(2,1) -> 4*
    revtl0(1,1) -> 4*
    revtl0(2,2) -> 4*
    nil0() -> 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