MAYBE
Time: 0.015352
TRS:
 {      ge(0(), 0()) -> true(),
      ge(0(), s 0()) -> false(),
      ge(0(), s s x) -> ge(0(), s x),
        ge(s x, 0()) -> ge(x, 0()),
        ge(s x, s y) -> ge(x, y),
     minus(0(), 0()) -> 0(),
     minus(0(), s x) -> minus(0(), x),
     minus(s x, 0()) -> s minus(x, 0()),
     minus(s x, s y) -> minus(x, y),
      plus(0(), 0()) -> 0(),
      plus(0(), s x) -> s plus(0(), x),
        plus(s x, y) -> s plus(x, y),
   ify(true(), x, y) -> if(ge(x, y), x, y),
  ify(false(), x, y) -> divByZeroError(),
           div(x, y) -> ify(ge(y, s 0()), x, y),
  div(plus(x, y), z) -> plus(div(x, z), div(y, z)),
    if(true(), x, y) -> s div(minus(x, y), y),
   if(false(), x, y) -> 0()}
 DP:
  DP:
   {    ge#(0(), s s x) -> ge#(0(), s x),
          ge#(s x, 0()) -> ge#(x, 0()),
          ge#(s x, s y) -> ge#(x, y),
       minus#(0(), s x) -> minus#(0(), x),
       minus#(s x, 0()) -> minus#(x, 0()),
       minus#(s x, s y) -> minus#(x, y),
        plus#(0(), s x) -> plus#(0(), x),
          plus#(s x, y) -> plus#(x, y),
     ify#(true(), x, y) -> ge#(x, y),
     ify#(true(), x, y) -> if#(ge(x, y), x, y),
             div#(x, y) -> ge#(y, s 0()),
             div#(x, y) -> ify#(ge(y, s 0()), x, y),
    div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)),
    div#(plus(x, y), z) -> div#(x, z),
    div#(plus(x, y), z) -> div#(y, z),
      if#(true(), x, y) -> minus#(x, y),
      if#(true(), x, y) -> div#(minus(x, y), y)}
  TRS:
  {      ge(0(), 0()) -> true(),
       ge(0(), s 0()) -> false(),
       ge(0(), s s x) -> ge(0(), s x),
         ge(s x, 0()) -> ge(x, 0()),
         ge(s x, s y) -> ge(x, y),
      minus(0(), 0()) -> 0(),
      minus(0(), s x) -> minus(0(), x),
      minus(s x, 0()) -> s minus(x, 0()),
      minus(s x, s y) -> minus(x, y),
       plus(0(), 0()) -> 0(),
       plus(0(), s x) -> s plus(0(), x),
         plus(s x, y) -> s plus(x, y),
    ify(true(), x, y) -> if(ge(x, y), x, y),
   ify(false(), x, y) -> divByZeroError(),
            div(x, y) -> ify(ge(y, s 0()), x, y),
   div(plus(x, y), z) -> plus(div(x, z), div(y, z)),
     if(true(), x, y) -> s div(minus(x, y), y),
    if(false(), x, y) -> 0()}
  EDG:
   {(plus#(0(), s x) -> plus#(0(), x), plus#(0(), s x) -> plus#(0(), x))
    (ify#(true(), x, y) -> if#(ge(x, y), x, y), if#(true(), x, y) -> div#(minus(x, y), y))
    (ify#(true(), x, y) -> if#(ge(x, y), x, y), if#(true(), x, y) -> minus#(x, y))
    (ge#(s x, 0()) -> ge#(x, 0()), ge#(s x, 0()) -> ge#(x, 0()))
    (div#(plus(x, y), z) -> div#(x, z), div#(plus(x, y), z) -> div#(y, z))
    (div#(plus(x, y), z) -> div#(x, z), div#(plus(x, y), z) -> div#(x, z))
    (div#(plus(x, y), z) -> div#(x, z), div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)))
    (div#(plus(x, y), z) -> div#(x, z), div#(x, y) -> ify#(ge(y, s 0()), x, y))
    (div#(plus(x, y), z) -> div#(x, z), div#(x, y) -> ge#(y, s 0()))
    (if#(true(), x, y) -> div#(minus(x, y), y), div#(plus(x, y), z) -> div#(y, z))
    (if#(true(), x, y) -> div#(minus(x, y), y), div#(plus(x, y), z) -> div#(x, z))
    (if#(true(), x, y) -> div#(minus(x, y), y), div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)))
    (if#(true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> ify#(ge(y, s 0()), x, y))
    (if#(true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> ge#(y, s 0()))
    (div#(x, y) -> ge#(y, s 0()), ge#(s x, s y) -> ge#(x, y))
    (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (minus#(s x, s y) -> minus#(x, y), minus#(s x, 0()) -> minus#(x, 0()))
    (minus#(s x, s y) -> minus#(x, y), minus#(0(), s x) -> minus#(0(), x))
    (ify#(true(), x, y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
    (ify#(true(), x, y) -> ge#(x, y), ge#(s x, 0()) -> ge#(x, 0()))
    (ify#(true(), x, y) -> ge#(x, y), ge#(0(), s s x) -> ge#(0(), s x))
    (if#(true(), x, y) -> minus#(x, y), minus#(0(), s x) -> minus#(0(), x))
    (if#(true(), x, y) -> minus#(x, y), minus#(s x, 0()) -> minus#(x, 0()))
    (if#(true(), x, y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (plus#(s x, y) -> plus#(x, y), plus#(0(), s x) -> plus#(0(), x))
    (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
    (ge#(s x, s y) -> ge#(x, y), ge#(0(), s s x) -> ge#(0(), s x))
    (ge#(s x, s y) -> ge#(x, y), ge#(s x, 0()) -> ge#(x, 0()))
    (ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
    (div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)), plus#(0(), s x) -> plus#(0(), x))
    (div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)), plus#(s x, y) -> plus#(x, y))
    (div#(plus(x, y), z) -> div#(y, z), div#(x, y) -> ge#(y, s 0()))
    (div#(plus(x, y), z) -> div#(y, z), div#(x, y) -> ify#(ge(y, s 0()), x, y))
    (div#(plus(x, y), z) -> div#(y, z), div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)))
    (div#(plus(x, y), z) -> div#(y, z), div#(plus(x, y), z) -> div#(x, z))
    (div#(plus(x, y), z) -> div#(y, z), div#(plus(x, y), z) -> div#(y, z))
    (minus#(s x, 0()) -> minus#(x, 0()), minus#(s x, 0()) -> minus#(x, 0()))
    (div#(x, y) -> ify#(ge(y, s 0()), x, y), ify#(true(), x, y) -> ge#(x, y))
    (div#(x, y) -> ify#(ge(y, s 0()), x, y), ify#(true(), x, y) -> if#(ge(x, y), x, y))
    (ge#(0(), s s x) -> ge#(0(), s x), ge#(0(), s s x) -> ge#(0(), s x))
    (minus#(0(), s x) -> minus#(0(), x), minus#(0(), s x) -> minus#(0(), x))}
   EDG:
    {(plus#(0(), s x) -> plus#(0(), x), plus#(0(), s x) -> plus#(0(), x))
     (ify#(true(), x, y) -> if#(ge(x, y), x, y), if#(true(), x, y) -> div#(minus(x, y), y))
     (ify#(true(), x, y) -> if#(ge(x, y), x, y), if#(true(), x, y) -> minus#(x, y))
     (ge#(s x, 0()) -> ge#(x, 0()), ge#(s x, 0()) -> ge#(x, 0()))
     (div#(plus(x, y), z) -> div#(x, z), div#(plus(x, y), z) -> div#(y, z))
     (div#(plus(x, y), z) -> div#(x, z), div#(plus(x, y), z) -> div#(x, z))
     (div#(plus(x, y), z) -> div#(x, z), div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)))
     (div#(plus(x, y), z) -> div#(x, z), div#(x, y) -> ify#(ge(y, s 0()), x, y))
     (div#(plus(x, y), z) -> div#(x, z), div#(x, y) -> ge#(y, s 0()))
     (if#(true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> ify#(ge(y, s 0()), x, y))
     (if#(true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> ge#(y, s 0()))
     (div#(x, y) -> ge#(y, s 0()), ge#(s x, s y) -> ge#(x, y))
     (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (minus#(s x, s y) -> minus#(x, y), minus#(s x, 0()) -> minus#(x, 0()))
     (minus#(s x, s y) -> minus#(x, y), minus#(0(), s x) -> minus#(0(), x))
     (ify#(true(), x, y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
     (ify#(true(), x, y) -> ge#(x, y), ge#(s x, 0()) -> ge#(x, 0()))
     (ify#(true(), x, y) -> ge#(x, y), ge#(0(), s s x) -> ge#(0(), s x))
     (if#(true(), x, y) -> minus#(x, y), minus#(0(), s x) -> minus#(0(), x))
     (if#(true(), x, y) -> minus#(x, y), minus#(s x, 0()) -> minus#(x, 0()))
     (if#(true(), x, y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (plus#(s x, y) -> plus#(x, y), plus#(0(), s x) -> plus#(0(), x))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
     (ge#(s x, s y) -> ge#(x, y), ge#(0(), s s x) -> ge#(0(), s x))
     (ge#(s x, s y) -> ge#(x, y), ge#(s x, 0()) -> ge#(x, 0()))
     (ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
     (div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)), plus#(0(), s x) -> plus#(0(), x))
     (div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)), plus#(s x, y) -> plus#(x, y))
     (div#(plus(x, y), z) -> div#(y, z), div#(x, y) -> ge#(y, s 0()))
     (div#(plus(x, y), z) -> div#(y, z), div#(x, y) -> ify#(ge(y, s 0()), x, y))
     (div#(plus(x, y), z) -> div#(y, z), div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)))
     (div#(plus(x, y), z) -> div#(y, z), div#(plus(x, y), z) -> div#(x, z))
     (div#(plus(x, y), z) -> div#(y, z), div#(plus(x, y), z) -> div#(y, z))
     (minus#(s x, 0()) -> minus#(x, 0()), minus#(s x, 0()) -> minus#(x, 0()))
     (div#(x, y) -> ify#(ge(y, s 0()), x, y), ify#(true(), x, y) -> ge#(x, y))
     (div#(x, y) -> ify#(ge(y, s 0()), x, y), ify#(true(), x, y) -> if#(ge(x, y), x, y))
     (ge#(0(), s s x) -> ge#(0(), s x), ge#(0(), s s x) -> ge#(0(), s x))
     (minus#(0(), s x) -> minus#(0(), x), minus#(0(), s x) -> minus#(0(), x))}
    EDG:
     {(plus#(0(), s x) -> plus#(0(), x), plus#(0(), s x) -> plus#(0(), x))
      (ify#(true(), x, y) -> if#(ge(x, y), x, y), if#(true(), x, y) -> div#(minus(x, y), y))
      (ify#(true(), x, y) -> if#(ge(x, y), x, y), if#(true(), x, y) -> minus#(x, y))
      (ge#(s x, 0()) -> ge#(x, 0()), ge#(s x, 0()) -> ge#(x, 0()))
      (div#(plus(x, y), z) -> div#(x, z), div#(plus(x, y), z) -> div#(y, z))
      (div#(plus(x, y), z) -> div#(x, z), div#(plus(x, y), z) -> div#(x, z))
      (div#(plus(x, y), z) -> div#(x, z), div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)))
      (div#(plus(x, y), z) -> div#(x, z), div#(x, y) -> ify#(ge(y, s 0()), x, y))
      (div#(plus(x, y), z) -> div#(x, z), div#(x, y) -> ge#(y, s 0()))
      (if#(true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> ify#(ge(y, s 0()), x, y))
      (if#(true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> ge#(y, s 0()))
      (div#(x, y) -> ge#(y, s 0()), ge#(s x, s y) -> ge#(x, y))
      (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
      (minus#(s x, s y) -> minus#(x, y), minus#(s x, 0()) -> minus#(x, 0()))
      (minus#(s x, s y) -> minus#(x, y), minus#(0(), s x) -> minus#(0(), x))
      (ify#(true(), x, y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
      (ify#(true(), x, y) -> ge#(x, y), ge#(s x, 0()) -> ge#(x, 0()))
      (ify#(true(), x, y) -> ge#(x, y), ge#(0(), s s x) -> ge#(0(), s x))
      (if#(true(), x, y) -> minus#(x, y), minus#(0(), s x) -> minus#(0(), x))
      (if#(true(), x, y) -> minus#(x, y), minus#(s x, 0()) -> minus#(x, 0()))
      (if#(true(), x, y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
      (plus#(s x, y) -> plus#(x, y), plus#(0(), s x) -> plus#(0(), x))
      (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
      (ge#(s x, s y) -> ge#(x, y), ge#(0(), s s x) -> ge#(0(), s x))
      (ge#(s x, s y) -> ge#(x, y), ge#(s x, 0()) -> ge#(x, 0()))
      (ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
      (div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)), plus#(0(), s x) -> plus#(0(), x))
      (div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)), plus#(s x, y) -> plus#(x, y))
      (div#(plus(x, y), z) -> div#(y, z), div#(x, y) -> ge#(y, s 0()))
      (div#(plus(x, y), z) -> div#(y, z), div#(x, y) -> ify#(ge(y, s 0()), x, y))
      (div#(plus(x, y), z) -> div#(y, z), div#(plus(x, y), z) -> plus#(div(x, z), div(y, z)))
      (div#(plus(x, y), z) -> div#(y, z), div#(plus(x, y), z) -> div#(x, z))
      (div#(plus(x, y), z) -> div#(y, z), div#(plus(x, y), z) -> div#(y, z))
      (minus#(s x, 0()) -> minus#(x, 0()), minus#(s x, 0()) -> minus#(x, 0()))
      (div#(x, y) -> ify#(ge(y, s 0()), x, y), ify#(true(), x, y) -> ge#(x, y))
      (div#(x, y) -> ify#(ge(y, s 0()), x, y), ify#(true(), x, y) -> if#(ge(x, y), x, y))
      (ge#(0(), s s x) -> ge#(0(), s x), ge#(0(), s s x) -> ge#(0(), s x))
      (minus#(0(), s x) -> minus#(0(), x), minus#(0(), s x) -> minus#(0(), x))}
     STATUS:
      arrows: 0.868512
      SCCS (10):
       Scc:
        {div#(plus(x, y), z) -> div#(x, z),
         div#(plus(x, y), z) -> div#(y, z)}
       Scc:
        {plus#(s x, y) -> plus#(x, y)}
       Scc:
        {ify#(true(), x, y) -> if#(ge(x, y), x, y),
                 div#(x, y) -> ify#(ge(y, s 0()), x, y),
          if#(true(), x, y) -> div#(minus(x, y), y)}
       Scc:
        {ge#(s x, s y) -> ge#(x, y)}
       Scc:
        {ge#(s x, 0()) -> ge#(x, 0())}
       Scc:
        {minus#(s x, s y) -> minus#(x, y)}
       Scc:
        {minus#(s x, 0()) -> minus#(x, 0())}
       Scc:
        {ge#(0(), s s x) -> ge#(0(), s x)}
       Scc:
        {plus#(0(), s x) -> plus#(0(), x)}
       Scc:
        {minus#(0(), s x) -> minus#(0(), x)}
       
       SCC (2):
        Strict:
         {div#(plus(x, y), z) -> div#(x, z),
          div#(plus(x, y), z) -> div#(y, z)}
        Weak:
        {      ge(0(), 0()) -> true(),
             ge(0(), s 0()) -> false(),
             ge(0(), s s x) -> ge(0(), s x),
               ge(s x, 0()) -> ge(x, 0()),
               ge(s x, s y) -> ge(x, y),
            minus(0(), 0()) -> 0(),
            minus(0(), s x) -> minus(0(), x),
            minus(s x, 0()) -> s minus(x, 0()),
            minus(s x, s y) -> minus(x, y),
             plus(0(), 0()) -> 0(),
             plus(0(), s x) -> s plus(0(), x),
               plus(s x, y) -> s plus(x, y),
          ify(true(), x, y) -> if(ge(x, y), x, y),
         ify(false(), x, y) -> divByZeroError(),
                  div(x, y) -> ify(ge(y, s 0()), x, y),
         div(plus(x, y), z) -> plus(div(x, z), div(y, z)),
           if(true(), x, y) -> s div(minus(x, y), y),
          if(false(), x, y) -> 0()}
        Open
       
       SCC (1):
        Strict:
         {plus#(s x, y) -> plus#(x, y)}
        Weak:
        {      ge(0(), 0()) -> true(),
             ge(0(), s 0()) -> false(),
             ge(0(), s s x) -> ge(0(), s x),
               ge(s x, 0()) -> ge(x, 0()),
               ge(s x, s y) -> ge(x, y),
            minus(0(), 0()) -> 0(),
            minus(0(), s x) -> minus(0(), x),
            minus(s x, 0()) -> s minus(x, 0()),
            minus(s x, s y) -> minus(x, y),
             plus(0(), 0()) -> 0(),
             plus(0(), s x) -> s plus(0(), x),
               plus(s x, y) -> s plus(x, y),
          ify(true(), x, y) -> if(ge(x, y), x, y),
         ify(false(), x, y) -> divByZeroError(),
                  div(x, y) -> ify(ge(y, s 0()), x, y),
         div(plus(x, y), z) -> plus(div(x, z), div(y, z)),
           if(true(), x, y) -> s div(minus(x, y), y),
          if(false(), x, y) -> 0()}
        Open
       SCC (3):
        Strict:
         {ify#(true(), x, y) -> if#(ge(x, y), x, y),
                  div#(x, y) -> ify#(ge(y, s 0()), x, y),
           if#(true(), x, y) -> div#(minus(x, y), y)}
        Weak:
        {      ge(0(), 0()) -> true(),
             ge(0(), s 0()) -> false(),
             ge(0(), s s x) -> ge(0(), s x),
               ge(s x, 0()) -> ge(x, 0()),
               ge(s x, s y) -> ge(x, y),
            minus(0(), 0()) -> 0(),
            minus(0(), s x) -> minus(0(), x),
            minus(s x, 0()) -> s minus(x, 0()),
            minus(s x, s y) -> minus(x, y),
             plus(0(), 0()) -> 0(),
             plus(0(), s x) -> s plus(0(), x),
               plus(s x, y) -> s plus(x, y),
          ify(true(), x, y) -> if(ge(x, y), x, y),
         ify(false(), x, y) -> divByZeroError(),
                  div(x, y) -> ify(ge(y, s 0()), x, y),
         div(plus(x, y), z) -> plus(div(x, z), div(y, z)),
           if(true(), x, y) -> s div(minus(x, y), y),
          if(false(), x, y) -> 0()}
        Open
       
       
       SCC (1):
        Strict:
         {ge#(s x, s y) -> ge#(x, y)}
        Weak:
        {      ge(0(), 0()) -> true(),
             ge(0(), s 0()) -> false(),
             ge(0(), s s x) -> ge(0(), s x),
               ge(s x, 0()) -> ge(x, 0()),
               ge(s x, s y) -> ge(x, y),
            minus(0(), 0()) -> 0(),
            minus(0(), s x) -> minus(0(), x),
            minus(s x, 0()) -> s minus(x, 0()),
            minus(s x, s y) -> minus(x, y),
             plus(0(), 0()) -> 0(),
             plus(0(), s x) -> s plus(0(), x),
               plus(s x, y) -> s plus(x, y),
          ify(true(), x, y) -> if(ge(x, y), x, y),
         ify(false(), x, y) -> divByZeroError(),
                  div(x, y) -> ify(ge(y, s 0()), x, y),
         div(plus(x, y), z) -> plus(div(x, z), div(y, z)),
           if(true(), x, y) -> s div(minus(x, y), y),
          if(false(), x, y) -> 0()}
        Open
       SCC (1):
        Strict:
         {ge#(s x, 0()) -> ge#(x, 0())}
        Weak:
        {      ge(0(), 0()) -> true(),
             ge(0(), s 0()) -> false(),
             ge(0(), s s x) -> ge(0(), s x),
               ge(s x, 0()) -> ge(x, 0()),
               ge(s x, s y) -> ge(x, y),
            minus(0(), 0()) -> 0(),
            minus(0(), s x) -> minus(0(), x),
            minus(s x, 0()) -> s minus(x, 0()),
            minus(s x, s y) -> minus(x, y),
             plus(0(), 0()) -> 0(),
             plus(0(), s x) -> s plus(0(), x),
               plus(s x, y) -> s plus(x, y),
          ify(true(), x, y) -> if(ge(x, y), x, y),
         ify(false(), x, y) -> divByZeroError(),
                  div(x, y) -> ify(ge(y, s 0()), x, y),
         div(plus(x, y), z) -> plus(div(x, z), div(y, z)),
           if(true(), x, y) -> s div(minus(x, y), y),
          if(false(), x, y) -> 0()}
        Open
       
       SCC (1):
        Strict:
         {minus#(s x, s y) -> minus#(x, y)}
        Weak:
        {      ge(0(), 0()) -> true(),
             ge(0(), s 0()) -> false(),
             ge(0(), s s x) -> ge(0(), s x),
               ge(s x, 0()) -> ge(x, 0()),
               ge(s x, s y) -> ge(x, y),
            minus(0(), 0()) -> 0(),
            minus(0(), s x) -> minus(0(), x),
            minus(s x, 0()) -> s minus(x, 0()),
            minus(s x, s y) -> minus(x, y),
             plus(0(), 0()) -> 0(),
             plus(0(), s x) -> s plus(0(), x),
               plus(s x, y) -> s plus(x, y),
          ify(true(), x, y) -> if(ge(x, y), x, y),
         ify(false(), x, y) -> divByZeroError(),
                  div(x, y) -> ify(ge(y, s 0()), x, y),
         div(plus(x, y), z) -> plus(div(x, z), div(y, z)),
           if(true(), x, y) -> s div(minus(x, y), y),
          if(false(), x, y) -> 0()}
        Open
       SCC (1):
        Strict:
         {minus#(s x, 0()) -> minus#(x, 0())}
        Weak:
        {      ge(0(), 0()) -> true(),
             ge(0(), s 0()) -> false(),
             ge(0(), s s x) -> ge(0(), s x),
               ge(s x, 0()) -> ge(x, 0()),
               ge(s x, s y) -> ge(x, y),
            minus(0(), 0()) -> 0(),
            minus(0(), s x) -> minus(0(), x),
            minus(s x, 0()) -> s minus(x, 0()),
            minus(s x, s y) -> minus(x, y),
             plus(0(), 0()) -> 0(),
             plus(0(), s x) -> s plus(0(), x),
               plus(s x, y) -> s plus(x, y),
          ify(true(), x, y) -> if(ge(x, y), x, y),
         ify(false(), x, y) -> divByZeroError(),
                  div(x, y) -> ify(ge(y, s 0()), x, y),
         div(plus(x, y), z) -> plus(div(x, z), div(y, z)),
           if(true(), x, y) -> s div(minus(x, y), y),
          if(false(), x, y) -> 0()}
        Open
       SCC (1):
        Strict:
         {ge#(0(), s s x) -> ge#(0(), s x)}
        Weak:
        {      ge(0(), 0()) -> true(),
             ge(0(), s 0()) -> false(),
             ge(0(), s s x) -> ge(0(), s x),
               ge(s x, 0()) -> ge(x, 0()),
               ge(s x, s y) -> ge(x, y),
            minus(0(), 0()) -> 0(),
            minus(0(), s x) -> minus(0(), x),
            minus(s x, 0()) -> s minus(x, 0()),
            minus(s x, s y) -> minus(x, y),
             plus(0(), 0()) -> 0(),
             plus(0(), s x) -> s plus(0(), x),
               plus(s x, y) -> s plus(x, y),
          ify(true(), x, y) -> if(ge(x, y), x, y),
         ify(false(), x, y) -> divByZeroError(),
                  div(x, y) -> ify(ge(y, s 0()), x, y),
         div(plus(x, y), z) -> plus(div(x, z), div(y, z)),
           if(true(), x, y) -> s div(minus(x, y), y),
          if(false(), x, y) -> 0()}
        Open
       SCC (1):
        Strict:
         {plus#(0(), s x) -> plus#(0(), x)}
        Weak:
        {      ge(0(), 0()) -> true(),
             ge(0(), s 0()) -> false(),
             ge(0(), s s x) -> ge(0(), s x),
               ge(s x, 0()) -> ge(x, 0()),
               ge(s x, s y) -> ge(x, y),
            minus(0(), 0()) -> 0(),
            minus(0(), s x) -> minus(0(), x),
            minus(s x, 0()) -> s minus(x, 0()),
            minus(s x, s y) -> minus(x, y),
             plus(0(), 0()) -> 0(),
             plus(0(), s x) -> s plus(0(), x),
               plus(s x, y) -> s plus(x, y),
          ify(true(), x, y) -> if(ge(x, y), x, y),
         ify(false(), x, y) -> divByZeroError(),
                  div(x, y) -> ify(ge(y, s 0()), x, y),
         div(plus(x, y), z) -> plus(div(x, z), div(y, z)),
           if(true(), x, y) -> s div(minus(x, y), y),
          if(false(), x, y) -> 0()}
        Open
       SCC (1):
        Strict:
         {minus#(0(), s x) -> minus#(0(), x)}
        Weak:
        {      ge(0(), 0()) -> true(),
             ge(0(), s 0()) -> false(),
             ge(0(), s s x) -> ge(0(), s x),
               ge(s x, 0()) -> ge(x, 0()),
               ge(s x, s y) -> ge(x, y),
            minus(0(), 0()) -> 0(),
            minus(0(), s x) -> minus(0(), x),
            minus(s x, 0()) -> s minus(x, 0()),
            minus(s x, s y) -> minus(x, y),
             plus(0(), 0()) -> 0(),
             plus(0(), s x) -> s plus(0(), x),
               plus(s x, y) -> s plus(x, y),
          ify(true(), x, y) -> if(ge(x, y), x, y),
         ify(false(), x, y) -> divByZeroError(),
                  div(x, y) -> ify(ge(y, s 0()), x, y),
         div(plus(x, y), z) -> plus(div(x, z), div(y, z)),
           if(true(), x, y) -> s div(minus(x, y), y),
          if(false(), x, y) -> 0()}
        Open