YES(?,O(n^1))

Problem:
 f(x,x) -> f(a(),b())
 b() -> c()

Proof:
 RT Transformation Processor:
  strict:
   f(x,x) -> f(a(),b())
   b() -> c()
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [c] = 0,
    
    [b] = 13,
    
    [a] = 16,
    
    [f](x0, x1) = x0 + x1 + 20
   orientation:
    f(x,x) = 2x + 20 >= 49 = f(a(),b())
    
    b() = 13 >= 0 = c()
   problem:
    strict:
     f(x,x) -> f(a(),b())
    weak:
     b() -> c()
   Bounds Processor:
    bound: 1
    enrichment: match-rt
    automaton:
     final states: {13,9,8,5}
     transitions:
      f0(13,5) -> 5*
      f0(8,5) -> 5*
      f0(13,9) -> 5*
      f0(8,9) -> 5*
      f0(13,13) -> 5*
      f0(8,13) -> 5*
      f0(9,8) -> 5*
      f0(5,5) -> 5*
      f0(5,9) -> 5*
      f0(5,13) -> 5*
      f0(13,8) -> 5*
      f0(8,8) -> 5*
      f0(9,5) -> 5*
      f0(9,9) -> 5*
      f0(9,13) -> 5*
      f0(5,8) -> 5*
      a0() -> 5*
      b0() -> 5*
      c0() -> 5*
      f1(8,9) -> 5*
      f1(8,13) -> 5*
      f1(7,9) -> 5*
      f1(7,13) -> 5*
      f1(8,6) -> 5*
      f1(7,6) -> 5*
      a1() -> 8*,5,7
      b1() -> 9*,5,6
      c1() -> 13*,5,10
      10 -> 9*
    problem:
     strict:
      
     weak:
      f(x,x) -> f(a(),b())
      b() -> c()
    Qed