YES
Time: 0.018012
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:
  DP:
   {  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)}
  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))}
  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 (3):
    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 (3):
     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 (1):
        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 (2):
         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 (1):
            Scc:
             {f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u)}
            SCC (1):
             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:
              Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
              Interpretation:
               [f](x0, x1, x2, x3) = x0 + 1,
               
               [if](x0, x1, x2) = x0 + x1 + 1,
               
               [minus](x0, x1) = x0,
               
               [le](x0, x1) = x0,
               
               [s](x0) = x0 + 1,
               
               [perfectp](x0) = 0,
               
               [0] = 0,
               
               [true] = 1,
               
               [false] = 1,
               
               [f#](x0, x1, x2, x3) = x0 + x1 + 1
              Strict:
               f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u)
               3 + 1y + 1x + 0u + 0z >= 2 + 1y + 1x + 0u + 0z
              Weak:
               
             Qed
   SCC (1):
    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#) = 1
     Strict:
      {}
     Qed
   SCC (1):
    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#) = 1
     Strict:
      {}
     Qed