MAYBE
TRS:
 {                      0() -> n__0(),
                       p(X) -> n__p(X),
                     p(0()) -> 0(),
                    p(s(X)) -> X,
                       s(X) -> n__s(X),
                leq(0(), Y) -> true(),
             leq(s(X), 0()) -> false(),
            leq(s(X), s(Y)) -> leq(X, Y),
                activate(X) -> X,
           activate(n__0()) -> 0(),
          activate(n__s(X)) -> s(activate(X)),
  activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)),
          activate(n__p(X)) -> p(activate(X)),
           if(true(), X, Y) -> activate(X),
          if(false(), X, Y) -> activate(Y),
                 diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))),
               diff(X1, X2) -> n__diff(X1, X2)}
 DP:
  Strict:
   {          leq#(s(X), s(Y)) -> leq#(X, Y),
             activate#(n__0()) -> 0#(),
            activate#(n__s(X)) -> s#(activate(X)),
            activate#(n__s(X)) -> activate#(X),
    activate#(n__diff(X1, X2)) -> activate#(X1),
    activate#(n__diff(X1, X2)) -> activate#(X2),
    activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)),
            activate#(n__p(X)) -> p#(activate(X)),
            activate#(n__p(X)) -> activate#(X),
             if#(true(), X, Y) -> activate#(X),
            if#(false(), X, Y) -> activate#(Y),
                   diff#(X, Y) -> leq#(X, Y),
                   diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))}
  Weak:
  {                      0() -> n__0(),
                        p(X) -> n__p(X),
                      p(0()) -> 0(),
                     p(s(X)) -> X,
                        s(X) -> n__s(X),
                 leq(0(), Y) -> true(),
              leq(s(X), 0()) -> false(),
             leq(s(X), s(Y)) -> leq(X, Y),
                 activate(X) -> X,
            activate(n__0()) -> 0(),
           activate(n__s(X)) -> s(activate(X)),
   activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)),
           activate(n__p(X)) -> p(activate(X)),
            if(true(), X, Y) -> activate(X),
           if(false(), X, Y) -> activate(Y),
                  diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))),
                diff(X1, X2) -> n__diff(X1, X2)}
  EDG:
   {(activate#(n__p(X)) -> activate#(X), activate#(n__p(X)) -> activate#(X))
    (activate#(n__p(X)) -> activate#(X), activate#(n__p(X)) -> p#(activate(X)))
    (activate#(n__p(X)) -> activate#(X), activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)))
    (activate#(n__p(X)) -> activate#(X), activate#(n__diff(X1, X2)) -> activate#(X2))
    (activate#(n__p(X)) -> activate#(X), activate#(n__diff(X1, X2)) -> activate#(X1))
    (activate#(n__p(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X))
    (activate#(n__p(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X)))
    (activate#(n__p(X)) -> activate#(X), activate#(n__0()) -> 0#())
    (diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))), if#(false(), X, Y) -> activate#(Y))
    (diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))), if#(true(), X, Y) -> activate#(X))
    (activate#(n__diff(X1, X2)) -> activate#(X1), activate#(n__p(X)) -> activate#(X))
    (activate#(n__diff(X1, X2)) -> activate#(X1), activate#(n__p(X)) -> p#(activate(X)))
    (activate#(n__diff(X1, X2)) -> activate#(X1), activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)))
    (activate#(n__diff(X1, X2)) -> activate#(X1), activate#(n__diff(X1, X2)) -> activate#(X2))
    (activate#(n__diff(X1, X2)) -> activate#(X1), activate#(n__diff(X1, X2)) -> activate#(X1))
    (activate#(n__diff(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X))
    (activate#(n__diff(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> s#(activate(X)))
    (activate#(n__diff(X1, X2)) -> activate#(X1), activate#(n__0()) -> 0#())
    (activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)), diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))))
    (activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)), diff#(X, Y) -> leq#(X, Y))
    (leq#(s(X), s(Y)) -> leq#(X, Y), leq#(s(X), s(Y)) -> leq#(X, Y))
    (diff#(X, Y) -> leq#(X, Y), leq#(s(X), s(Y)) -> leq#(X, Y))
    (activate#(n__diff(X1, X2)) -> activate#(X2), activate#(n__0()) -> 0#())
    (activate#(n__diff(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> s#(activate(X)))
    (activate#(n__diff(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> activate#(X))
    (activate#(n__diff(X1, X2)) -> activate#(X2), activate#(n__diff(X1, X2)) -> activate#(X1))
    (activate#(n__diff(X1, X2)) -> activate#(X2), activate#(n__diff(X1, X2)) -> activate#(X2))
    (activate#(n__diff(X1, X2)) -> activate#(X2), activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)))
    (activate#(n__diff(X1, X2)) -> activate#(X2), activate#(n__p(X)) -> p#(activate(X)))
    (activate#(n__diff(X1, X2)) -> activate#(X2), activate#(n__p(X)) -> activate#(X))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__0()) -> 0#())
    (if#(false(), X, Y) -> activate#(Y), activate#(n__s(X)) -> s#(activate(X)))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__s(X)) -> activate#(X))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__diff(X1, X2)) -> activate#(X1))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__diff(X1, X2)) -> activate#(X2))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__p(X)) -> p#(activate(X)))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__p(X)) -> activate#(X))
    (if#(true(), X, Y) -> activate#(X), activate#(n__0()) -> 0#())
    (if#(true(), X, Y) -> activate#(X), activate#(n__s(X)) -> s#(activate(X)))
    (if#(true(), X, Y) -> activate#(X), activate#(n__s(X)) -> activate#(X))
    (if#(true(), X, Y) -> activate#(X), activate#(n__diff(X1, X2)) -> activate#(X1))
    (if#(true(), X, Y) -> activate#(X), activate#(n__diff(X1, X2)) -> activate#(X2))
    (if#(true(), X, Y) -> activate#(X), activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)))
    (if#(true(), X, Y) -> activate#(X), activate#(n__p(X)) -> p#(activate(X)))
    (if#(true(), X, Y) -> activate#(X), activate#(n__p(X)) -> activate#(X))
    (activate#(n__s(X)) -> activate#(X), activate#(n__0()) -> 0#())
    (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X)))
    (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X))
    (activate#(n__s(X)) -> activate#(X), activate#(n__diff(X1, X2)) -> activate#(X1))
    (activate#(n__s(X)) -> activate#(X), activate#(n__diff(X1, X2)) -> activate#(X2))
    (activate#(n__s(X)) -> activate#(X), activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)))
    (activate#(n__s(X)) -> activate#(X), activate#(n__p(X)) -> p#(activate(X)))
    (activate#(n__s(X)) -> activate#(X), activate#(n__p(X)) -> activate#(X))}
   SCCS:
    Scc:
     {        activate#(n__s(X)) -> activate#(X),
      activate#(n__diff(X1, X2)) -> activate#(X1),
      activate#(n__diff(X1, X2)) -> activate#(X2),
      activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)),
              activate#(n__p(X)) -> activate#(X),
               if#(true(), X, Y) -> activate#(X),
              if#(false(), X, Y) -> activate#(Y),
                     diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))}
    Scc:
     {leq#(s(X), s(Y)) -> leq#(X, Y)}
    SCC:
     Strict:
      {        activate#(n__s(X)) -> activate#(X),
       activate#(n__diff(X1, X2)) -> activate#(X1),
       activate#(n__diff(X1, X2)) -> activate#(X2),
       activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)),
               activate#(n__p(X)) -> activate#(X),
                if#(true(), X, Y) -> activate#(X),
               if#(false(), X, Y) -> activate#(Y),
                      diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))}
     Weak:
     {                      0() -> n__0(),
                           p(X) -> n__p(X),
                         p(0()) -> 0(),
                        p(s(X)) -> X,
                           s(X) -> n__s(X),
                    leq(0(), Y) -> true(),
                 leq(s(X), 0()) -> false(),
                leq(s(X), s(Y)) -> leq(X, Y),
                    activate(X) -> X,
               activate(n__0()) -> 0(),
              activate(n__s(X)) -> s(activate(X)),
      activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)),
              activate(n__p(X)) -> p(activate(X)),
               if(true(), X, Y) -> activate(X),
              if(false(), X, Y) -> activate(Y),
                     diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))),
                   diff(X1, X2) -> n__diff(X1, X2)}
     POLY:
      Argument Filtering:
       pi(diff#) = [0,1], pi(diff) = [0,1], pi(n__p) = 0, pi(n__diff) = [0,1], pi(n__s) = 0, pi(n__0) = [], pi(if#) = [1,2], pi(if) = [1,2], pi(activate#) = 0, pi(activate) = 0, pi(false) = [], pi(leq) = [], pi(true) = [], pi(s) = 0, pi(p) = 0, pi(0) = []
      Usable Rules:
       {}
      Interpretation:
       [if#](x0, x1) = x0 + x1,
       [diff#](x0, x1) = x0 + x1 + 1,
       [n__diff](x0, x1) = x0 + x1 + 1,
       [n__0] = 0
      Strict:
       {        activate#(n__s(X)) -> activate#(X),
        activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)),
                activate#(n__p(X)) -> activate#(X),
                 if#(true(), X, Y) -> activate#(X),
                if#(false(), X, Y) -> activate#(Y),
                       diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))}
      Weak:
       {                      0() -> n__0(),
                             p(X) -> n__p(X),
                           p(0()) -> 0(),
                          p(s(X)) -> X,
                             s(X) -> n__s(X),
                      leq(0(), Y) -> true(),
                   leq(s(X), 0()) -> false(),
                  leq(s(X), s(Y)) -> leq(X, Y),
                      activate(X) -> X,
                 activate(n__0()) -> 0(),
                activate(n__s(X)) -> s(activate(X)),
        activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)),
                activate(n__p(X)) -> p(activate(X)),
                 if(true(), X, Y) -> activate(X),
                if(false(), X, Y) -> activate(Y),
                       diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))),
                     diff(X1, X2) -> n__diff(X1, X2)}
      EDG:
       {(activate#(n__p(X)) -> activate#(X), activate#(n__p(X)) -> activate#(X))
        (activate#(n__p(X)) -> activate#(X), activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)))
        (activate#(n__p(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X))
        (activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)), diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))))
        (if#(false(), X, Y) -> activate#(Y), activate#(n__p(X)) -> activate#(X))
        (if#(false(), X, Y) -> activate#(Y), activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)))
        (if#(false(), X, Y) -> activate#(Y), activate#(n__s(X)) -> activate#(X))
        (diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))), if#(true(), X, Y) -> activate#(X))
        (diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))), if#(false(), X, Y) -> activate#(Y))
        (if#(true(), X, Y) -> activate#(X), activate#(n__s(X)) -> activate#(X))
        (if#(true(), X, Y) -> activate#(X), activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)))
        (if#(true(), X, Y) -> activate#(X), activate#(n__p(X)) -> activate#(X))
        (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X))
        (activate#(n__s(X)) -> activate#(X), activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)))
        (activate#(n__s(X)) -> activate#(X), activate#(n__p(X)) -> activate#(X))}
       SCCS:
        Scc:
         {        activate#(n__s(X)) -> activate#(X),
          activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)),
                  activate#(n__p(X)) -> activate#(X),
                   if#(true(), X, Y) -> activate#(X),
                  if#(false(), X, Y) -> activate#(Y),
                         diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))}
        SCC:
         Strict:
          {        activate#(n__s(X)) -> activate#(X),
           activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)),
                   activate#(n__p(X)) -> activate#(X),
                    if#(true(), X, Y) -> activate#(X),
                   if#(false(), X, Y) -> activate#(Y),
                          diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))}
         Weak:
         {                      0() -> n__0(),
                               p(X) -> n__p(X),
                             p(0()) -> 0(),
                            p(s(X)) -> X,
                               s(X) -> n__s(X),
                        leq(0(), Y) -> true(),
                     leq(s(X), 0()) -> false(),
                    leq(s(X), s(Y)) -> leq(X, Y),
                        activate(X) -> X,
                   activate(n__0()) -> 0(),
                  activate(n__s(X)) -> s(activate(X)),
          activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)),
                  activate(n__p(X)) -> p(activate(X)),
                   if(true(), X, Y) -> activate(X),
                  if(false(), X, Y) -> activate(Y),
                         diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))),
                       diff(X1, X2) -> n__diff(X1, X2)}
         POLY:
          Argument Filtering:
           pi(diff#) = [], pi(diff) = [], pi(n__p) = [0], pi(n__diff) = [], pi(n__s) = 0, pi(n__0) = [], pi(if#) = [1,2], pi(if) = [], pi(activate#) = 0, pi(activate) = [], pi(false) = [], pi(leq) = [], pi(true) = [], pi(s) = [], pi(p) = [], pi(0) = []
          Usable Rules:
           {}
          Interpretation:
           [if#](x0, x1) = x0 + x1,
           [diff#] = 0,
           [n__diff] = 0,
           [n__p](x0) = x0 + 1,
           [n__0] = 0
          Strict:
           {        activate#(n__s(X)) -> activate#(X),
            activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)),
                     if#(true(), X, Y) -> activate#(X),
                    if#(false(), X, Y) -> activate#(Y),
                           diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))}
          Weak:
           {                      0() -> n__0(),
                                 p(X) -> n__p(X),
                               p(0()) -> 0(),
                              p(s(X)) -> X,
                                 s(X) -> n__s(X),
                          leq(0(), Y) -> true(),
                       leq(s(X), 0()) -> false(),
                      leq(s(X), s(Y)) -> leq(X, Y),
                          activate(X) -> X,
                     activate(n__0()) -> 0(),
                    activate(n__s(X)) -> s(activate(X)),
            activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)),
                    activate(n__p(X)) -> p(activate(X)),
                     if(true(), X, Y) -> activate(X),
                    if(false(), X, Y) -> activate(Y),
                           diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))),
                         diff(X1, X2) -> n__diff(X1, X2)}
          EDG:
           {(if#(true(), X, Y) -> activate#(X), activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)))
            (if#(true(), X, Y) -> activate#(X), activate#(n__s(X)) -> activate#(X))
            (diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))), if#(false(), X, Y) -> activate#(Y))
            (diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))), if#(true(), X, Y) -> activate#(X))
            (activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)), diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))))
            (if#(false(), X, Y) -> activate#(Y), activate#(n__s(X)) -> activate#(X))
            (if#(false(), X, Y) -> activate#(Y), activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)))
            (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X))
            (activate#(n__s(X)) -> activate#(X), activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)))}
           SCCS:
            Scc:
             {        activate#(n__s(X)) -> activate#(X),
              activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)),
                       if#(true(), X, Y) -> activate#(X),
                      if#(false(), X, Y) -> activate#(Y),
                             diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))}
            SCC:
             Strict:
              {        activate#(n__s(X)) -> activate#(X),
               activate#(n__diff(X1, X2)) -> diff#(activate(X1), activate(X2)),
                        if#(true(), X, Y) -> activate#(X),
                       if#(false(), X, Y) -> activate#(Y),
                              diff#(X, Y) -> if#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))}
             Weak:
             {                      0() -> n__0(),
                                   p(X) -> n__p(X),
                                 p(0()) -> 0(),
                                p(s(X)) -> X,
                                   s(X) -> n__s(X),
                            leq(0(), Y) -> true(),
                         leq(s(X), 0()) -> false(),
                        leq(s(X), s(Y)) -> leq(X, Y),
                            activate(X) -> X,
                       activate(n__0()) -> 0(),
                      activate(n__s(X)) -> s(activate(X)),
              activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)),
                      activate(n__p(X)) -> p(activate(X)),
                       if(true(), X, Y) -> activate(X),
                      if(false(), X, Y) -> activate(Y),
                             diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))),
                           diff(X1, X2) -> n__diff(X1, X2)}
             Fail
    SCC:
     Strict:
      {leq#(s(X), s(Y)) -> leq#(X, Y)}
     Weak:
     {                      0() -> n__0(),
                           p(X) -> n__p(X),
                         p(0()) -> 0(),
                        p(s(X)) -> X,
                           s(X) -> n__s(X),
                    leq(0(), Y) -> true(),
                 leq(s(X), 0()) -> false(),
                leq(s(X), s(Y)) -> leq(X, Y),
                    activate(X) -> X,
               activate(n__0()) -> 0(),
              activate(n__s(X)) -> s(activate(X)),
      activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2)),
              activate(n__p(X)) -> p(activate(X)),
               if(true(), X, Y) -> activate(X),
              if(false(), X, Y) -> activate(Y),
                     diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))),
                   diff(X1, X2) -> n__diff(X1, X2)}
     SPSC:
      Simple Projection:
       pi(leq#) = 0
      Strict:
       {}
      Qed