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