YES

Problem:
 perfectp(0()) -> false()
 perfectp(s(x)) -> f(x,s(0()),s(x),s(x))
 f(0(),y,0(),u) -> true()
 f(0(),y,s(z),u) -> false()
 f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u)
 f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))

Proof:
 DP Processor:
  DPs:
   perfectp#(s(x)) -> f#(x,s(0()),s(x),s(x))
   f#(s(x),0(),z,u) -> f#(x,u,minus(z,s(x)),u)
   f#(s(x),s(y),z,u) -> f#(x,u,z,u)
   f#(s(x),s(y),z,u) -> f#(s(x),minus(y,x),z,u)
  TRS:
   perfectp(0()) -> false()
   perfectp(s(x)) -> f(x,s(0()),s(x),s(x))
   f(0(),y,0(),u) -> true()
   f(0(),y,s(z),u) -> false()
   f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u)
   f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
  Usable Rule Processor:
   DPs:
    perfectp#(s(x)) -> f#(x,s(0()),s(x),s(x))
    f#(s(x),0(),z,u) -> f#(x,u,minus(z,s(x)),u)
    f#(s(x),s(y),z,u) -> f#(x,u,z,u)
    f#(s(x),s(y),z,u) -> f#(s(x),minus(y,x),z,u)
   TRS:
    f11(x,y) -> x
    f11(x,y) -> y
   TDG Processor:
    DPs:
     perfectp#(s(x)) -> f#(x,s(0()),s(x),s(x))
     f#(s(x),0(),z,u) -> f#(x,u,minus(z,s(x)),u)
     f#(s(x),s(y),z,u) -> f#(x,u,z,u)
     f#(s(x),s(y),z,u) -> f#(s(x),minus(y,x),z,u)
    TRS:
     f11(x,y) -> x
     f11(x,y) -> y
    graph:
     f#(s(x),s(y),z,u) -> f#(s(x),minus(y,x),z,u) ->
     f#(s(x),s(y),z,u) -> f#(s(x),minus(y,x),z,u)
     f#(s(x),s(y),z,u) -> f#(s(x),minus(y,x),z,u) ->
     f#(s(x),s(y),z,u) -> f#(x,u,z,u)
     f#(s(x),s(y),z,u) -> f#(s(x),minus(y,x),z,u) ->
     f#(s(x),0(),z,u) -> f#(x,u,minus(z,s(x)),u)
     f#(s(x),s(y),z,u) -> f#(x,u,z,u) ->
     f#(s(x),s(y),z,u) -> f#(s(x),minus(y,x),z,u)
     f#(s(x),s(y),z,u) -> f#(x,u,z,u) ->
     f#(s(x),s(y),z,u) -> f#(x,u,z,u)
     f#(s(x),s(y),z,u) -> f#(x,u,z,u) ->
     f#(s(x),0(),z,u) -> f#(x,u,minus(z,s(x)),u)
     f#(s(x),0(),z,u) -> f#(x,u,minus(z,s(x)),u) ->
     f#(s(x),s(y),z,u) -> f#(s(x),minus(y,x),z,u)
     f#(s(x),0(),z,u) -> f#(x,u,minus(z,s(x)),u) ->
     f#(s(x),s(y),z,u) -> f#(x,u,z,u)
     f#(s(x),0(),z,u) -> f#(x,u,minus(z,s(x)),u) ->
     f#(s(x),0(),z,u) -> f#(x,u,minus(z,s(x)),u)
     perfectp#(s(x)) -> f#(x,s(0()),s(x),s(x)) ->
     f#(s(x),s(y),z,u) -> f#(s(x),minus(y,x),z,u)
     perfectp#(s(x)) -> f#(x,s(0()),s(x),s(x)) ->
     f#(s(x),s(y),z,u) -> f#(x,u,z,u)
     perfectp#(s(x)) -> f#(x,s(0()),s(x),s(x)) -> f#(s(x),0(),z,u) -> f#(x,u,minus(z,s(x)),u)
    Restore Modifier:
     DPs:
      perfectp#(s(x)) -> f#(x,s(0()),s(x),s(x))
      f#(s(x),0(),z,u) -> f#(x,u,minus(z,s(x)),u)
      f#(s(x),s(y),z,u) -> f#(x,u,z,u)
      f#(s(x),s(y),z,u) -> f#(s(x),minus(y,x),z,u)
     TRS:
      perfectp(0()) -> false()
      perfectp(s(x)) -> f(x,s(0()),s(x),s(x))
      f(0(),y,0(),u) -> true()
      f(0(),y,s(z),u) -> false()
      f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u)
      f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
     SCC Processor:
      #sccs: 1
      #rules: 3
      #arcs: 12/16
      DPs:
       f#(s(x),s(y),z,u) -> f#(s(x),minus(y,x),z,u)
       f#(s(x),0(),z,u) -> f#(x,u,minus(z,s(x)),u)
       f#(s(x),s(y),z,u) -> f#(x,u,z,u)
      TRS:
       perfectp(0()) -> false()
       perfectp(s(x)) -> f(x,s(0()),s(x),s(x))
       f(0(),y,0(),u) -> true()
       f(0(),y,s(z),u) -> false()
       f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u)
       f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [f#](x0, x1, x2, x3) = x0 + x2 + x3 + 1,
        
        [if](x0, x1, x2) = 0,
        
        [le](x0, x1) = 0,
        
        [minus](x0, x1) = 1,
        
        [true] = 0,
        
        [f](x0, x1, x2, x3) = 0,
        
        [s](x0) = x0 + 1,
        
        [false] = 0,
        
        [perfectp](x0) = 0,
        
        [0] = 1
       orientation:
        f#(s(x),s(y),z,u) = u + x + z + 2 >= u + x + z + 2 = f#(s(x),minus(y,x),z,u)
        
        f#(s(x),0(),z,u) = u + x + z + 2 >= u + x + 2 = f#(x,u,minus(z,s(x)),u)
        
        f#(s(x),s(y),z,u) = u + x + z + 2 >= u + x + z + 1 = f#(x,u,z,u)
        
        perfectp(0()) = 0 >= 0 = false()
        
        perfectp(s(x)) = 0 >= 0 = f(x,s(0()),s(x),s(x))
        
        f(0(),y,0(),u) = 0 >= 0 = true()
        
        f(0(),y,s(z),u) = 0 >= 0 = false()
        
        f(s(x),0(),z,u) = 0 >= 0 = f(x,u,minus(z,s(x)),u)
        
        f(s(x),s(y),z,u) = 0 >= 0 = if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
       problem:
        DPs:
         f#(s(x),s(y),z,u) -> f#(s(x),minus(y,x),z,u)
         f#(s(x),0(),z,u) -> f#(x,u,minus(z,s(x)),u)
        TRS:
         perfectp(0()) -> false()
         perfectp(s(x)) -> f(x,s(0()),s(x),s(x))
         f(0(),y,0(),u) -> true()
         f(0(),y,s(z),u) -> false()
         f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u)
         f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [f#](x0, x1, x2, x3) = x0 + 1,
         
         [if](x0, x1, x2) = 0,
         
         [le](x0, x1) = 0,
         
         [minus](x0, x1) = 0,
         
         [true] = 0,
         
         [f](x0, x1, x2, x3) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [false] = 0,
         
         [perfectp](x0) = x0,
         
         [0] = 0
        orientation:
         f#(s(x),s(y),z,u) = x + 2 >= x + 2 = f#(s(x),minus(y,x),z,u)
         
         f#(s(x),0(),z,u) = x + 2 >= x + 1 = f#(x,u,minus(z,s(x)),u)
         
         perfectp(0()) = 0 >= 0 = false()
         
         perfectp(s(x)) = x + 1 >= x + 1 = f(x,s(0()),s(x),s(x))
         
         f(0(),y,0(),u) = 1 >= 0 = true()
         
         f(0(),y,s(z),u) = 1 >= 0 = false()
         
         f(s(x),0(),z,u) = x + 2 >= x + 1 = f(x,u,minus(z,s(x)),u)
         
         f(s(x),s(y),z,u) = x + 2 >= 0 = if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
        problem:
         DPs:
          f#(s(x),s(y),z,u) -> f#(s(x),minus(y,x),z,u)
         TRS:
          perfectp(0()) -> false()
          perfectp(s(x)) -> f(x,s(0()),s(x),s(x))
          f(0(),y,0(),u) -> true()
          f(0(),y,s(z),u) -> false()
          f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u)
          f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
        Matrix Interpretation Processor:
         dimension: 1
         interpretation:
          [f#](x0, x1, x2, x3) = x1,
          
          [if](x0, x1, x2) = 0,
          
          [le](x0, x1) = 0,
          
          [minus](x0, x1) = 0,
          
          [true] = 0,
          
          [f](x0, x1, x2, x3) = 0,
          
          [s](x0) = 1,
          
          [false] = 0,
          
          [perfectp](x0) = 0,
          
          [0] = 0
         orientation:
          f#(s(x),s(y),z,u) = 1 >= 0 = f#(s(x),minus(y,x),z,u)
          
          perfectp(0()) = 0 >= 0 = false()
          
          perfectp(s(x)) = 0 >= 0 = f(x,s(0()),s(x),s(x))
          
          f(0(),y,0(),u) = 0 >= 0 = true()
          
          f(0(),y,s(z),u) = 0 >= 0 = false()
          
          f(s(x),0(),z,u) = 0 >= 0 = f(x,u,minus(z,s(x)),u)
          
          f(s(x),s(y),z,u) = 0 >= 0 = if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
         problem:
          DPs:
           
          TRS:
           perfectp(0()) -> false()
           perfectp(s(x)) -> f(x,s(0()),s(x),s(x))
           f(0(),y,0(),u) -> true()
           f(0(),y,s(z),u) -> false()
           f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u)
           f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
         Qed