YES
Time: 0.001734
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))}
 DP:
  DP:
   {     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))}
  EDG:
   {(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))
    (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, 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, 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, s y, z, u) -> f#(s x, minus(y, x), z, u))}
   SCCS (1):
    Scc:
     {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)}
    SCC (2):
     Strict:
      {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)}
     Weak:
     {     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))}
     SPSC:
      Simple Projection:
       pi(f#) = 0
      Strict:
       {f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u)}
      EDG:
       {(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))}
       SCCS (1):
        Scc:
         {f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u)}
        SCC (1):
         Strict:
          {f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u)}
         Weak:
         {     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))}
         SPSC:
          Simple Projection:
           pi(f#) = 0
          Strict:
           {}
          Qed