YES(?,O(n^1))

Problem:
 f(c(s(x),y)) -> f(c(x,s(y)))
 g(c(x,s(y))) -> g(c(s(x),y))

Proof:
 RT Transformation Processor:
  strict:
   f(c(s(x),y)) -> f(c(x,s(y)))
   g(c(x,s(y))) -> g(c(s(x),y))
  weak:
   
  Bounds Processor:
   bound: 1
   enrichment: match-rt
   automaton:
    final states: {5}
    transitions:
     c1(12,5) -> 13*
     s1(5) -> 12*
     s1(12) -> 12*
     g1(13) -> 5*
     f0(5) -> 5*
     c0(5,5) -> 5*
     s0(5) -> 5*
     g0(5) -> 5*
   problem:
    strict:
     f(c(s(x),y)) -> f(c(x,s(y)))
    weak:
     g(c(x,s(y))) -> g(c(s(x),y))
   Bounds Processor:
    bound: 1
    enrichment: match-rt
    automaton:
     final states: {5}
     transitions:
      f1(9) -> 5*
      c1(5,8) -> 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(s(x),y)) -> f(c(x,s(y)))
      g(c(x,s(y))) -> g(c(s(x),y))
    Qed