YES

Problem:
 f(s(X)) -> f(X)
 g(cons(0(),Y)) -> g(Y)
 g(cons(s(X),Y)) -> s(X)
 h(cons(X,Y)) -> h(g(cons(X,Y)))

Proof:
 DP Processor:
  DPs:
   f#(s(X)) -> f#(X)
   g#(cons(0(),Y)) -> g#(Y)
   h#(cons(X,Y)) -> g#(cons(X,Y))
   h#(cons(X,Y)) -> h#(g(cons(X,Y)))
  TRS:
   f(s(X)) -> f(X)
   g(cons(0(),Y)) -> g(Y)
   g(cons(s(X),Y)) -> s(X)
   h(cons(X,Y)) -> h(g(cons(X,Y)))
  Usable Rule Processor:
   DPs:
    f#(s(X)) -> f#(X)
    g#(cons(0(),Y)) -> g#(Y)
    h#(cons(X,Y)) -> g#(cons(X,Y))
    h#(cons(X,Y)) -> h#(g(cons(X,Y)))
   TRS:
    g(cons(0(),Y)) -> g(Y)
    g(cons(s(X),Y)) -> s(X)
   TDG Processor:
    DPs:
     f#(s(X)) -> f#(X)
     g#(cons(0(),Y)) -> g#(Y)
     h#(cons(X,Y)) -> g#(cons(X,Y))
     h#(cons(X,Y)) -> h#(g(cons(X,Y)))
    TRS:
     g(cons(0(),Y)) -> g(Y)
     g(cons(s(X),Y)) -> s(X)
    graph:
     h#(cons(X,Y)) -> h#(g(cons(X,Y))) ->
     h#(cons(X,Y)) -> h#(g(cons(X,Y)))
     h#(cons(X,Y)) -> h#(g(cons(X,Y))) ->
     h#(cons(X,Y)) -> g#(cons(X,Y))
     h#(cons(X,Y)) -> g#(cons(X,Y)) -> g#(cons(0(),Y)) -> g#(Y)
     g#(cons(0(),Y)) -> g#(Y) -> g#(cons(0(),Y)) -> g#(Y)
     f#(s(X)) -> f#(X) -> f#(s(X)) -> f#(X)
    Restore Modifier:
     DPs:
      f#(s(X)) -> f#(X)
      g#(cons(0(),Y)) -> g#(Y)
      h#(cons(X,Y)) -> g#(cons(X,Y))
      h#(cons(X,Y)) -> h#(g(cons(X,Y)))
     TRS:
      f(s(X)) -> f(X)
      g(cons(0(),Y)) -> g(Y)
      g(cons(s(X),Y)) -> s(X)
      h(cons(X,Y)) -> h(g(cons(X,Y)))
     SCC Processor:
      #sccs: 3
      #rules: 3
      #arcs: 5/16
      DPs:
       f#(s(X)) -> f#(X)
      TRS:
       f(s(X)) -> f(X)
       g(cons(0(),Y)) -> g(Y)
       g(cons(s(X),Y)) -> s(X)
       h(cons(X,Y)) -> h(g(cons(X,Y)))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [f#](x0) = x0 + 1,
        
        [h](x0) = 0,
        
        [g](x0) = x0,
        
        [cons](x0, x1) = x0 + x1,
        
        [0] = 0,
        
        [f](x0) = 0,
        
        [s](x0) = x0 + 1
       orientation:
        f#(s(X)) = X + 2 >= X + 1 = f#(X)
        
        f(s(X)) = 0 >= 0 = f(X)
        
        g(cons(0(),Y)) = Y >= Y = g(Y)
        
        g(cons(s(X),Y)) = X + Y + 1 >= X + 1 = s(X)
        
        h(cons(X,Y)) = 0 >= 0 = h(g(cons(X,Y)))
       problem:
        DPs:
         
        TRS:
         f(s(X)) -> f(X)
         g(cons(0(),Y)) -> g(Y)
         g(cons(s(X),Y)) -> s(X)
         h(cons(X,Y)) -> h(g(cons(X,Y)))
       Qed
      
      DPs:
       h#(cons(X,Y)) -> h#(g(cons(X,Y)))
      TRS:
       f(s(X)) -> f(X)
       g(cons(0(),Y)) -> g(Y)
       g(cons(s(X),Y)) -> s(X)
       h(cons(X,Y)) -> h(g(cons(X,Y)))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [h#](x0) = x0,
        
        [h](x0) = 0,
        
        [g](x0) = 0,
        
        [cons](x0, x1) = 1,
        
        [0] = 0,
        
        [f](x0) = 0,
        
        [s](x0) = 0
       orientation:
        h#(cons(X,Y)) = 1 >= 0 = h#(g(cons(X,Y)))
        
        f(s(X)) = 0 >= 0 = f(X)
        
        g(cons(0(),Y)) = 0 >= 0 = g(Y)
        
        g(cons(s(X),Y)) = 0 >= 0 = s(X)
        
        h(cons(X,Y)) = 0 >= 0 = h(g(cons(X,Y)))
       problem:
        DPs:
         
        TRS:
         f(s(X)) -> f(X)
         g(cons(0(),Y)) -> g(Y)
         g(cons(s(X),Y)) -> s(X)
         h(cons(X,Y)) -> h(g(cons(X,Y)))
       Qed
      
      DPs:
       g#(cons(0(),Y)) -> g#(Y)
      TRS:
       f(s(X)) -> f(X)
       g(cons(0(),Y)) -> g(Y)
       g(cons(s(X),Y)) -> s(X)
       h(cons(X,Y)) -> h(g(cons(X,Y)))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [g#](x0) = x0,
        
        [h](x0) = x0,
        
        [g](x0) = 0,
        
        [cons](x0, x1) = x0 + x1 + 1,
        
        [0] = 1,
        
        [f](x0) = 0,
        
        [s](x0) = 0
       orientation:
        g#(cons(0(),Y)) = Y + 2 >= Y = g#(Y)
        
        f(s(X)) = 0 >= 0 = f(X)
        
        g(cons(0(),Y)) = 0 >= 0 = g(Y)
        
        g(cons(s(X),Y)) = 0 >= 0 = s(X)
        
        h(cons(X,Y)) = X + Y + 1 >= 0 = h(g(cons(X,Y)))
       problem:
        DPs:
         
        TRS:
         f(s(X)) -> f(X)
         g(cons(0(),Y)) -> g(Y)
         g(cons(s(X),Y)) -> s(X)
         h(cons(X,Y)) -> h(g(cons(X,Y)))
       Qed