YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {3}
   transitions:
    cons1(1,6) -> 5,3
    cons1(2,5) -> 5,3
    cons1(1,5) -> 5,3
    cons1(2,6) -> 5,3
    app1(1,2) -> 6*
    app1(2,1) -> 5*
    app1(1,1) -> 5*
    app1(2,2) -> 5*
    nil1() -> 6,5,3
    app0(1,2) -> 3*
    app0(2,1) -> 3*
    app0(1,1) -> 3*
    app0(2,2) -> 3*
    nil0() -> 1*
    cons0(1,2) -> 2*
    cons0(2,1) -> 2*
    cons0(1,1) -> 2*
    cons0(2,2) -> 2*
  problem:
   
  Qed