YES
O(n)
TRS:
 {
  f(c(s(x), y)) -> f(c(x, s(y))),
  g(c(x, s(y))) -> g(c(s(x), y)),
     g(s(f(x))) -> g(f(x))
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
    f(c(s(x), y)) -> f(c(x, s(y))),
    g(c(x, s(y))) -> g(c(s(x), y)),
       g(s(f(x))) -> g(f(x))
   }
  BOUND:
   Automaton:
    {
        g_1(5) -> 4,
        g_1(4) -> 4,
        g_0(4) -> 4,
        s_1(7) -> 7,
        s_1(4) -> 7,
        s_0(4) -> 4,
     c_1(7, 4) -> 5,
     c_1(4, 7) -> 8,
     c_0(4, 4) -> 4,
        f_1(8) -> 5 | 4,
        f_1(4) -> 5,
        f_0(4) -> 4
    }
   Strict:
    {}
   Qed