YES
TRS:
 {      minus_active(x, y) -> minus(x, y),
      minus_active(0(), y) -> 0(),
  minus_active(s(x), s(y)) -> minus_active(x, y),
                 mark(0()) -> 0(),
                mark(s(x)) -> s(mark(x)),
         mark(minus(x, y)) -> minus_active(x, y),
            mark(ge(x, y)) -> ge_active(x, y),
           mark(div(x, y)) -> div_active(mark(x), y),
         mark(if(x, y, z)) -> if_active(mark(x), y, z),
           ge_active(x, y) -> ge(x, y),
         ge_active(x, 0()) -> true(),
      ge_active(0(), s(y)) -> false(),
     ge_active(s(x), s(y)) -> ge_active(x, y),
          div_active(x, y) -> div(x, y),
     div_active(0(), s(y)) -> 0(),
    div_active(s(x), s(y)) -> if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
        if_active(x, y, z) -> if(x, y, z),
   if_active(true(), x, y) -> mark(x),
  if_active(false(), x, y) -> mark(y)}
 DP:
  Strict:
   {minus_active#(s(x), s(y)) -> minus_active#(x, y),
                  mark#(s(x)) -> mark#(x),
           mark#(minus(x, y)) -> minus_active#(x, y),
              mark#(ge(x, y)) -> ge_active#(x, y),
             mark#(div(x, y)) -> mark#(x),
             mark#(div(x, y)) -> div_active#(mark(x), y),
           mark#(if(x, y, z)) -> mark#(x),
           mark#(if(x, y, z)) -> if_active#(mark(x), y, z),
       ge_active#(s(x), s(y)) -> ge_active#(x, y),
      div_active#(s(x), s(y)) -> ge_active#(x, y),
      div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
     if_active#(true(), x, y) -> mark#(x),
    if_active#(false(), x, y) -> mark#(y)}
  Weak:
  {      minus_active(x, y) -> minus(x, y),
       minus_active(0(), y) -> 0(),
   minus_active(s(x), s(y)) -> minus_active(x, y),
                  mark(0()) -> 0(),
                 mark(s(x)) -> s(mark(x)),
          mark(minus(x, y)) -> minus_active(x, y),
             mark(ge(x, y)) -> ge_active(x, y),
            mark(div(x, y)) -> div_active(mark(x), y),
          mark(if(x, y, z)) -> if_active(mark(x), y, z),
            ge_active(x, y) -> ge(x, y),
          ge_active(x, 0()) -> true(),
       ge_active(0(), s(y)) -> false(),
      ge_active(s(x), s(y)) -> ge_active(x, y),
           div_active(x, y) -> div(x, y),
      div_active(0(), s(y)) -> 0(),
     div_active(s(x), s(y)) -> if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
         if_active(x, y, z) -> if(x, y, z),
    if_active(true(), x, y) -> mark(x),
   if_active(false(), x, y) -> mark(y)}
  EDG:
   {(div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()), if_active#(false(), x, y) -> mark#(y))
    (div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()), if_active#(true(), x, y) -> mark#(x))
    (if_active#(false(), x, y) -> mark#(y), mark#(if(x, y, z)) -> if_active#(mark(x), y, z))
    (if_active#(false(), x, y) -> mark#(y), mark#(if(x, y, z)) -> mark#(x))
    (if_active#(false(), x, y) -> mark#(y), mark#(div(x, y)) -> div_active#(mark(x), y))
    (if_active#(false(), x, y) -> mark#(y), mark#(div(x, y)) -> mark#(x))
    (if_active#(false(), x, y) -> mark#(y), mark#(ge(x, y)) -> ge_active#(x, y))
    (if_active#(false(), x, y) -> mark#(y), mark#(minus(x, y)) -> minus_active#(x, y))
    (if_active#(false(), x, y) -> mark#(y), mark#(s(x)) -> mark#(x))
    (mark#(div(x, y)) -> mark#(x), mark#(if(x, y, z)) -> if_active#(mark(x), y, z))
    (mark#(div(x, y)) -> mark#(x), mark#(if(x, y, z)) -> mark#(x))
    (mark#(div(x, y)) -> mark#(x), mark#(div(x, y)) -> div_active#(mark(x), y))
    (mark#(div(x, y)) -> mark#(x), mark#(div(x, y)) -> mark#(x))
    (mark#(div(x, y)) -> mark#(x), mark#(ge(x, y)) -> ge_active#(x, y))
    (mark#(div(x, y)) -> mark#(x), mark#(minus(x, y)) -> minus_active#(x, y))
    (mark#(div(x, y)) -> mark#(x), mark#(s(x)) -> mark#(x))
    (if_active#(true(), x, y) -> mark#(x), mark#(if(x, y, z)) -> if_active#(mark(x), y, z))
    (if_active#(true(), x, y) -> mark#(x), mark#(if(x, y, z)) -> mark#(x))
    (if_active#(true(), x, y) -> mark#(x), mark#(div(x, y)) -> div_active#(mark(x), y))
    (if_active#(true(), x, y) -> mark#(x), mark#(div(x, y)) -> mark#(x))
    (if_active#(true(), x, y) -> mark#(x), mark#(ge(x, y)) -> ge_active#(x, y))
    (if_active#(true(), x, y) -> mark#(x), mark#(minus(x, y)) -> minus_active#(x, y))
    (if_active#(true(), x, y) -> mark#(x), mark#(s(x)) -> mark#(x))
    (mark#(minus(x, y)) -> minus_active#(x, y), minus_active#(s(x), s(y)) -> minus_active#(x, y))
    (ge_active#(s(x), s(y)) -> ge_active#(x, y), ge_active#(s(x), s(y)) -> ge_active#(x, y))
    (div_active#(s(x), s(y)) -> ge_active#(x, y), ge_active#(s(x), s(y)) -> ge_active#(x, y))
    (mark#(ge(x, y)) -> ge_active#(x, y), ge_active#(s(x), s(y)) -> ge_active#(x, y))
    (minus_active#(s(x), s(y)) -> minus_active#(x, y), minus_active#(s(x), s(y)) -> minus_active#(x, y))
    (mark#(if(x, y, z)) -> mark#(x), mark#(s(x)) -> mark#(x))
    (mark#(if(x, y, z)) -> mark#(x), mark#(minus(x, y)) -> minus_active#(x, y))
    (mark#(if(x, y, z)) -> mark#(x), mark#(ge(x, y)) -> ge_active#(x, y))
    (mark#(if(x, y, z)) -> mark#(x), mark#(div(x, y)) -> mark#(x))
    (mark#(if(x, y, z)) -> mark#(x), mark#(div(x, y)) -> div_active#(mark(x), y))
    (mark#(if(x, y, z)) -> mark#(x), mark#(if(x, y, z)) -> mark#(x))
    (mark#(if(x, y, z)) -> mark#(x), mark#(if(x, y, z)) -> if_active#(mark(x), y, z))
    (mark#(s(x)) -> mark#(x), mark#(s(x)) -> mark#(x))
    (mark#(s(x)) -> mark#(x), mark#(minus(x, y)) -> minus_active#(x, y))
    (mark#(s(x)) -> mark#(x), mark#(ge(x, y)) -> ge_active#(x, y))
    (mark#(s(x)) -> mark#(x), mark#(div(x, y)) -> mark#(x))
    (mark#(s(x)) -> mark#(x), mark#(div(x, y)) -> div_active#(mark(x), y))
    (mark#(s(x)) -> mark#(x), mark#(if(x, y, z)) -> mark#(x))
    (mark#(s(x)) -> mark#(x), mark#(if(x, y, z)) -> if_active#(mark(x), y, z))
    (mark#(if(x, y, z)) -> if_active#(mark(x), y, z), if_active#(true(), x, y) -> mark#(x))
    (mark#(if(x, y, z)) -> if_active#(mark(x), y, z), if_active#(false(), x, y) -> mark#(y))
    (mark#(div(x, y)) -> div_active#(mark(x), y), div_active#(s(x), s(y)) -> ge_active#(x, y))
    (mark#(div(x, y)) -> div_active#(mark(x), y), div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()))}
   SCCS:
    Scc:
     {ge_active#(s(x), s(y)) -> ge_active#(x, y)}
    Scc:
     {              mark#(s(x)) -> mark#(x),
               mark#(div(x, y)) -> mark#(x),
               mark#(div(x, y)) -> div_active#(mark(x), y),
             mark#(if(x, y, z)) -> mark#(x),
             mark#(if(x, y, z)) -> if_active#(mark(x), y, z),
        div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
       if_active#(true(), x, y) -> mark#(x),
      if_active#(false(), x, y) -> mark#(y)}
    Scc:
     {minus_active#(s(x), s(y)) -> minus_active#(x, y)}
    SCC:
     Strict:
      {ge_active#(s(x), s(y)) -> ge_active#(x, y)}
     Weak:
     {      minus_active(x, y) -> minus(x, y),
          minus_active(0(), y) -> 0(),
      minus_active(s(x), s(y)) -> minus_active(x, y),
                     mark(0()) -> 0(),
                    mark(s(x)) -> s(mark(x)),
             mark(minus(x, y)) -> minus_active(x, y),
                mark(ge(x, y)) -> ge_active(x, y),
               mark(div(x, y)) -> div_active(mark(x), y),
             mark(if(x, y, z)) -> if_active(mark(x), y, z),
               ge_active(x, y) -> ge(x, y),
             ge_active(x, 0()) -> true(),
          ge_active(0(), s(y)) -> false(),
         ge_active(s(x), s(y)) -> ge_active(x, y),
              div_active(x, y) -> div(x, y),
         div_active(0(), s(y)) -> 0(),
        div_active(s(x), s(y)) -> if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
            if_active(x, y, z) -> if(x, y, z),
       if_active(true(), x, y) -> mark(x),
      if_active(false(), x, y) -> mark(y)}
     SPSC:
      Simple Projection:
       pi(ge_active#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {              mark#(s(x)) -> mark#(x),
                mark#(div(x, y)) -> mark#(x),
                mark#(div(x, y)) -> div_active#(mark(x), y),
              mark#(if(x, y, z)) -> mark#(x),
              mark#(if(x, y, z)) -> if_active#(mark(x), y, z),
         div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
        if_active#(true(), x, y) -> mark#(x),
       if_active#(false(), x, y) -> mark#(y)}
     Weak:
     {      minus_active(x, y) -> minus(x, y),
          minus_active(0(), y) -> 0(),
      minus_active(s(x), s(y)) -> minus_active(x, y),
                     mark(0()) -> 0(),
                    mark(s(x)) -> s(mark(x)),
             mark(minus(x, y)) -> minus_active(x, y),
                mark(ge(x, y)) -> ge_active(x, y),
               mark(div(x, y)) -> div_active(mark(x), y),
             mark(if(x, y, z)) -> if_active(mark(x), y, z),
               ge_active(x, y) -> ge(x, y),
             ge_active(x, 0()) -> true(),
          ge_active(0(), s(y)) -> false(),
         ge_active(s(x), s(y)) -> ge_active(x, y),
              div_active(x, y) -> div(x, y),
         div_active(0(), s(y)) -> 0(),
        div_active(s(x), s(y)) -> if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
            if_active(x, y, z) -> if(x, y, z),
       if_active(true(), x, y) -> mark(x),
      if_active(false(), x, y) -> mark(y)}
     POLY:
      Argument Filtering:
       pi(if) = [0,1,2], pi(if_active#) = [1,2], pi(if_active) = [], pi(div) = 0, pi(div_active#) = [], pi(div_active) = [], pi(ge) = [], pi(false) = [], pi(minus) = [], pi(ge_active) = [], pi(true) = [], pi(s) = 0, pi(mark#) = 0, pi(mark) = [], pi(minus_active) = [], pi(0) = []
      Usable Rules:
       {}
      Interpretation:
       [if_active#](x0, x1) = x0 + x1,
       [div_active#] = 0,
       [if](x0, x1, x2) = x0 + x1 + x2 + 1,
       [minus] = 0,
       [0] = 0
      Strict:
       {              mark#(s(x)) -> mark#(x),
                 mark#(div(x, y)) -> mark#(x),
                 mark#(div(x, y)) -> div_active#(mark(x), y),
          div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
         if_active#(true(), x, y) -> mark#(x),
        if_active#(false(), x, y) -> mark#(y)}
      Weak:
       {      minus_active(x, y) -> minus(x, y),
            minus_active(0(), y) -> 0(),
        minus_active(s(x), s(y)) -> minus_active(x, y),
                       mark(0()) -> 0(),
                      mark(s(x)) -> s(mark(x)),
               mark(minus(x, y)) -> minus_active(x, y),
                  mark(ge(x, y)) -> ge_active(x, y),
                 mark(div(x, y)) -> div_active(mark(x), y),
               mark(if(x, y, z)) -> if_active(mark(x), y, z),
                 ge_active(x, y) -> ge(x, y),
               ge_active(x, 0()) -> true(),
            ge_active(0(), s(y)) -> false(),
           ge_active(s(x), s(y)) -> ge_active(x, y),
                div_active(x, y) -> div(x, y),
           div_active(0(), s(y)) -> 0(),
          div_active(s(x), s(y)) -> if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
              if_active(x, y, z) -> if(x, y, z),
         if_active(true(), x, y) -> mark(x),
        if_active(false(), x, y) -> mark(y)}
      EDG:
       {(if_active#(false(), x, y) -> mark#(y), mark#(div(x, y)) -> div_active#(mark(x), y))
        (if_active#(false(), x, y) -> mark#(y), mark#(div(x, y)) -> mark#(x))
        (if_active#(false(), x, y) -> mark#(y), mark#(s(x)) -> mark#(x))
        (mark#(div(x, y)) -> mark#(x), mark#(div(x, y)) -> div_active#(mark(x), y))
        (mark#(div(x, y)) -> mark#(x), mark#(div(x, y)) -> mark#(x))
        (mark#(div(x, y)) -> mark#(x), mark#(s(x)) -> mark#(x))
        (if_active#(true(), x, y) -> mark#(x), mark#(div(x, y)) -> div_active#(mark(x), y))
        (if_active#(true(), x, y) -> mark#(x), mark#(div(x, y)) -> mark#(x))
        (if_active#(true(), x, y) -> mark#(x), mark#(s(x)) -> mark#(x))
        (mark#(div(x, y)) -> div_active#(mark(x), y), div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()))
        (mark#(s(x)) -> mark#(x), mark#(s(x)) -> mark#(x))
        (mark#(s(x)) -> mark#(x), mark#(div(x, y)) -> mark#(x))
        (mark#(s(x)) -> mark#(x), mark#(div(x, y)) -> div_active#(mark(x), y))
        (div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()), if_active#(true(), x, y) -> mark#(x))
        (div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()), if_active#(false(), x, y) -> mark#(y))}
       SCCS:
        Scc:
         {              mark#(s(x)) -> mark#(x),
                   mark#(div(x, y)) -> mark#(x),
                   mark#(div(x, y)) -> div_active#(mark(x), y),
            div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
           if_active#(true(), x, y) -> mark#(x),
          if_active#(false(), x, y) -> mark#(y)}
        SCC:
         Strict:
          {              mark#(s(x)) -> mark#(x),
                    mark#(div(x, y)) -> mark#(x),
                    mark#(div(x, y)) -> div_active#(mark(x), y),
             div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
            if_active#(true(), x, y) -> mark#(x),
           if_active#(false(), x, y) -> mark#(y)}
         Weak:
         {      minus_active(x, y) -> minus(x, y),
              minus_active(0(), y) -> 0(),
          minus_active(s(x), s(y)) -> minus_active(x, y),
                         mark(0()) -> 0(),
                        mark(s(x)) -> s(mark(x)),
                 mark(minus(x, y)) -> minus_active(x, y),
                    mark(ge(x, y)) -> ge_active(x, y),
                   mark(div(x, y)) -> div_active(mark(x), y),
                 mark(if(x, y, z)) -> if_active(mark(x), y, z),
                   ge_active(x, y) -> ge(x, y),
                 ge_active(x, 0()) -> true(),
              ge_active(0(), s(y)) -> false(),
             ge_active(s(x), s(y)) -> ge_active(x, y),
                  div_active(x, y) -> div(x, y),
             div_active(0(), s(y)) -> 0(),
            div_active(s(x), s(y)) -> if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
                if_active(x, y, z) -> if(x, y, z),
           if_active(true(), x, y) -> mark(x),
          if_active(false(), x, y) -> mark(y)}
         POLY:
          Argument Filtering:
           pi(if) = [], pi(if_active#) = [1,2], pi(if_active) = [], pi(div) = [0], pi(div_active#) = [], pi(div_active) = [], pi(ge) = [], pi(false) = [], pi(minus) = [], pi(ge_active) = [], pi(true) = [], pi(s) = 0, pi(mark#) = 0, pi(mark) = [], pi(minus_active) = [], pi(0) = []
          Usable Rules:
           {}
          Interpretation:
           [if_active#](x0, x1) = x0 + x1,
           [div_active#] = 1,
           [div](x0) = x0 + 1,
           [minus] = 0,
           [0] = 0
          Strict:
           {              mark#(s(x)) -> mark#(x),
                     mark#(div(x, y)) -> div_active#(mark(x), y),
              div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
             if_active#(true(), x, y) -> mark#(x),
            if_active#(false(), x, y) -> mark#(y)}
          Weak:
           {      minus_active(x, y) -> minus(x, y),
                minus_active(0(), y) -> 0(),
            minus_active(s(x), s(y)) -> minus_active(x, y),
                           mark(0()) -> 0(),
                          mark(s(x)) -> s(mark(x)),
                   mark(minus(x, y)) -> minus_active(x, y),
                      mark(ge(x, y)) -> ge_active(x, y),
                     mark(div(x, y)) -> div_active(mark(x), y),
                   mark(if(x, y, z)) -> if_active(mark(x), y, z),
                     ge_active(x, y) -> ge(x, y),
                   ge_active(x, 0()) -> true(),
                ge_active(0(), s(y)) -> false(),
               ge_active(s(x), s(y)) -> ge_active(x, y),
                    div_active(x, y) -> div(x, y),
               div_active(0(), s(y)) -> 0(),
              div_active(s(x), s(y)) -> if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
                  if_active(x, y, z) -> if(x, y, z),
             if_active(true(), x, y) -> mark(x),
            if_active(false(), x, y) -> mark(y)}
          EDG:
           {(mark#(s(x)) -> mark#(x), mark#(div(x, y)) -> div_active#(mark(x), y))
            (mark#(s(x)) -> mark#(x), mark#(s(x)) -> mark#(x))
            (mark#(div(x, y)) -> div_active#(mark(x), y), div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()))
            (div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()), if_active#(true(), x, y) -> mark#(x))
            (div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()), if_active#(false(), x, y) -> mark#(y))
            (if_active#(true(), x, y) -> mark#(x), mark#(s(x)) -> mark#(x))
            (if_active#(true(), x, y) -> mark#(x), mark#(div(x, y)) -> div_active#(mark(x), y))
            (if_active#(false(), x, y) -> mark#(y), mark#(s(x)) -> mark#(x))
            (if_active#(false(), x, y) -> mark#(y), mark#(div(x, y)) -> div_active#(mark(x), y))}
           SCCS:
            Scc:
             {              mark#(s(x)) -> mark#(x),
                       mark#(div(x, y)) -> div_active#(mark(x), y),
                div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
               if_active#(true(), x, y) -> mark#(x),
              if_active#(false(), x, y) -> mark#(y)}
            SCC:
             Strict:
              {              mark#(s(x)) -> mark#(x),
                        mark#(div(x, y)) -> div_active#(mark(x), y),
                 div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
                if_active#(true(), x, y) -> mark#(x),
               if_active#(false(), x, y) -> mark#(y)}
             Weak:
             {      minus_active(x, y) -> minus(x, y),
                  minus_active(0(), y) -> 0(),
              minus_active(s(x), s(y)) -> minus_active(x, y),
                             mark(0()) -> 0(),
                            mark(s(x)) -> s(mark(x)),
                     mark(minus(x, y)) -> minus_active(x, y),
                        mark(ge(x, y)) -> ge_active(x, y),
                       mark(div(x, y)) -> div_active(mark(x), y),
                     mark(if(x, y, z)) -> if_active(mark(x), y, z),
                       ge_active(x, y) -> ge(x, y),
                     ge_active(x, 0()) -> true(),
                  ge_active(0(), s(y)) -> false(),
                 ge_active(s(x), s(y)) -> ge_active(x, y),
                      div_active(x, y) -> div(x, y),
                 div_active(0(), s(y)) -> 0(),
                div_active(s(x), s(y)) -> if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
                    if_active(x, y, z) -> if(x, y, z),
               if_active(true(), x, y) -> mark(x),
              if_active(false(), x, y) -> mark(y)}
             POLY:
              Argument Filtering:
               pi(if) = [1,2], pi(if_active#) = [1,2], pi(if_active) = [1,2], pi(div) = [0], pi(div_active#) = [0], pi(div_active) = [0], pi(ge) = [], pi(false) = [], pi(minus) = [], pi(ge_active) = [], pi(true) = [], pi(s) = [0], pi(mark#) = 0, pi(mark) = 0, pi(minus_active) = [], pi(0) = []
              Usable Rules:
               {}
              Interpretation:
               [if_active#](x0, x1) = x0 + x1,
               [div_active#](x0) = x0 + 1,
               [div](x0) = x0 + 1,
               [minus] = 0,
               [s](x0) = x0 + 1,
               [0] = 0
              Strict:
               {         mark#(div(x, y)) -> div_active#(mark(x), y),
                  div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
                 if_active#(true(), x, y) -> mark#(x),
                if_active#(false(), x, y) -> mark#(y)}
              Weak:
               {      minus_active(x, y) -> minus(x, y),
                    minus_active(0(), y) -> 0(),
                minus_active(s(x), s(y)) -> minus_active(x, y),
                               mark(0()) -> 0(),
                              mark(s(x)) -> s(mark(x)),
                       mark(minus(x, y)) -> minus_active(x, y),
                          mark(ge(x, y)) -> ge_active(x, y),
                         mark(div(x, y)) -> div_active(mark(x), y),
                       mark(if(x, y, z)) -> if_active(mark(x), y, z),
                         ge_active(x, y) -> ge(x, y),
                       ge_active(x, 0()) -> true(),
                    ge_active(0(), s(y)) -> false(),
                   ge_active(s(x), s(y)) -> ge_active(x, y),
                        div_active(x, y) -> div(x, y),
                   div_active(0(), s(y)) -> 0(),
                  div_active(s(x), s(y)) -> if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
                      if_active(x, y, z) -> if(x, y, z),
                 if_active(true(), x, y) -> mark(x),
                if_active(false(), x, y) -> mark(y)}
              EDG:
               {(mark#(div(x, y)) -> div_active#(mark(x), y), div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()))
                (div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()), if_active#(false(), x, y) -> mark#(y))
                (div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()), if_active#(true(), x, y) -> mark#(x))
                (if_active#(true(), x, y) -> mark#(x), mark#(div(x, y)) -> div_active#(mark(x), y))
                (if_active#(false(), x, y) -> mark#(y), mark#(div(x, y)) -> div_active#(mark(x), y))}
               SCCS:
                Scc:
                 {         mark#(div(x, y)) -> div_active#(mark(x), y),
                    div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
                   if_active#(true(), x, y) -> mark#(x),
                  if_active#(false(), x, y) -> mark#(y)}
                SCC:
                 Strict:
                  {         mark#(div(x, y)) -> div_active#(mark(x), y),
                     div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
                    if_active#(true(), x, y) -> mark#(x),
                   if_active#(false(), x, y) -> mark#(y)}
                 Weak:
                 {      minus_active(x, y) -> minus(x, y),
                      minus_active(0(), y) -> 0(),
                  minus_active(s(x), s(y)) -> minus_active(x, y),
                                 mark(0()) -> 0(),
                                mark(s(x)) -> s(mark(x)),
                         mark(minus(x, y)) -> minus_active(x, y),
                            mark(ge(x, y)) -> ge_active(x, y),
                           mark(div(x, y)) -> div_active(mark(x), y),
                         mark(if(x, y, z)) -> if_active(mark(x), y, z),
                           ge_active(x, y) -> ge(x, y),
                         ge_active(x, 0()) -> true(),
                      ge_active(0(), s(y)) -> false(),
                     ge_active(s(x), s(y)) -> ge_active(x, y),
                          div_active(x, y) -> div(x, y),
                     div_active(0(), s(y)) -> 0(),
                    div_active(s(x), s(y)) -> if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
                        if_active(x, y, z) -> if(x, y, z),
                   if_active(true(), x, y) -> mark(x),
                  if_active(false(), x, y) -> mark(y)}
                 POLY:
                  Argument Filtering:
                   pi(if) = [], pi(if_active#) = [1,2], pi(if_active) = [], pi(div) = [], pi(div_active#) = [], pi(div_active) = [], pi(ge) = [], pi(false) = [], pi(minus) = [], pi(ge_active) = [], pi(true) = [], pi(s) = [], pi(mark#) = 0, pi(mark) = [], pi(minus_active) = [], pi(0) = []
                  Usable Rules:
                   {}
                  Interpretation:
                   [if_active#](x0, x1) = x0 + x1,
                   [div_active#] = 0,
                   [div] = 1,
                   [s] = 0,
                   [0] = 0
                  Strict:
                   {  div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
                     if_active#(true(), x, y) -> mark#(x),
                    if_active#(false(), x, y) -> mark#(y)}
                  Weak:
                   {      minus_active(x, y) -> minus(x, y),
                        minus_active(0(), y) -> 0(),
                    minus_active(s(x), s(y)) -> minus_active(x, y),
                                   mark(0()) -> 0(),
                                  mark(s(x)) -> s(mark(x)),
                           mark(minus(x, y)) -> minus_active(x, y),
                              mark(ge(x, y)) -> ge_active(x, y),
                             mark(div(x, y)) -> div_active(mark(x), y),
                           mark(if(x, y, z)) -> if_active(mark(x), y, z),
                             ge_active(x, y) -> ge(x, y),
                           ge_active(x, 0()) -> true(),
                        ge_active(0(), s(y)) -> false(),
                       ge_active(s(x), s(y)) -> ge_active(x, y),
                            div_active(x, y) -> div(x, y),
                       div_active(0(), s(y)) -> 0(),
                      div_active(s(x), s(y)) -> if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
                          if_active(x, y, z) -> if(x, y, z),
                     if_active(true(), x, y) -> mark(x),
                    if_active(false(), x, y) -> mark(y)}
                  EDG:
                   {(div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()), if_active#(true(), x, y) -> mark#(x))
                    (div_active#(s(x), s(y)) -> if_active#(ge_active(x, y), s(div(minus(x, y), s(y))), 0()), if_active#(false(), x, y) -> mark#(y))}
                   SCCS:
                    
                    Qed
    SCC:
     Strict:
      {minus_active#(s(x), s(y)) -> minus_active#(x, y)}
     Weak:
     {      minus_active(x, y) -> minus(x, y),
          minus_active(0(), y) -> 0(),
      minus_active(s(x), s(y)) -> minus_active(x, y),
                     mark(0()) -> 0(),
                    mark(s(x)) -> s(mark(x)),
             mark(minus(x, y)) -> minus_active(x, y),
                mark(ge(x, y)) -> ge_active(x, y),
               mark(div(x, y)) -> div_active(mark(x), y),
             mark(if(x, y, z)) -> if_active(mark(x), y, z),
               ge_active(x, y) -> ge(x, y),
             ge_active(x, 0()) -> true(),
          ge_active(0(), s(y)) -> false(),
         ge_active(s(x), s(y)) -> ge_active(x, y),
              div_active(x, y) -> div(x, y),
         div_active(0(), s(y)) -> 0(),
        div_active(s(x), s(y)) -> if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0()),
            if_active(x, y, z) -> if(x, y, z),
       if_active(true(), x, y) -> mark(x),
      if_active(false(), x, y) -> mark(y)}
     SPSC:
      Simple Projection:
       pi(minus_active#) = 0
      Strict:
       {}
      Qed