MAYBE
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),
    if(true(), x, y) -> s(div(minus(x, y), y)),
   if(false(), x, y) -> 0()}
 DP:
  Strict:
   { 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),
     if#(true(), x, y) -> minus#(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),
     if(true(), x, y) -> s(div(minus(x, y), y)),
    if(false(), x, y) -> 0()}
  EDG:
   {(ge#(s(x), 0()) -> ge#(x, 0()), ge#(s(x), 0()) -> ge#(x, 0()))
    (minus#(s(x), 0()) -> minus#(x, 0()), minus#(s(x), 0()) -> minus#(x, 0()))
    (plus#(s(x), y) -> plus#(x, y), plus#(s(x), y) -> plus#(x, y))
    (plus#(s(x), y) -> plus#(x, y), plus#(0(), s(x)) -> plus#(0(), x))
    (if#(true(), x, y) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y))
    (if#(true(), x, y) -> minus#(x, y), minus#(s(x), 0()) -> minus#(x, 0()))
    (if#(true(), x, y) -> minus#(x, y), minus#(0(), s(x)) -> minus#(0(), x))
    (div#(x, y) -> ify#(ge(y, s(0())), x, y), ify#(true(), x, y) -> if#(ge(x, y), x, y))
    (div#(x, y) -> ify#(ge(y, s(0())), x, y), ify#(true(), x, y) -> ge#(x, y))
    (minus#(0(), s(x)) -> minus#(0(), x), minus#(0(), s(x)) -> minus#(0(), x))
    (ge#(0(), s(s(x))) -> ge#(0(), s(x)), ge#(0(), s(s(x))) -> ge#(0(), s(x)))
    (plus#(0(), s(x)) -> plus#(0(), x), plus#(0(), s(x)) -> plus#(0(), x))
    (if#(true(), x, y) -> div#(minus(x, y), y), 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))
    (ify#(true(), x, y) -> if#(ge(x, y), x, y), if#(true(), x, y) -> minus#(x, y))
    (ify#(true(), x, y) -> if#(ge(x, y), x, y), if#(true(), x, y) -> div#(minus(x, y), y))
    (ify#(true(), x, y) -> ge#(x, y), ge#(0(), s(s(x))) -> ge#(0(), s(x)))
    (ify#(true(), x, y) -> ge#(x, y), ge#(s(x), 0()) -> ge#(x, 0()))
    (ify#(true(), x, y) -> ge#(x, y), ge#(s(x), s(y)) -> ge#(x, y))
    (minus#(s(x), s(y)) -> minus#(x, y), minus#(0(), s(x)) -> minus#(0(), x))
    (minus#(s(x), s(y)) -> minus#(x, y), minus#(s(x), 0()) -> minus#(x, 0()))
    (minus#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(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#(x, y) -> ge#(y, s(0())), ge#(s(x), s(y)) -> ge#(x, y))}
   SCCS:
    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:
     {plus#(s(x), y) -> plus#(x, y)}
    Scc:
     {plus#(0(), s(x)) -> plus#(0(), x)}
    Scc:
     {minus#(s(x), s(y)) -> minus#(x, y)}
    Scc:
     {minus#(s(x), 0()) -> minus#(x, 0())}
    Scc:
     {minus#(0(), s(x)) -> minus#(0(), x)}
    Scc:
     {ge#(s(x), s(y)) -> ge#(x, y)}
    Scc:
     {ge#(s(x), 0()) -> ge#(x, 0())}
    Scc:
     {ge#(0(), s(s(x))) -> ge#(0(), s(x))}
    SCC:
     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),
        if(true(), x, y) -> s(div(minus(x, y), y)),
       if(false(), x, y) -> 0()}
     Fail
    SCC:
     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),
        if(true(), x, y) -> s(div(minus(x, y), y)),
       if(false(), x, y) -> 0()}
     SPSC:
      Simple Projection:
       pi(plus#) = 0
      Strict:
       {}
      Qed
    SCC:
     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),
        if(true(), x, y) -> s(div(minus(x, y), y)),
       if(false(), x, y) -> 0()}
     SPSC:
      Simple Projection:
       pi(plus#) = 1
      Strict:
       {}
      Qed
    SCC:
     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),
        if(true(), x, y) -> s(div(minus(x, y), y)),
       if(false(), x, y) -> 0()}
     SPSC:
      Simple Projection:
       pi(minus#) = 0
      Strict:
       {}
      Qed
    SCC:
     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),
        if(true(), x, y) -> s(div(minus(x, y), y)),
       if(false(), x, y) -> 0()}
     SPSC:
      Simple Projection:
       pi(minus#) = 0
      Strict:
       {}
      Qed
    SCC:
     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),
        if(true(), x, y) -> s(div(minus(x, y), y)),
       if(false(), x, y) -> 0()}
     SPSC:
      Simple Projection:
       pi(minus#) = 1
      Strict:
       {}
      Qed
    SCC:
     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),
        if(true(), x, y) -> s(div(minus(x, y), y)),
       if(false(), x, y) -> 0()}
     SPSC:
      Simple Projection:
       pi(ge#) = 0
      Strict:
       {}
      Qed
    SCC:
     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),
        if(true(), x, y) -> s(div(minus(x, y), y)),
       if(false(), x, y) -> 0()}
     SPSC:
      Simple Projection:
       pi(ge#) = 0
      Strict:
       {}
      Qed
    SCC:
     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),
        if(true(), x, y) -> s(div(minus(x, y), y)),
       if(false(), x, y) -> 0()}
     SPSC:
      Simple Projection:
       pi(ge#) = 1
      Strict:
       {}
      Qed