YES

Problem:
 f(0(),n) -> g(0(),n)
 f(m,0()) -> g(m,0())
 f(s(m),s(n)) -> h(m,n,f(m,p(m,n)),f(s(m),n))
 g(n,m) -> bot()
 p(m,n) -> bot()
 h(k,l,m,n) -> bot()

Proof:
 DP Processor:
  DPs:
   f#(0(),n) -> g#(0(),n)
   f#(m,0()) -> g#(m,0())
   f#(s(m),s(n)) -> f#(s(m),n)
   f#(s(m),s(n)) -> p#(m,n)
   f#(s(m),s(n)) -> f#(m,p(m,n))
   f#(s(m),s(n)) -> h#(m,n,f(m,p(m,n)),f(s(m),n))
  TRS:
   f(0(),n) -> g(0(),n)
   f(m,0()) -> g(m,0())
   f(s(m),s(n)) -> h(m,n,f(m,p(m,n)),f(s(m),n))
   g(n,m) -> bot()
   p(m,n) -> bot()
   h(k,l,m,n) -> bot()
  TDG Processor:
   DPs:
    f#(0(),n) -> g#(0(),n)
    f#(m,0()) -> g#(m,0())
    f#(s(m),s(n)) -> f#(s(m),n)
    f#(s(m),s(n)) -> p#(m,n)
    f#(s(m),s(n)) -> f#(m,p(m,n))
    f#(s(m),s(n)) -> h#(m,n,f(m,p(m,n)),f(s(m),n))
   TRS:
    f(0(),n) -> g(0(),n)
    f(m,0()) -> g(m,0())
    f(s(m),s(n)) -> h(m,n,f(m,p(m,n)),f(s(m),n))
    g(n,m) -> bot()
    p(m,n) -> bot()
    h(k,l,m,n) -> bot()
   graph:
    f#(s(m),s(n)) -> f#(s(m),n) ->
    f#(s(m),s(n)) -> h#(m,n,f(m,p(m,n)),f(s(m),n))
    f#(s(m),s(n)) -> f#(s(m),n) -> f#(s(m),s(n)) -> f#(m,p(m,n))
    f#(s(m),s(n)) -> f#(s(m),n) -> f#(s(m),s(n)) -> p#(m,n)
    f#(s(m),s(n)) -> f#(s(m),n) -> f#(s(m),s(n)) -> f#(s(m),n)
    f#(s(m),s(n)) -> f#(s(m),n) -> f#(m,0()) -> g#(m,0())
    f#(s(m),s(n)) -> f#(s(m),n) -> f#(0(),n) -> g#(0(),n)
    f#(s(m),s(n)) -> f#(m,p(m,n)) ->
    f#(s(m),s(n)) -> h#(m,n,f(m,p(m,n)),f(s(m),n))
    f#(s(m),s(n)) -> f#(m,p(m,n)) -> f#(s(m),s(n)) -> f#(m,p(m,n))
    f#(s(m),s(n)) -> f#(m,p(m,n)) -> f#(s(m),s(n)) -> p#(m,n)
    f#(s(m),s(n)) -> f#(m,p(m,n)) -> f#(s(m),s(n)) -> f#(s(m),n)
    f#(s(m),s(n)) -> f#(m,p(m,n)) -> f#(m,0()) -> g#(m,0())
    f#(s(m),s(n)) -> f#(m,p(m,n)) -> f#(0(),n) -> g#(0(),n)
   EDG Processor:
    DPs:
     f#(0(),n) -> g#(0(),n)
     f#(m,0()) -> g#(m,0())
     f#(s(m),s(n)) -> f#(s(m),n)
     f#(s(m),s(n)) -> p#(m,n)
     f#(s(m),s(n)) -> f#(m,p(m,n))
     f#(s(m),s(n)) -> h#(m,n,f(m,p(m,n)),f(s(m),n))
    TRS:
     f(0(),n) -> g(0(),n)
     f(m,0()) -> g(m,0())
     f(s(m),s(n)) -> h(m,n,f(m,p(m,n)),f(s(m),n))
     g(n,m) -> bot()
     p(m,n) -> bot()
     h(k,l,m,n) -> bot()
    graph:
     f#(s(m),s(n)) -> f#(s(m),n) -> f#(m,0()) -> g#(m,0())
     f#(s(m),s(n)) -> f#(s(m),n) -> f#(s(m),s(n)) -> f#(s(m),n)
     f#(s(m),s(n)) -> f#(s(m),n) -> f#(s(m),s(n)) -> p#(m,n)
     f#(s(m),s(n)) -> f#(s(m),n) -> f#(s(m),s(n)) -> f#(m,p(m,n))
     f#(s(m),s(n)) -> f#(s(m),n) ->
     f#(s(m),s(n)) -> h#(m,n,f(m,p(m,n)),f(s(m),n))
     f#(s(m),s(n)) -> f#(m,p(m,n)) -> f#(0(),n) -> g#(0(),n)
    Restore Modifier:
     DPs:
      f#(0(),n) -> g#(0(),n)
      f#(m,0()) -> g#(m,0())
      f#(s(m),s(n)) -> f#(s(m),n)
      f#(s(m),s(n)) -> p#(m,n)
      f#(s(m),s(n)) -> f#(m,p(m,n))
      f#(s(m),s(n)) -> h#(m,n,f(m,p(m,n)),f(s(m),n))
     TRS:
      f(0(),n) -> g(0(),n)
      f(m,0()) -> g(m,0())
      f(s(m),s(n)) -> h(m,n,f(m,p(m,n)),f(s(m),n))
      g(n,m) -> bot()
      p(m,n) -> bot()
      h(k,l,m,n) -> bot()
     SCC Processor:
      #sccs: 1
      #rules: 1
      #arcs: 6/36
      DPs:
       f#(s(m),s(n)) -> f#(s(m),n)
      TRS:
       f(0(),n) -> g(0(),n)
       f(m,0()) -> g(m,0())
       f(s(m),s(n)) -> h(m,n,f(m,p(m,n)),f(s(m),n))
       g(n,m) -> bot()
       p(m,n) -> bot()
       h(k,l,m,n) -> bot()
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [f#](x0, x1) = x0 + x1 + 1,
        
        [bot] = 0,
        
        [h](x0, x1, x2, x3) = 0,
        
        [p](x0, x1) = 0,
        
        [s](x0) = x0 + 1,
        
        [g](x0, x1) = 0,
        
        [f](x0, x1) = 0,
        
        [0] = 0
       orientation:
        f#(s(m),s(n)) = m + n + 3 >= m + n + 2 = f#(s(m),n)
        
        f(0(),n) = 0 >= 0 = g(0(),n)
        
        f(m,0()) = 0 >= 0 = g(m,0())
        
        f(s(m),s(n)) = 0 >= 0 = h(m,n,f(m,p(m,n)),f(s(m),n))
        
        g(n,m) = 0 >= 0 = bot()
        
        p(m,n) = 0 >= 0 = bot()
        
        h(k,l,m,n) = 0 >= 0 = bot()
       problem:
        DPs:
         
        TRS:
         f(0(),n) -> g(0(),n)
         f(m,0()) -> g(m,0())
         f(s(m),s(n)) -> h(m,n,f(m,p(m,n)),f(s(m),n))
         g(n,m) -> bot()
         p(m,n) -> bot()
         h(k,l,m,n) -> bot()
       Qed