MAYBE
Time: 0.022022
TRS:
 {            p 0() -> 0(),
              p s x -> x,
         le(0(), y) -> true(),
       le(s x, 0()) -> false(),
       le(s x, s y) -> le(x, y),
   if(true(), x, y) -> 0(),
  if(false(), x, y) -> s minus(p x, y),
        minus(x, y) -> if(le(x, y), x, y)}
 DP:
  DP:
   {     le#(s x, s y) -> le#(x, y),
    if#(false(), x, y) -> p# x,
    if#(false(), x, y) -> minus#(p x, y),
          minus#(x, y) -> le#(x, y),
          minus#(x, y) -> if#(le(x, y), x, y)}
  TRS:
  {            p 0() -> 0(),
               p s x -> x,
          le(0(), y) -> true(),
        le(s x, 0()) -> false(),
        le(s x, s y) -> le(x, y),
    if(true(), x, y) -> 0(),
   if(false(), x, y) -> s minus(p x, y),
         minus(x, y) -> if(le(x, y), x, y)}
  UR:
   {       p 0() -> 0(),
           p s x -> x,
      le(0(), y) -> true(),
    le(s x, 0()) -> false(),
    le(s x, s y) -> le(x, y)}
   EDG:
    {(minus#(x, y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
     (minus#(x, y) -> if#(le(x, y), x, y), if#(false(), x, y) -> minus#(p x, y))
     (minus#(x, y) -> if#(le(x, y), x, y), if#(false(), x, y) -> p# x)
     (if#(false(), x, y) -> minus#(p x, y), minus#(x, y) -> le#(x, y))
     (if#(false(), x, y) -> minus#(p x, y), minus#(x, y) -> if#(le(x, y), x, y))
     (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))}
    EDG:
     {(minus#(x, y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
      (minus#(x, y) -> if#(le(x, y), x, y), if#(false(), x, y) -> minus#(p x, y))
      (minus#(x, y) -> if#(le(x, y), x, y), if#(false(), x, y) -> p# x)
      (if#(false(), x, y) -> minus#(p x, y), minus#(x, y) -> le#(x, y))
      (if#(false(), x, y) -> minus#(p x, y), minus#(x, y) -> if#(le(x, y), x, y))
      (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))}
     EDG:
      {(minus#(x, y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
       (minus#(x, y) -> if#(le(x, y), x, y), if#(false(), x, y) -> minus#(p x, y))
       (minus#(x, y) -> if#(le(x, y), x, y), if#(false(), x, y) -> p# x)
       (if#(false(), x, y) -> minus#(p x, y), minus#(x, y) -> le#(x, y))
       (if#(false(), x, y) -> minus#(p x, y), minus#(x, y) -> if#(le(x, y), x, y))
       (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))}
      EDG:
       {(minus#(x, y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
        (minus#(x, y) -> if#(le(x, y), x, y), if#(false(), x, y) -> minus#(p x, y))
        (minus#(x, y) -> if#(le(x, y), x, y), if#(false(), x, y) -> p# x)
        (if#(false(), x, y) -> minus#(p x, y), minus#(x, y) -> le#(x, y))
        (if#(false(), x, y) -> minus#(p x, y), minus#(x, y) -> if#(le(x, y), x, y))
        (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))}
       STATUS:
        arrows: 0.760000
        SCCS (2):
         Scc:
          {if#(false(), x, y) -> minus#(p x, y),
                 minus#(x, y) -> if#(le(x, y), x, y)}
         Scc:
          {le#(s x, s y) -> le#(x, y)}
         
         SCC (2):
          Strict:
           {if#(false(), x, y) -> minus#(p x, y),
                  minus#(x, y) -> if#(le(x, y), x, y)}
          Weak:
          {            p 0() -> 0(),
                       p s x -> x,
                  le(0(), y) -> true(),
                le(s x, 0()) -> false(),
                le(s x, s y) -> le(x, y),
            if(true(), x, y) -> 0(),
           if(false(), x, y) -> s minus(p x, y),
                 minus(x, y) -> if(le(x, y), x, y)}
          Fail
         
         
         SCC (1):
          Strict:
           {le#(s x, s y) -> le#(x, y)}
          Weak:
          {            p 0() -> 0(),
                       p s x -> x,
                  le(0(), y) -> true(),
                le(s x, 0()) -> false(),
                le(s x, s y) -> le(x, y),
            if(true(), x, y) -> 0(),
           if(false(), x, y) -> s minus(p x, y),
                 minus(x, y) -> if(le(x, y), x, y)}
          POLY:
           Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
           Interpretation:
            [if](x0, x1, x2) = 0,
            
            [le](x0, x1) = x0 + 1,
            
            [minus](x0, x1) = x0 + 1,
            
            [p](x0) = x0 + 1,
            
            [s](x0) = x0 + 1,
            
            [0] = 1,
            
            [true] = 0,
            
            [false] = 0,
            
            [le#](x0, x1) = x0
           Strict:
            le#(s x, s y) -> le#(x, y)
            1 + 0x + 1y >= 0 + 0x + 1y
           Weak:
            minus(x, y) -> if(le(x, y), x, y)
            1 + 1x + 0y >= 0 + 0x + 0y
            if(false(), x, y) -> s minus(p x, y)
            0 + 0x + 0y >= 3 + 1x + 0y
            if(true(), x, y) -> 0()
            0 + 0x + 0y >= 1
            le(s x, s y) -> le(x, y)
            2 + 1x + 0y >= 1 + 1x + 0y
            le(s x, 0()) -> false()
            2 + 1x >= 0
            le(0(), y) -> true()
            2 + 0y >= 0
            p s x -> x
            2 + 1x >= 1x
            p 0() -> 0()
            2 >= 1
          Qed