YES(?,O(n^1))

Problem:
 app(app(apply(),f),x) -> app(f,x)

Proof:
 RT Transformation Processor:
  strict:
   app(app(apply(),f),x) -> app(f,x)
  weak:
   
  Bounds Processor:
   bound: 1
   enrichment: match-rt
   automaton:
    final states: {4,3}
    transitions:
     app1(3,3) -> 3*
     app1(4,4) -> 3*
     app1(3,4) -> 3*
     app1(4,3) -> 3*
     app0(3,3) -> 3*
     app0(4,4) -> 3*
     app0(3,4) -> 3*
     app0(4,3) -> 3*
     apply0() -> 4*
   problem:
    strict:
     
    weak:
     app(app(apply(),f),x) -> app(f,x)
   Qed