YES(?,O(n^1))

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

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {6}
   transitions:
    f1(11) -> 12,6
    f1(6) -> 12*
    d1(12) -> 11*
    c1(9,6) -> 10*
    c1(9,9) -> 10*
    c1(6,9) -> 11*
    s1(9) -> 9*
    s1(6) -> 9*
    g1(10) -> 6*
    f2(14) -> 12*
    f2(11) -> 13*
    g0(6) -> 6*
    d2(13) -> 14*
    c0(6,6) -> 6*
    g2(17) -> 6,12
    s0(6) -> 6*
    c2(16,6) -> 17*
    c2(16,9) -> 17*
    f0(6) -> 6*
    s2(9) -> 16*
    s2(16) -> 16*
    d0(6) -> 6*
    6 -> 12*
    11 -> 13,6
    14 -> 12*
  problem:
   
  Qed