YES
TRS:
 {      minus(0(), y) -> 0(),
     minus(s(x), 0()) -> s(x),
    minus(s(x), s(y)) -> minus(x, y),
           le(0(), y) -> true(),
        le(s(x), 0()) -> false(),
       le(s(x), s(y)) -> le(x, y),
     if(true(), x, y) -> x,
    if(false(), x, y) -> y,
        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:
  Strict:
   {  minus#(s(x), s(y)) -> minus#(x, y),
         le#(s(x), s(y)) -> le#(x, y),
         perfectp#(s(x)) -> f#(x, s(0()), s(x), s(x)),
     f#(s(x), 0(), z, u) -> minus#(z, s(x)),
     f#(s(x), 0(), z, u) -> f#(x, u, minus(z, s(x)), u),
    f#(s(x), s(y), z, u) -> minus#(y, x),
    f#(s(x), s(y), z, u) -> le#(x, y),
    f#(s(x), s(y), z, u) -> if#(le(x, y), f(s(x), minus(y, x), 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)}
  Weak:
  {      minus(0(), y) -> 0(),
      minus(s(x), 0()) -> s(x),
     minus(s(x), s(y)) -> minus(x, y),
            le(0(), y) -> true(),
         le(s(x), 0()) -> false(),
        le(s(x), s(y)) -> le(x, y),
      if(true(), x, y) -> x,
     if(false(), x, y) -> y,
         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:
   {(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), s(y), z, u) -> if#(le(x, y), f(s(x), minus(y, x), 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) -> le#(x, y))
    (perfectp#(s(x)) -> f#(x, s(0()), s(x), s(x)), f#(s(x), s(y), z, u) -> minus#(y, x))
    (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), s(y), z, u) -> if#(le(x, y), f(s(x), minus(y, x), 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) -> le#(x, y))
    (f#(s(x), s(y), z, u) -> f#(x, u, z, u), f#(s(x), s(y), z, u) -> minus#(y, x))
    (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), 0(), z, u) -> minus#(z, s(x)))
    (f#(s(x), s(y), z, u) -> minus#(y, x), minus#(s(x), s(y)) -> minus#(x, y))
    (le#(s(x), s(y)) -> le#(x, y), le#(s(x), s(y)) -> le#(x, y))
    (f#(s(x), s(y), z, u) -> le#(x, y), le#(s(x), s(y)) -> le#(x, y))
    (minus#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y))
    (f#(s(x), s(y), z, u) -> f#(s(x), minus(y, x), z, u), f#(s(x), 0(), z, u) -> minus#(z, s(x)))
    (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#(s(x), minus(y, x), z, u), f#(s(x), s(y), z, u) -> minus#(y, x))
    (f#(s(x), s(y), z, u) -> f#(s(x), minus(y, x), z, u), f#(s(x), s(y), z, u) -> le#(x, y))
    (f#(s(x), s(y), z, u) -> f#(s(x), minus(y, x), z, 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)))
    (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), 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), 0(), z, u) -> minus#(z, s(x)))
    (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), 0(), z, u) -> f#(x, u, minus(z, s(x)), u), f#(s(x), s(y), z, u) -> minus#(y, x))
    (f#(s(x), 0(), z, u) -> f#(x, u, minus(z, s(x)), u), f#(s(x), s(y), z, u) -> le#(x, y))
    (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)))
    (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#(s(x), minus(y, x), z, u))
    (f#(s(x), 0(), z, u) -> minus#(z, s(x)), minus#(s(x), s(y)) -> minus#(x, y))}
   SCCS:
    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),
      f#(s(x), s(y), z, u) -> f#(s(x), minus(y, x), z, u)}
    Scc:
     {le#(s(x), s(y)) -> le#(x, y)}
    Scc:
     {minus#(s(x), s(y)) -> minus#(x, y)}
    SCC:
     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),
       f#(s(x), s(y), z, u) -> f#(s(x), minus(y, x), z, u)}
     Weak:
     {      minus(0(), y) -> 0(),
         minus(s(x), 0()) -> s(x),
        minus(s(x), s(y)) -> minus(x, y),
               le(0(), y) -> true(),
            le(s(x), 0()) -> false(),
           le(s(x), s(y)) -> le(x, y),
         if(true(), x, y) -> x,
        if(false(), x, y) -> y,
            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),
        f#(s(x), s(y), z, u) -> f#(s(x), minus(y, x), z, u)}
      EDG:
       {(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), 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), 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))}
       SCCS:
        Scc:
         { 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)}
        SCC:
         Strict:
          { 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)}
         Weak:
         {      minus(0(), y) -> 0(),
             minus(s(x), 0()) -> s(x),
            minus(s(x), s(y)) -> minus(x, y),
                   le(0(), y) -> true(),
                le(s(x), 0()) -> false(),
               le(s(x), s(y)) -> le(x, y),
             if(true(), x, y) -> x,
            if(false(), x, y) -> y,
                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), s(y), z, u) -> f#(s(x), minus(y, x), z, u)}
          EDG:
           {(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))}
           SCCS:
            Scc:
             {f#(s(x), s(y), z, u) -> f#(s(x), minus(y, x), z, u)}
            SCC:
             Strict:
              {f#(s(x), s(y), z, u) -> f#(s(x), minus(y, x), z, u)}
             Weak:
             {      minus(0(), y) -> 0(),
                 minus(s(x), 0()) -> s(x),
                minus(s(x), s(y)) -> minus(x, y),
                       le(0(), y) -> true(),
                    le(s(x), 0()) -> false(),
                   le(s(x), s(y)) -> le(x, y),
                 if(true(), x, y) -> x,
                if(false(), x, y) -> y,
                    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))}
             POLY:
              Argument Filtering:
               pi(f#) = 1, pi(f) = [], pi(perfectp) = [], pi(if) = [], pi(false) = [], pi(le) = [], pi(true) = [], pi(s) = [0], pi(minus) = 0, pi(0) = []
              Usable Rules:
               {}
              Interpretation:
               [s](x0) = x0 + 1
              Strict:
               {}
              Weak:
               {      minus(0(), y) -> 0(),
                   minus(s(x), 0()) -> s(x),
                  minus(s(x), s(y)) -> minus(x, y),
                         le(0(), y) -> true(),
                      le(s(x), 0()) -> false(),
                     le(s(x), s(y)) -> le(x, y),
                   if(true(), x, y) -> x,
                  if(false(), x, y) -> y,
                      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
    SCC:
     Strict:
      {le#(s(x), s(y)) -> le#(x, y)}
     Weak:
     {      minus(0(), y) -> 0(),
         minus(s(x), 0()) -> s(x),
        minus(s(x), s(y)) -> minus(x, y),
               le(0(), y) -> true(),
            le(s(x), 0()) -> false(),
           le(s(x), s(y)) -> le(x, y),
         if(true(), x, y) -> x,
        if(false(), x, y) -> y,
            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(le#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {minus#(s(x), s(y)) -> minus#(x, y)}
     Weak:
     {      minus(0(), y) -> 0(),
         minus(s(x), 0()) -> s(x),
        minus(s(x), s(y)) -> minus(x, y),
               le(0(), y) -> true(),
            le(s(x), 0()) -> false(),
           le(s(x), s(y)) -> le(x, y),
         if(true(), x, y) -> x,
        if(false(), x, y) -> y,
            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(minus#) = 0
      Strict:
       {}
      Qed