YES

Problem:
 f(s(x)) -> s(s(f(p(s(x)))))
 f(0()) -> 0()
 p(s(x)) -> x

Proof:
 Matrix Interpretation Processor: dim=3
  
  interpretation:
         [0]
   [0] = [0]
         [0],
   
               
   [p](x0) = x0
               ,
   
             [1 0 0]     [1]
   [f](x0) = [0 0 0]x0 + [0]
             [1 0 0]     [1],
   
               
   [s](x0) = x0
               
  orientation:
             [1 0 0]    [1]    [1 0 0]    [1]                   
   f(s(x)) = [0 0 0]x + [0] >= [0 0 0]x + [0] = s(s(f(p(s(x)))))
             [1 0 0]    [1]    [1 0 0]    [1]                   
   
            [1]    [0]      
   f(0()) = [0] >= [0] = 0()
            [1]    [0]      
   
                       
   p(s(x)) = x >= x = x
                       
  problem:
   f(s(x)) -> s(s(f(p(s(x)))))
   p(s(x)) -> x
  DP Processor:
   DPs:
    f#(s(x)) -> p#(s(x))
    f#(s(x)) -> f#(p(s(x)))
   TRS:
    f(s(x)) -> s(s(f(p(s(x)))))
    p(s(x)) -> x
   TDG Processor:
    DPs:
     f#(s(x)) -> p#(s(x))
     f#(s(x)) -> f#(p(s(x)))
    TRS:
     f(s(x)) -> s(s(f(p(s(x)))))
     p(s(x)) -> x
    graph:
     f#(s(x)) -> f#(p(s(x))) -> f#(s(x)) -> f#(p(s(x)))
     f#(s(x)) -> f#(p(s(x))) -> f#(s(x)) -> p#(s(x))
    SCC Processor:
     #sccs: 1
     #rules: 1
     #arcs: 2/4
     DPs:
      f#(s(x)) -> f#(p(s(x)))
     TRS:
      f(s(x)) -> s(s(f(p(s(x)))))
      p(s(x)) -> x
     CDG Processor:
      DPs:
       f#(s(x)) -> f#(p(s(x)))
      TRS:
       f(s(x)) -> s(s(f(p(s(x)))))
       p(s(x)) -> x
      graph:
       
      Qed