YES(?,O(n^1))

Problem:
 f(c(X,s(Y))) -> f(c(s(X),Y))
 g(c(s(X),Y)) -> f(c(X,s(Y)))

Proof:
 RT Transformation Processor:
  strict:
   f(c(X,s(Y))) -> f(c(s(X),Y))
   g(c(s(X),Y)) -> f(c(X,s(Y)))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [g](x0) = x0 + 21,
    
    [f](x0) = x0 + 20,
    
    [c](x0, x1) = x0 + x1 + 16,
    
    [s](x0) = x0 + 8
   orientation:
    f(c(X,s(Y))) = X + Y + 44 >= X + Y + 44 = f(c(s(X),Y))
    
    g(c(s(X),Y)) = X + Y + 45 >= X + Y + 44 = f(c(X,s(Y)))
   problem:
    strict:
     f(c(X,s(Y))) -> f(c(s(X),Y))
    weak:
     g(c(s(X),Y)) -> f(c(X,s(Y)))
   Bounds Processor:
    bound: 1
    enrichment: match-rt
    automaton:
     final states: {5}
     transitions:
      f1(9) -> 5*
      c1(8,5) -> 9*
      s1(5) -> 8*
      s1(8) -> 8*
      f0(5) -> 5*
      c0(5,5) -> 5*
      s0(5) -> 5*
      g0(5) -> 5*
    problem:
     strict:
      
     weak:
      f(c(X,s(Y))) -> f(c(s(X),Y))
      g(c(s(X),Y)) -> f(c(X,s(Y)))
    Qed