YES

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

Proof:
 DP Processor:
  DPs:
   f#(s(x)) -> id_inc#(c(x,x))
   f#(s(x)) -> f#(id_inc(c(x,x)))
   f#(c(s(x),y)) -> g#(c(x,y))
   g#(c(s(x),y)) -> g#(c(y,x))
   g#(c(x,s(y))) -> g#(c(y,x))
   g#(c(x,x)) -> f#(x)
   id_inc#(c(x,y)) -> id_inc#(y)
   id_inc#(c(x,y)) -> id_inc#(x)
   id_inc#(s(x)) -> id_inc#(x)
  TRS:
   f(s(x)) -> f(id_inc(c(x,x)))
   f(c(s(x),y)) -> g(c(x,y))
   g(c(s(x),y)) -> g(c(y,x))
   g(c(x,s(y))) -> g(c(y,x))
   g(c(x,x)) -> f(x)
   id_inc(c(x,y)) -> c(id_inc(x),id_inc(y))
   id_inc(s(x)) -> s(id_inc(x))
   id_inc(0()) -> 0()
   id_inc(0()) -> s(0())
  TDG Processor:
   DPs:
    f#(s(x)) -> id_inc#(c(x,x))
    f#(s(x)) -> f#(id_inc(c(x,x)))
    f#(c(s(x),y)) -> g#(c(x,y))
    g#(c(s(x),y)) -> g#(c(y,x))
    g#(c(x,s(y))) -> g#(c(y,x))
    g#(c(x,x)) -> f#(x)
    id_inc#(c(x,y)) -> id_inc#(y)
    id_inc#(c(x,y)) -> id_inc#(x)
    id_inc#(s(x)) -> id_inc#(x)
   TRS:
    f(s(x)) -> f(id_inc(c(x,x)))
    f(c(s(x),y)) -> g(c(x,y))
    g(c(s(x),y)) -> g(c(y,x))
    g(c(x,s(y))) -> g(c(y,x))
    g(c(x,x)) -> f(x)
    id_inc(c(x,y)) -> c(id_inc(x),id_inc(y))
    id_inc(s(x)) -> s(id_inc(x))
    id_inc(0()) -> 0()
    id_inc(0()) -> s(0())
   graph:
    g#(c(s(x),y)) -> g#(c(y,x)) -> g#(c(x,x)) -> f#(x)
    g#(c(s(x),y)) -> g#(c(y,x)) -> g#(c(x,s(y))) -> g#(c(y,x))
    g#(c(s(x),y)) -> g#(c(y,x)) -> g#(c(s(x),y)) -> g#(c(y,x))
    g#(c(x,s(y))) -> g#(c(y,x)) -> g#(c(x,x)) -> f#(x)
    g#(c(x,s(y))) -> g#(c(y,x)) -> g#(c(x,s(y))) -> g#(c(y,x))
    g#(c(x,s(y))) -> g#(c(y,x)) -> g#(c(s(x),y)) -> g#(c(y,x))
    g#(c(x,x)) -> f#(x) -> f#(c(s(x),y)) -> g#(c(x,y))
    g#(c(x,x)) -> f#(x) -> f#(s(x)) -> f#(id_inc(c(x,x)))
    g#(c(x,x)) -> f#(x) -> f#(s(x)) -> id_inc#(c(x,x))
    id_inc#(c(x,y)) -> id_inc#(y) -> id_inc#(s(x)) -> id_inc#(x)
    id_inc#(c(x,y)) -> id_inc#(y) -> id_inc#(c(x,y)) -> id_inc#(x)
    id_inc#(c(x,y)) -> id_inc#(y) -> id_inc#(c(x,y)) -> id_inc#(y)
    id_inc#(c(x,y)) -> id_inc#(x) -> id_inc#(s(x)) -> id_inc#(x)
    id_inc#(c(x,y)) -> id_inc#(x) -> id_inc#(c(x,y)) -> id_inc#(x)
    id_inc#(c(x,y)) -> id_inc#(x) -> id_inc#(c(x,y)) -> id_inc#(y)
    id_inc#(s(x)) -> id_inc#(x) -> id_inc#(s(x)) -> id_inc#(x)
    id_inc#(s(x)) -> id_inc#(x) -> id_inc#(c(x,y)) -> id_inc#(x)
    id_inc#(s(x)) -> id_inc#(x) -> id_inc#(c(x,y)) -> id_inc#(y)
    f#(c(s(x),y)) -> g#(c(x,y)) -> g#(c(x,x)) -> f#(x)
    f#(c(s(x),y)) -> g#(c(x,y)) -> g#(c(x,s(y))) -> g#(c(y,x))
    f#(c(s(x),y)) -> g#(c(x,y)) -> g#(c(s(x),y)) -> g#(c(y,x))
    f#(s(x)) -> id_inc#(c(x,x)) -> id_inc#(s(x)) -> id_inc#(x)
    f#(s(x)) -> id_inc#(c(x,x)) -> id_inc#(c(x,y)) -> id_inc#(x)
    f#(s(x)) -> id_inc#(c(x,x)) -> id_inc#(c(x,y)) -> id_inc#(y)
    f#(s(x)) -> f#(id_inc(c(x,x))) -> f#(c(s(x),y)) -> g#(c(x,y))
    f#(s(x)) -> f#(id_inc(c(x,x))) -> f#(s(x)) -> f#(id_inc(c(x,x)))
    f#(s(x)) -> f#(id_inc(c(x,x))) -> f#(s(x)) -> id_inc#(c(x,x))
   SCC Processor:
    #sccs: 2
    #rules: 8
    #arcs: 27/81
    DPs:
     g#(c(s(x),y)) -> g#(c(y,x))
     g#(c(x,s(y))) -> g#(c(y,x))
     g#(c(x,x)) -> f#(x)
     f#(s(x)) -> f#(id_inc(c(x,x)))
     f#(c(s(x),y)) -> g#(c(x,y))
    TRS:
     f(s(x)) -> f(id_inc(c(x,x)))
     f(c(s(x),y)) -> g(c(x,y))
     g(c(s(x),y)) -> g(c(y,x))
     g(c(x,s(y))) -> g(c(y,x))
     g(c(x,x)) -> f(x)
     id_inc(c(x,y)) -> c(id_inc(x),id_inc(y))
     id_inc(s(x)) -> s(id_inc(x))
     id_inc(0()) -> 0()
     id_inc(0()) -> s(0())
    CDG Processor:
     DPs:
      g#(c(s(x),y)) -> g#(c(y,x))
      g#(c(x,s(y))) -> g#(c(y,x))
      g#(c(x,x)) -> f#(x)
      f#(s(x)) -> f#(id_inc(c(x,x)))
      f#(c(s(x),y)) -> g#(c(x,y))
     TRS:
      f(s(x)) -> f(id_inc(c(x,x)))
      f(c(s(x),y)) -> g(c(x,y))
      g(c(s(x),y)) -> g(c(y,x))
      g(c(x,s(y))) -> g(c(y,x))
      g(c(x,x)) -> f(x)
      id_inc(c(x,y)) -> c(id_inc(x),id_inc(y))
      id_inc(s(x)) -> s(id_inc(x))
      id_inc(0()) -> 0()
      id_inc(0()) -> s(0())
     graph:
      g#(c(s(x),y)) -> g#(c(y,x)) -> g#(c(s(x),y)) -> g#(c(y,x))
      g#(c(s(x),y)) -> g#(c(y,x)) -> g#(c(x,s(y))) -> g#(c(y,x))
      g#(c(s(x),y)) -> g#(c(y,x)) -> g#(c(x,x)) -> f#(x)
      g#(c(x,s(y))) -> g#(c(y,x)) -> g#(c(s(x),y)) -> g#(c(y,x))
      g#(c(x,s(y))) -> g#(c(y,x)) -> g#(c(x,s(y))) -> g#(c(y,x))
      g#(c(x,s(y))) -> g#(c(y,x)) -> g#(c(x,x)) -> f#(x)
      g#(c(x,x)) -> f#(x) -> f#(s(x)) -> f#(id_inc(c(x,x)))
      g#(c(x,x)) -> f#(x) -> f#(c(s(x),y)) -> g#(c(x,y))
      f#(c(s(x),y)) -> g#(c(x,y)) -> g#(c(s(x),y)) -> g#(c(y,x))
      f#(c(s(x),y)) -> g#(c(x,y)) -> g#(c(x,s(y))) -> g#(c(y,x))
      f#(c(s(x),y)) -> g#(c(x,y)) -> g#(c(x,x)) -> f#(x)
      f#(s(x)) -> f#(id_inc(c(x,x))) -> f#(c(s(x),y)) -> g#(c(x,y))
     Usable Rule Processor:
      DPs:
       g#(c(s(x),y)) -> g#(c(y,x))
       g#(c(x,s(y))) -> g#(c(y,x))
       g#(c(x,x)) -> f#(x)
       f#(s(x)) -> f#(id_inc(c(x,x)))
       f#(c(s(x),y)) -> g#(c(x,y))
      TRS:
       id_inc(c(x,y)) -> c(id_inc(x),id_inc(y))
       id_inc(s(x)) -> s(id_inc(x))
       id_inc(0()) -> 0()
       id_inc(0()) -> s(0())
      Matrix Interpretation Processor: dim=1
       
       usable rules:
        id_inc(c(x,y)) -> c(id_inc(x),id_inc(y))
        id_inc(s(x)) -> s(id_inc(x))
        id_inc(0()) -> 0()
        id_inc(0()) -> s(0())
       interpretation:
        [g#](x0) = 2x0,
        
        [f#](x0) = 2x0,
        
        [0] = 0,
        
        [id_inc](x0) = 2x0 + 1,
        
        [c](x0, x1) = 1/2x0 + 1/2x1,
        
        [s](x0) = 2x0 + 1
       orientation:
        g#(c(s(x),y)) = 2x + y + 1 >= x + y = g#(c(y,x))
        
        g#(c(x,s(y))) = x + 2y + 1 >= x + y = g#(c(y,x))
        
        g#(c(x,x)) = 2x >= 2x = f#(x)
        
        f#(s(x)) = 4x + 2 >= 4x + 2 = f#(id_inc(c(x,x)))
        
        f#(c(s(x),y)) = 2x + y + 1 >= x + y = g#(c(x,y))
        
        id_inc(c(x,y)) = x + y + 1 >= x + y + 1 = c(id_inc(x),id_inc(y))
        
        id_inc(s(x)) = 4x + 3 >= 4x + 3 = s(id_inc(x))
        
        id_inc(0()) = 1 >= 0 = 0()
        
        id_inc(0()) = 1 >= 1 = s(0())
       problem:
        DPs:
         g#(c(x,x)) -> f#(x)
         f#(s(x)) -> f#(id_inc(c(x,x)))
        TRS:
         id_inc(c(x,y)) -> c(id_inc(x),id_inc(y))
         id_inc(s(x)) -> s(id_inc(x))
         id_inc(0()) -> 0()
         id_inc(0()) -> s(0())
       Restore Modifier:
        DPs:
         g#(c(x,x)) -> f#(x)
         f#(s(x)) -> f#(id_inc(c(x,x)))
        TRS:
         f(s(x)) -> f(id_inc(c(x,x)))
         f(c(s(x),y)) -> g(c(x,y))
         g(c(s(x),y)) -> g(c(y,x))
         g(c(x,s(y))) -> g(c(y,x))
         g(c(x,x)) -> f(x)
         id_inc(c(x,y)) -> c(id_inc(x),id_inc(y))
         id_inc(s(x)) -> s(id_inc(x))
         id_inc(0()) -> 0()
         id_inc(0()) -> s(0())
        SCC Processor:
         #sccs: 0
         #rules: 0
         #arcs: 12/4
         
    
    DPs:
     id_inc#(c(x,y)) -> id_inc#(y)
     id_inc#(c(x,y)) -> id_inc#(x)
     id_inc#(s(x)) -> id_inc#(x)
    TRS:
     f(s(x)) -> f(id_inc(c(x,x)))
     f(c(s(x),y)) -> g(c(x,y))
     g(c(s(x),y)) -> g(c(y,x))
     g(c(x,s(y))) -> g(c(y,x))
     g(c(x,x)) -> f(x)
     id_inc(c(x,y)) -> c(id_inc(x),id_inc(y))
     id_inc(s(x)) -> s(id_inc(x))
     id_inc(0()) -> 0()
     id_inc(0()) -> s(0())
    Subterm Criterion Processor:
     simple projection:
      pi(id_inc#) = 0
     problem:
      DPs:
       
      TRS:
       f(s(x)) -> f(id_inc(c(x,x)))
       f(c(s(x),y)) -> g(c(x,y))
       g(c(s(x),y)) -> g(c(y,x))
       g(c(x,s(y))) -> g(c(y,x))
       g(c(x,x)) -> f(x)
       id_inc(c(x,y)) -> c(id_inc(x),id_inc(y))
       id_inc(s(x)) -> s(id_inc(x))
       id_inc(0()) -> 0()
       id_inc(0()) -> s(0())
     Qed