Time: 4.939250
TRS:
 {               halfExp(b, e, r) -> condLoop(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r),
           mult_int(pos x, pos y) -> pos mult_nat(x, y),
           mult_int(pos x, neg y) -> neg mult_nat(x, y),
           mult_int(neg x, pos y) -> neg mult_nat(x, y),
           mult_int(neg x, neg y) -> pos mult_nat(x, y),
                  sqBase(b, e, r) -> halfExp(mult_int(b, b), e, r),
         condMod(true(), b, e, r) -> sqBase(b, e, mult_int(r, b)),
        condMod(false(), b, e, r) -> sqBase(b, e, r),
        condLoop(true(), b, e, r) -> condMod(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r),
       condLoop(false(), b, e, r) -> r,
    greater_int(pos 0(), pos 0()) -> false(),
    greater_int(pos 0(), pos s y) -> false(),
    greater_int(pos 0(), neg 0()) -> false(),
    greater_int(pos 0(), neg s y) -> true(),
    greater_int(pos s x, pos 0()) -> true(),
    greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
    greater_int(pos s x, neg 0()) -> true(),
    greater_int(pos s x, neg s y) -> true(),
    greater_int(neg 0(), pos 0()) -> false(),
    greater_int(neg 0(), pos s y) -> false(),
    greater_int(neg 0(), neg 0()) -> false(),
    greater_int(neg 0(), neg s y) -> true(),
    greater_int(neg s x, pos 0()) -> false(),
    greater_int(neg s x, pos s y) -> false(),
    greater_int(neg s x, neg 0()) -> false(),
    greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
          div_int(pos x, pos s y) -> pos div_nat(x, s y),
          div_int(pos x, neg s y) -> neg div_nat(x, s y),
          div_int(neg x, pos s y) -> neg div_nat(x, s y),
          div_int(neg x, neg s y) -> pos div_nat(x, s y),
                        pow(b, e) -> condLoop(greater_int(e, pos 0()), b, e, pos s 0()),
      equal_int(pos 0(), pos 0()) -> true(),
      equal_int(pos 0(), pos s y) -> false(),
      equal_int(pos 0(), neg 0()) -> true(),
      equal_int(pos 0(), neg s y) -> false(),
      equal_int(pos s x, pos 0()) -> false(),
      equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
      equal_int(pos s x, neg 0()) -> false(),
      equal_int(pos s x, neg s y) -> false(),
      equal_int(neg 0(), pos 0()) -> true(),
      equal_int(neg 0(), pos s y) -> false(),
      equal_int(neg 0(), neg 0()) -> true(),
      equal_int(neg 0(), neg s y) -> false(),
      equal_int(neg s x, pos 0()) -> false(),
      equal_int(neg s x, pos s y) -> false(),
      equal_int(neg s x, neg 0()) -> false(),
      equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
            mod_int(pos x, pos y) -> pos mod_nat(x, y),
            mod_int(pos x, neg y) -> pos mod_nat(x, y),
            mod_int(neg x, pos y) -> neg mod_nat(x, y),
            mod_int(neg x, neg y) -> neg mod_nat(x, y),
                 mult_nat(0(), y) -> 0(),
               mult_nat(s x, 0()) -> 0(),
               mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                 plus_nat(0(), x) -> x,
                 plus_nat(s x, y) -> s plus_nat(x, y),
                div_nat(0(), s y) -> 0(),
                div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                 if(true(), x, y) -> x,
                if(false(), x, y) -> y,
    greatereq_int(pos x, pos 0()) -> true(),
      greatereq_int(pos x, neg y) -> true(),
  greatereq_int(pos 0(), pos s y) -> false(),
  greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
    greatereq_int(neg x, pos s y) -> false(),
  greatereq_int(neg 0(), pos 0()) -> true(),
    greatereq_int(neg 0(), neg y) -> true(),
  greatereq_int(neg s x, pos 0()) -> false(),
  greatereq_int(neg s x, neg 0()) -> false(),
  greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
              minus_nat_s(x, 0()) -> x,
            minus_nat_s(0(), s y) -> 0(),
            minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                mod_nat(0(), s x) -> 0(),
                mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x)}
 SRS: We consider a TRS.
  Trs:
   {               halfExp(b, e, r) -> condLoop(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r),
             mult_int(pos x, pos y) -> pos mult_nat(x, y),
             mult_int(pos x, neg y) -> neg mult_nat(x, y),
             mult_int(neg x, pos y) -> neg mult_nat(x, y),
             mult_int(neg x, neg y) -> pos mult_nat(x, y),
                    sqBase(b, e, r) -> halfExp(mult_int(b, b), e, r),
           condMod(true(), b, e, r) -> sqBase(b, e, mult_int(r, b)),
          condMod(false(), b, e, r) -> sqBase(b, e, r),
          condLoop(true(), b, e, r) -> condMod(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r),
         condLoop(false(), b, e, r) -> r,
      greater_int(pos 0(), pos 0()) -> false(),
      greater_int(pos 0(), pos s y) -> false(),
      greater_int(pos 0(), neg 0()) -> false(),
      greater_int(pos 0(), neg s y) -> true(),
      greater_int(pos s x, pos 0()) -> true(),
      greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
      greater_int(pos s x, neg 0()) -> true(),
      greater_int(pos s x, neg s y) -> true(),
      greater_int(neg 0(), pos 0()) -> false(),
      greater_int(neg 0(), pos s y) -> false(),
      greater_int(neg 0(), neg 0()) -> false(),
      greater_int(neg 0(), neg s y) -> true(),
      greater_int(neg s x, pos 0()) -> false(),
      greater_int(neg s x, pos s y) -> false(),
      greater_int(neg s x, neg 0()) -> false(),
      greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
            div_int(pos x, pos s y) -> pos div_nat(x, s y),
            div_int(pos x, neg s y) -> neg div_nat(x, s y),
            div_int(neg x, pos s y) -> neg div_nat(x, s y),
            div_int(neg x, neg s y) -> pos div_nat(x, s y),
                          pow(b, e) -> condLoop(greater_int(e, pos 0()), b, e, pos s 0()),
        equal_int(pos 0(), pos 0()) -> true(),
        equal_int(pos 0(), pos s y) -> false(),
        equal_int(pos 0(), neg 0()) -> true(),
        equal_int(pos 0(), neg s y) -> false(),
        equal_int(pos s x, pos 0()) -> false(),
        equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
        equal_int(pos s x, neg 0()) -> false(),
        equal_int(pos s x, neg s y) -> false(),
        equal_int(neg 0(), pos 0()) -> true(),
        equal_int(neg 0(), pos s y) -> false(),
        equal_int(neg 0(), neg 0()) -> true(),
        equal_int(neg 0(), neg s y) -> false(),
        equal_int(neg s x, pos 0()) -> false(),
        equal_int(neg s x, pos s y) -> false(),
        equal_int(neg s x, neg 0()) -> false(),
        equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
              mod_int(pos x, pos y) -> pos mod_nat(x, y),
              mod_int(pos x, neg y) -> pos mod_nat(x, y),
              mod_int(neg x, pos y) -> neg mod_nat(x, y),
              mod_int(neg x, neg y) -> neg mod_nat(x, y),
                   mult_nat(0(), y) -> 0(),
                 mult_nat(s x, 0()) -> 0(),
                 mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                   plus_nat(0(), x) -> x,
                   plus_nat(s x, y) -> s plus_nat(x, y),
                  div_nat(0(), s y) -> 0(),
                  div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                   if(true(), x, y) -> x,
                  if(false(), x, y) -> y,
      greatereq_int(pos x, pos 0()) -> true(),
        greatereq_int(pos x, neg y) -> true(),
    greatereq_int(pos 0(), pos s y) -> false(),
    greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
      greatereq_int(neg x, pos s y) -> false(),
    greatereq_int(neg 0(), pos 0()) -> true(),
      greatereq_int(neg 0(), neg y) -> true(),
    greatereq_int(neg s x, pos 0()) -> false(),
    greatereq_int(neg s x, neg 0()) -> false(),
    greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
                minus_nat_s(x, 0()) -> x,
              minus_nat_s(0(), s y) -> 0(),
              minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                  mod_nat(0(), s x) -> 0(),
                  mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x)}
  APP: We consider a non-applicative system.
   Trs:
    {               halfExp(b, e, r) -> condLoop(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r),
              mult_int(pos x, pos y) -> pos mult_nat(x, y),
              mult_int(pos x, neg y) -> neg mult_nat(x, y),
              mult_int(neg x, pos y) -> neg mult_nat(x, y),
              mult_int(neg x, neg y) -> pos mult_nat(x, y),
                     sqBase(b, e, r) -> halfExp(mult_int(b, b), e, r),
            condMod(true(), b, e, r) -> sqBase(b, e, mult_int(r, b)),
           condMod(false(), b, e, r) -> sqBase(b, e, r),
           condLoop(true(), b, e, r) -> condMod(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r),
          condLoop(false(), b, e, r) -> r,
       greater_int(pos 0(), pos 0()) -> false(),
       greater_int(pos 0(), pos s y) -> false(),
       greater_int(pos 0(), neg 0()) -> false(),
       greater_int(pos 0(), neg s y) -> true(),
       greater_int(pos s x, pos 0()) -> true(),
       greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
       greater_int(pos s x, neg 0()) -> true(),
       greater_int(pos s x, neg s y) -> true(),
       greater_int(neg 0(), pos 0()) -> false(),
       greater_int(neg 0(), pos s y) -> false(),
       greater_int(neg 0(), neg 0()) -> false(),
       greater_int(neg 0(), neg s y) -> true(),
       greater_int(neg s x, pos 0()) -> false(),
       greater_int(neg s x, pos s y) -> false(),
       greater_int(neg s x, neg 0()) -> false(),
       greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
             div_int(pos x, pos s y) -> pos div_nat(x, s y),
             div_int(pos x, neg s y) -> neg div_nat(x, s y),
             div_int(neg x, pos s y) -> neg div_nat(x, s y),
             div_int(neg x, neg s y) -> pos div_nat(x, s y),
                           pow(b, e) -> condLoop(greater_int(e, pos 0()), b, e, pos s 0()),
         equal_int(pos 0(), pos 0()) -> true(),
         equal_int(pos 0(), pos s y) -> false(),
         equal_int(pos 0(), neg 0()) -> true(),
         equal_int(pos 0(), neg s y) -> false(),
         equal_int(pos s x, pos 0()) -> false(),
         equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
         equal_int(pos s x, neg 0()) -> false(),
         equal_int(pos s x, neg s y) -> false(),
         equal_int(neg 0(), pos 0()) -> true(),
         equal_int(neg 0(), pos s y) -> false(),
         equal_int(neg 0(), neg 0()) -> true(),
         equal_int(neg 0(), neg s y) -> false(),
         equal_int(neg s x, pos 0()) -> false(),
         equal_int(neg s x, pos s y) -> false(),
         equal_int(neg s x, neg 0()) -> false(),
         equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
               mod_int(pos x, pos y) -> pos mod_nat(x, y),
               mod_int(pos x, neg y) -> pos mod_nat(x, y),
               mod_int(neg x, pos y) -> neg mod_nat(x, y),
               mod_int(neg x, neg y) -> neg mod_nat(x, y),
                    mult_nat(0(), y) -> 0(),
                  mult_nat(s x, 0()) -> 0(),
                  mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                    plus_nat(0(), x) -> x,
                    plus_nat(s x, y) -> s plus_nat(x, y),
                   div_nat(0(), s y) -> 0(),
                   div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                    if(true(), x, y) -> x,
                   if(false(), x, y) -> y,
       greatereq_int(pos x, pos 0()) -> true(),
         greatereq_int(pos x, neg y) -> true(),
     greatereq_int(pos 0(), pos s y) -> false(),
     greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
       greatereq_int(neg x, pos s y) -> false(),
     greatereq_int(neg 0(), pos 0()) -> true(),
       greatereq_int(neg 0(), neg y) -> true(),
     greatereq_int(neg s x, pos 0()) -> false(),
     greatereq_int(neg s x, neg 0()) -> false(),
     greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
                 minus_nat_s(x, 0()) -> x,
               minus_nat_s(0(), s y) -> 0(),
               minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                   mod_nat(0(), s x) -> 0(),
                   mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x)}
   REWRITE:
    Strict:
     {               halfExp(b, e, r) -> condLoop(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r),
               mult_int(pos x, pos y) -> pos mult_nat(x, y),
               mult_int(pos x, neg y) -> neg mult_nat(x, y),
               mult_int(neg x, pos y) -> neg mult_nat(x, y),
               mult_int(neg x, neg y) -> pos mult_nat(x, y),
                      sqBase(b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
             condMod(true(), b, e, r) -> sqBase(b, e, mult_int(r, b)),
            condMod(false(), b, e, r) -> sqBase(b, e, r),
            condLoop(true(), b, e, r) -> condMod(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r),
           condLoop(false(), b, e, r) -> r,
        greater_int(pos 0(), pos 0()) -> false(),
        greater_int(pos 0(), pos s y) -> false(),
        greater_int(pos 0(), neg 0()) -> false(),
        greater_int(pos 0(), neg s y) -> true(),
        greater_int(pos s x, pos 0()) -> true(),
        greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
        greater_int(pos s x, neg 0()) -> true(),
        greater_int(pos s x, neg s y) -> true(),
        greater_int(neg 0(), pos 0()) -> false(),
        greater_int(neg 0(), pos s y) -> false(),
        greater_int(neg 0(), neg 0()) -> false(),
        greater_int(neg 0(), neg s y) -> true(),
        greater_int(neg s x, pos 0()) -> false(),
        greater_int(neg s x, pos s y) -> false(),
        greater_int(neg s x, neg 0()) -> false(),
        greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
              div_int(pos x, pos s y) -> pos div_nat(x, s y),
              div_int(pos x, neg s y) -> neg div_nat(x, s y),
              div_int(neg x, pos s y) -> neg div_nat(x, s y),
              div_int(neg x, neg s y) -> pos div_nat(x, s y),
                            pow(b, e) -> condLoop(greater_int(e, pos 0()), b, e, pos s 0()),
          equal_int(pos 0(), pos 0()) -> true(),
          equal_int(pos 0(), pos s y) -> false(),
          equal_int(pos 0(), neg 0()) -> true(),
          equal_int(pos 0(), neg s y) -> false(),
          equal_int(pos s x, pos 0()) -> false(),
          equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
          equal_int(pos s x, neg 0()) -> false(),
          equal_int(pos s x, neg s y) -> false(),
          equal_int(neg 0(), pos 0()) -> true(),
          equal_int(neg 0(), pos s y) -> false(),
          equal_int(neg 0(), neg 0()) -> true(),
          equal_int(neg 0(), neg s y) -> false(),
          equal_int(neg s x, pos 0()) -> false(),
          equal_int(neg s x, pos s y) -> false(),
          equal_int(neg s x, neg 0()) -> false(),
          equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
                mod_int(pos x, pos y) -> pos mod_nat(x, y),
                mod_int(pos x, neg y) -> pos mod_nat(x, y),
                mod_int(neg x, pos y) -> neg mod_nat(x, y),
                mod_int(neg x, neg y) -> neg mod_nat(x, y),
                     mult_nat(0(), y) -> 0(),
                   mult_nat(s x, 0()) -> 0(),
                   mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                     plus_nat(0(), x) -> x,
                     plus_nat(s x, y) -> s plus_nat(x, y),
                    div_nat(0(), s y) -> 0(),
                    div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                     if(true(), x, y) -> x,
                    if(false(), x, y) -> y,
        greatereq_int(pos x, pos 0()) -> true(),
          greatereq_int(pos x, neg y) -> true(),
      greatereq_int(pos 0(), pos s y) -> false(),
      greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
        greatereq_int(neg x, pos s y) -> false(),
      greatereq_int(neg 0(), pos 0()) -> true(),
        greatereq_int(neg 0(), neg y) -> true(),
      greatereq_int(neg s x, pos 0()) -> false(),
      greatereq_int(neg s x, neg 0()) -> false(),
      greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
                  minus_nat_s(x, 0()) -> x,
                minus_nat_s(0(), s y) -> 0(),
                minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                    mod_nat(0(), s x) -> 0(),
                    mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x)}
    Weak:
    {}
    REWRITE:
     Strict:
      {               halfExp(b, e, r) -> condLoop(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r),
                mult_int(pos x, pos y) -> pos mult_nat(x, y),
                mult_int(pos x, neg y) -> neg mult_nat(x, y),
                mult_int(neg x, pos y) -> neg mult_nat(x, y),
                mult_int(neg x, neg y) -> pos mult_nat(x, y),
                       sqBase(b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
              condMod(true(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)),
             condMod(false(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
             condLoop(true(), b, e, r) -> condMod(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r),
            condLoop(false(), b, e, r) -> r,
         greater_int(pos 0(), pos 0()) -> false(),
         greater_int(pos 0(), pos s y) -> false(),
         greater_int(pos 0(), neg 0()) -> false(),
         greater_int(pos 0(), neg s y) -> true(),
         greater_int(pos s x, pos 0()) -> true(),
         greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
         greater_int(pos s x, neg 0()) -> true(),
         greater_int(pos s x, neg s y) -> true(),
         greater_int(neg 0(), pos 0()) -> false(),
         greater_int(neg 0(), pos s y) -> false(),
         greater_int(neg 0(), neg 0()) -> false(),
         greater_int(neg 0(), neg s y) -> true(),
         greater_int(neg s x, pos 0()) -> false(),
         greater_int(neg s x, pos s y) -> false(),
         greater_int(neg s x, neg 0()) -> false(),
         greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
               div_int(pos x, pos s y) -> pos div_nat(x, s y),
               div_int(pos x, neg s y) -> neg div_nat(x, s y),
               div_int(neg x, pos s y) -> neg div_nat(x, s y),
               div_int(neg x, neg s y) -> pos div_nat(x, s y),
                             pow(b, e) -> condLoop(greater_int(e, pos 0()), b, e, pos s 0()),
           equal_int(pos 0(), pos 0()) -> true(),
           equal_int(pos 0(), pos s y) -> false(),
           equal_int(pos 0(), neg 0()) -> true(),
           equal_int(pos 0(), neg s y) -> false(),
           equal_int(pos s x, pos 0()) -> false(),
           equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
           equal_int(pos s x, neg 0()) -> false(),
           equal_int(pos s x, neg s y) -> false(),
           equal_int(neg 0(), pos 0()) -> true(),
           equal_int(neg 0(), pos s y) -> false(),
           equal_int(neg 0(), neg 0()) -> true(),
           equal_int(neg 0(), neg s y) -> false(),
           equal_int(neg s x, pos 0()) -> false(),
           equal_int(neg s x, pos s y) -> false(),
           equal_int(neg s x, neg 0()) -> false(),
           equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
                 mod_int(pos x, pos y) -> pos mod_nat(x, y),
                 mod_int(pos x, neg y) -> pos mod_nat(x, y),
                 mod_int(neg x, pos y) -> neg mod_nat(x, y),
                 mod_int(neg x, neg y) -> neg mod_nat(x, y),
                      mult_nat(0(), y) -> 0(),
                    mult_nat(s x, 0()) -> 0(),
                    mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                      plus_nat(0(), x) -> x,
                      plus_nat(s x, y) -> s plus_nat(x, y),
                     div_nat(0(), s y) -> 0(),
                     div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                      if(true(), x, y) -> x,
                     if(false(), x, y) -> y,
         greatereq_int(pos x, pos 0()) -> true(),
           greatereq_int(pos x, neg y) -> true(),
       greatereq_int(pos 0(), pos s y) -> false(),
       greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
         greatereq_int(neg x, pos s y) -> false(),
       greatereq_int(neg 0(), pos 0()) -> true(),
         greatereq_int(neg 0(), neg y) -> true(),
       greatereq_int(neg s x, pos 0()) -> false(),
       greatereq_int(neg s x, neg 0()) -> false(),
       greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
                   minus_nat_s(x, 0()) -> x,
                 minus_nat_s(0(), s y) -> 0(),
                 minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                     mod_nat(0(), s x) -> 0(),
                     mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x)}
     Weak:
     {}
     DP:
      DP:
       {         halfExp#(b, e, r) -> condLoop#(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r),
                 halfExp#(b, e, r) -> greater_int#(e, pos 0()),
                 halfExp#(b, e, r) -> div_int#(e, pos s s 0()),
            mult_int#(pos x, pos y) -> mult_nat#(x, y),
            mult_int#(pos x, neg y) -> mult_nat#(x, y),
            mult_int#(neg x, pos y) -> mult_nat#(x, y),
            mult_int#(neg x, neg y) -> mult_nat#(x, y),
                 sqBase#(b, e, r) -> mult_int#(b, b),
                 sqBase#(b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                 sqBase#(b, e, r) -> greater_int#(e, pos 0()),
                 sqBase#(b, e, r) -> div_int#(e, pos s s 0()),
         condMod#(true(), b, e, r) -> mult_int#(b, b),
         condMod#(true(), b, e, r) -> mult_int#(r, b),
         condMod#(true(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)),
         condMod#(true(), b, e, r) -> greater_int#(e, pos 0()),
         condMod#(true(), b, e, r) -> div_int#(e, pos s s 0()),
        condMod#(false(), b, e, r) -> mult_int#(b, b),
        condMod#(false(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
        condMod#(false(), b, e, r) -> greater_int#(e, pos 0()),
        condMod#(false(), b, e, r) -> div_int#(e, pos s s 0()),
         condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r),
         condLoop#(true(), b, e, r) -> equal_int#(mod_int(e, pos s s 0()), pos s 0()),
         condLoop#(true(), b, e, r) -> mod_int#(e, pos s s 0()),
        greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y),
        greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y),
          div_int#(pos x, pos s y) -> div_nat#(x, s y),
          div_int#(pos x, neg s y) -> div_nat#(x, s y),
          div_int#(neg x, pos s y) -> div_nat#(x, s y),
          div_int#(neg x, neg s y) -> div_nat#(x, s y),
                    pow#(b, e) -> condLoop#(greater_int(e, pos 0()), b, e, pos s 0()),
                    pow#(b, e) -> greater_int#(e, pos 0()),
        equal_int#(pos s x, pos s y) -> equal_int#(pos x, pos y),
        equal_int#(neg s x, neg s y) -> equal_int#(neg x, neg y),
            mod_int#(pos x, pos y) -> mod_nat#(x, y),
            mod_int#(pos x, neg y) -> mod_nat#(x, y),
            mod_int#(neg x, pos y) -> mod_nat#(x, y),
            mod_int#(neg x, neg y) -> mod_nat#(x, y),
                mult_nat#(s x, s y) -> mult_nat#(x, s y),
                mult_nat#(s x, s y) -> plus_nat#(mult_nat(x, s y), s y),
                  plus_nat#(s x, y) -> plus_nat#(x, y),
                div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y),
                div_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                div_nat#(s x, s y) -> greatereq_int#(pos x, pos y),
                div_nat#(s x, s y) -> minus_nat_s#(x, y),
        greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y),
        greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y),
                minus_nat_s#(s x, s y) -> minus_nat_s#(x, y),
                mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x),
                mod_nat#(s x, s y) -> greatereq_int#(pos x, pos y),
                mod_nat#(s x, s y) -> minus_nat_s#(x, y),
                mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y)}
      TRS:
      {               halfExp(b, e, r) -> condLoop(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r),
                mult_int(pos x, pos y) -> pos mult_nat(x, y),
                mult_int(pos x, neg y) -> neg mult_nat(x, y),
                mult_int(neg x, pos y) -> neg mult_nat(x, y),
                mult_int(neg x, neg y) -> pos mult_nat(x, y),
                       sqBase(b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
              condMod(true(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)),
             condMod(false(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
             condLoop(true(), b, e, r) -> condMod(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r),
            condLoop(false(), b, e, r) -> r,
         greater_int(pos 0(), pos 0()) -> false(),
         greater_int(pos 0(), pos s y) -> false(),
         greater_int(pos 0(), neg 0()) -> false(),
         greater_int(pos 0(), neg s y) -> true(),
         greater_int(pos s x, pos 0()) -> true(),
         greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
         greater_int(pos s x, neg 0()) -> true(),
         greater_int(pos s x, neg s y) -> true(),
         greater_int(neg 0(), pos 0()) -> false(),
         greater_int(neg 0(), pos s y) -> false(),
         greater_int(neg 0(), neg 0()) -> false(),
         greater_int(neg 0(), neg s y) -> true(),
         greater_int(neg s x, pos 0()) -> false(),
         greater_int(neg s x, pos s y) -> false(),
         greater_int(neg s x, neg 0()) -> false(),
         greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
               div_int(pos x, pos s y) -> pos div_nat(x, s y),
               div_int(pos x, neg s y) -> neg div_nat(x, s y),
               div_int(neg x, pos s y) -> neg div_nat(x, s y),
               div_int(neg x, neg s y) -> pos div_nat(x, s y),
                             pow(b, e) -> condLoop(greater_int(e, pos 0()), b, e, pos s 0()),
           equal_int(pos 0(), pos 0()) -> true(),
           equal_int(pos 0(), pos s y) -> false(),
           equal_int(pos 0(), neg 0()) -> true(),
           equal_int(pos 0(), neg s y) -> false(),
           equal_int(pos s x, pos 0()) -> false(),
           equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
           equal_int(pos s x, neg 0()) -> false(),
           equal_int(pos s x, neg s y) -> false(),
           equal_int(neg 0(), pos 0()) -> true(),
           equal_int(neg 0(), pos s y) -> false(),
           equal_int(neg 0(), neg 0()) -> true(),
           equal_int(neg 0(), neg s y) -> false(),
           equal_int(neg s x, pos 0()) -> false(),
           equal_int(neg s x, pos s y) -> false(),
           equal_int(neg s x, neg 0()) -> false(),
           equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
                 mod_int(pos x, pos y) -> pos mod_nat(x, y),
                 mod_int(pos x, neg y) -> pos mod_nat(x, y),
                 mod_int(neg x, pos y) -> neg mod_nat(x, y),
                 mod_int(neg x, neg y) -> neg mod_nat(x, y),
                      mult_nat(0(), y) -> 0(),
                    mult_nat(s x, 0()) -> 0(),
                    mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                      plus_nat(0(), x) -> x,
                      plus_nat(s x, y) -> s plus_nat(x, y),
                     div_nat(0(), s y) -> 0(),
                     div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                      if(true(), x, y) -> x,
                     if(false(), x, y) -> y,
         greatereq_int(pos x, pos 0()) -> true(),
           greatereq_int(pos x, neg y) -> true(),
       greatereq_int(pos 0(), pos s y) -> false(),
       greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
         greatereq_int(neg x, pos s y) -> false(),
       greatereq_int(neg 0(), pos 0()) -> true(),
         greatereq_int(neg 0(), neg y) -> true(),
       greatereq_int(neg s x, pos 0()) -> false(),
       greatereq_int(neg s x, neg 0()) -> false(),
       greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
                   minus_nat_s(x, 0()) -> x,
                 minus_nat_s(0(), s y) -> 0(),
                 minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                     mod_nat(0(), s x) -> 0(),
                     mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x)}
      EDG:
       {
        (mult_int#(pos x, neg y) -> mult_nat#(x, y), mult_nat#(s x, s y) -> plus_nat#(mult_nat(x, s y), s y))
        (mult_int#(pos x, neg y) -> mult_nat#(x, y), mult_nat#(s x, s y) -> mult_nat#(x, s y))
        (mult_int#(neg x, neg y) -> mult_nat#(x, y), mult_nat#(s x, s y) -> plus_nat#(mult_nat(x, s y), s y))
        (mult_int#(neg x, neg y) -> mult_nat#(x, y), mult_nat#(s x, s y) -> mult_nat#(x, s y))
        (mod_int#(pos x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y))
        (mod_int#(pos x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> minus_nat_s#(x, y))
        (mod_int#(pos x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> greatereq_int#(pos x, pos y))
        (mod_int#(pos x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x))
        (mod_int#(neg x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y))
        (mod_int#(neg x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> minus_nat_s#(x, y))
        (mod_int#(neg x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> greatereq_int#(pos x, pos y))
        (mod_int#(neg x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x))
        (div_nat#(s x, s y) -> minus_nat_s#(x, y), minus_nat_s#(s x, s y) -> minus_nat_s#(x, y))
        (mod_nat#(s x, s y) -> minus_nat_s#(x, y), minus_nat_s#(s x, s y) -> minus_nat_s#(x, y))
        (condMod#(true(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)), condLoop#(true(), b, e, r) -> mod_int#(e, pos s s 0()))
        (condMod#(true(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)), condLoop#(true(), b, e, r) -> equal_int#(mod_int(e, pos s s 0()), pos s 0()))
        (condMod#(true(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)), condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r))
        (condMod#(true(), b, e, r) -> mult_int#(b, b), mult_int#(neg x, neg y) -> mult_nat#(x, y))
        (condMod#(true(), b, e, r) -> mult_int#(b, b), mult_int#(neg x, pos y) -> mult_nat#(x, y))
        (condMod#(true(), b, e, r) -> mult_int#(b, b), mult_int#(pos x, neg y) -> mult_nat#(x, y))
        (condMod#(true(), b, e, r) -> mult_int#(b, b), mult_int#(pos x, pos y) -> mult_nat#(x, y))
        (condMod#(false(), b, e, r) -> mult_int#(b, b), mult_int#(neg x, neg y) -> mult_nat#(x, y))
        (condMod#(false(), b, e, r) -> mult_int#(b, b), mult_int#(neg x, pos y) -> mult_nat#(x, y))
        (condMod#(false(), b, e, r) -> mult_int#(b, b), mult_int#(pos x, neg y) -> mult_nat#(x, y))
        (condMod#(false(), b, e, r) -> mult_int#(b, b), mult_int#(pos x, pos y) -> mult_nat#(x, y))
        (sqBase#(b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r), condLoop#(true(), b, e, r) -> mod_int#(e, pos s s 0()))
        (sqBase#(b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r), condLoop#(true(), b, e, r) -> equal_int#(mod_int(e, pos s s 0()), pos s 0()))
        (sqBase#(b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r), condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r))
        (condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r), condMod#(false(), b, e, r) -> div_int#(e, pos s s 0()))
        (condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r), condMod#(false(), b, e, r) -> greater_int#(e, pos 0()))
        (condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r), condMod#(false(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r))
        (condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r), condMod#(false(), b, e, r) -> mult_int#(b, b))
        (condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r), condMod#(true(), b, e, r) -> div_int#(e, pos s s 0()))
        (condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r), condMod#(true(), b, e, r) -> greater_int#(e, pos 0()))
        (condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r), condMod#(true(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)))
        (condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r), condMod#(true(), b, e, r) -> mult_int#(r, b))
        (condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r), condMod#(true(), b, e, r) -> mult_int#(b, b))
        (greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
        (greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
        (div_int#(pos x, neg s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> minus_nat_s#(x, y))
        (div_int#(pos x, neg s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> greatereq_int#(pos x, pos y))
        (div_int#(pos x, neg s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()))
        (div_int#(pos x, neg s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y))
        (div_int#(neg x, neg s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> minus_nat_s#(x, y))
        (div_int#(neg x, neg s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> greatereq_int#(pos x, pos y))
        (div_int#(neg x, neg s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()))
        (div_int#(neg x, neg s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y))
        (equal_int#(neg s x, neg s y) -> equal_int#(neg x, neg y), equal_int#(neg s x, neg s y) -> equal_int#(neg x, neg y))
        (equal_int#(neg s x, neg s y) -> equal_int#(neg x, neg y), equal_int#(pos s x, pos s y) -> equal_int#(pos x, pos y))
        (mult_nat#(s x, s y) -> plus_nat#(mult_nat(x, s y), s y), plus_nat#(s x, y) -> plus_nat#(x, y))
        (div_nat#(s x, s y) -> greatereq_int#(pos x, pos y), greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y))
        (div_nat#(s x, s y) -> greatereq_int#(pos x, pos y), greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y))
        (greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y), greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y))
        (greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y), greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y))
        (mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y), mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y))
        (mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y), mod_nat#(s x, s y) -> minus_nat_s#(x, y))
        (mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y), mod_nat#(s x, s y) -> greatereq_int#(pos x, pos y))
        (mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y), mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x))
        (halfExp#(b, e, r) -> div_int#(e, pos s s 0()), div_int#(neg x, neg s y) -> div_nat#(x, s y))
        (halfExp#(b, e, r) -> div_int#(e, pos s s 0()), div_int#(neg x, pos s y) -> div_nat#(x, s y))
        (halfExp#(b, e, r) -> div_int#(e, pos s s 0()), div_int#(pos x, neg s y) -> div_nat#(x, s y))
        (halfExp#(b, e, r) -> div_int#(e, pos s s 0()), div_int#(pos x, pos s y) -> div_nat#(x, s y))
        (sqBase#(b, e, r) -> div_int#(e, pos s s 0()), div_int#(neg x, neg s y) -> div_nat#(x, s y))
        (sqBase#(b, e, r) -> div_int#(e, pos s s 0()), div_int#(neg x, pos s y) -> div_nat#(x, s y))
        (sqBase#(b, e, r) -> div_int#(e, pos s s 0()), div_int#(pos x, neg s y) -> div_nat#(x, s y))
        (sqBase#(b, e, r) -> div_int#(e, pos s s 0()), div_int#(pos x, pos s y) -> div_nat#(x, s y))
        (condMod#(true(), b, e, r) -> div_int#(e, pos s s 0()), div_int#(neg x, neg s y) -> div_nat#(x, s y))
        (condMod#(true(), b, e, r) -> div_int#(e, pos s s 0()), div_int#(neg x, pos s y) -> div_nat#(x, s y))
        (condMod#(true(), b, e, r) -> div_int#(e, pos s s 0()), div_int#(pos x, neg s y) -> div_nat#(x, s y))
        (condMod#(true(), b, e, r) -> div_int#(e, pos s s 0()), div_int#(pos x, pos s y) -> div_nat#(x, s y))
        (condMod#(false(), b, e, r) -> div_int#(e, pos s s 0()), div_int#(neg x, neg s y) -> div_nat#(x, s y))
        (condMod#(false(), b, e, r) -> div_int#(e, pos s s 0()), div_int#(neg x, pos s y) -> div_nat#(x, s y))
        (condMod#(false(), b, e, r) -> div_int#(e, pos s s 0()), div_int#(pos x, neg s y) -> div_nat#(x, s y))
        (condMod#(false(), b, e, r) -> div_int#(e, pos s s 0()), div_int#(pos x, pos s y) -> div_nat#(x, s y))
        (condLoop#(true(), b, e, r) -> mod_int#(e, pos s s 0()), mod_int#(neg x, neg y) -> mod_nat#(x, y))
        (condLoop#(true(), b, e, r) -> mod_int#(e, pos s s 0()), mod_int#(neg x, pos y) -> mod_nat#(x, y))
        (condLoop#(true(), b, e, r) -> mod_int#(e, pos s s 0()), mod_int#(pos x, neg y) -> mod_nat#(x, y))
        (condLoop#(true(), b, e, r) -> mod_int#(e, pos s s 0()), mod_int#(pos x, pos y) -> mod_nat#(x, y))
        (pow#(b, e) -> greater_int#(e, pos 0()), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
        (pow#(b, e) -> greater_int#(e, pos 0()), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
        (condLoop#(true(), b, e, r) -> equal_int#(mod_int(e, pos s s 0()), pos s 0()), equal_int#(pos s x, pos s y) -> equal_int#(pos x, pos y))
        (condLoop#(true(), b, e, r) -> equal_int#(mod_int(e, pos s s 0()), pos s 0()), equal_int#(neg s x, neg s y) -> equal_int#(neg x, neg y))
        (condMod#(false(), b, e, r) -> greater_int#(e, pos 0()), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
        (condMod#(false(), b, e, r) -> greater_int#(e, pos 0()), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
        (condMod#(true(), b, e, r) -> greater_int#(e, pos 0()), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
        (condMod#(true(), b, e, r) -> greater_int#(e, pos 0()), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
        (sqBase#(b, e, r) -> greater_int#(e, pos 0()), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
        (sqBase#(b, e, r) -> greater_int#(e, pos 0()), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
        (halfExp#(b, e, r) -> greater_int#(e, pos 0()), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
        (halfExp#(b, e, r) -> greater_int#(e, pos 0()), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
        (mod_nat#(s x, s y) -> greatereq_int#(pos x, pos y), greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y))
        (mod_nat#(s x, s y) -> greatereq_int#(pos x, pos y), greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y))
        (greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y), greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y))
        (greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y), greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y))
        (div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y), div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y))
        (div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y), div_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()))
        (div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y), div_nat#(s x, s y) -> greatereq_int#(pos x, pos y))
        (div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y), div_nat#(s x, s y) -> minus_nat_s#(x, y))
        (mult_nat#(s x, s y) -> mult_nat#(x, s y), mult_nat#(s x, s y) -> mult_nat#(x, s y))
        (mult_nat#(s x, s y) -> mult_nat#(x, s y), mult_nat#(s x, s y) -> plus_nat#(mult_nat(x, s y), s y))
        (equal_int#(pos s x, pos s y) -> equal_int#(pos x, pos y), equal_int#(pos s x, pos s y) -> equal_int#(pos x, pos y))
        (equal_int#(pos s x, pos s y) -> equal_int#(pos x, pos y), equal_int#(neg s x, neg s y) -> equal_int#(neg x, neg y))
        (div_int#(neg x, pos s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y))
        (div_int#(neg x, pos s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()))
        (div_int#(neg x, pos s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> greatereq_int#(pos x, pos y))
        (div_int#(neg x, pos s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> minus_nat_s#(x, y))
        (div_int#(pos x, pos s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y))
        (div_int#(pos x, pos s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()))
        (div_int#(pos x, pos s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> greatereq_int#(pos x, pos y))
        (div_int#(pos x, pos s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> minus_nat_s#(x, y))
        (greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
        (greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
        (condMod#(false(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r), condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r))
        (condMod#(false(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r), condLoop#(true(), b, e, r) -> equal_int#(mod_int(e, pos s s 0()), pos s 0()))
        (condMod#(false(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r), condLoop#(true(), b, e, r) -> mod_int#(e, pos s s 0()))
        (halfExp#(b, e, r) -> condLoop#(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r), condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r))
        (halfExp#(b, e, r) -> condLoop#(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r), condLoop#(true(), b, e, r) -> equal_int#(mod_int(e, pos s s 0()), pos s 0()))
        (halfExp#(b, e, r) -> condLoop#(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r), condLoop#(true(), b, e, r) -> mod_int#(e, pos s s 0()))
        (condMod#(true(), b, e, r) -> mult_int#(r, b), mult_int#(pos x, pos y) -> mult_nat#(x, y))
        (condMod#(true(), b, e, r) -> mult_int#(r, b), mult_int#(pos x, neg y) -> mult_nat#(x, y))
        (condMod#(true(), b, e, r) -> mult_int#(r, b), mult_int#(neg x, pos y) -> mult_nat#(x, y))
        (condMod#(true(), b, e, r) -> mult_int#(r, b), mult_int#(neg x, neg y) -> mult_nat#(x, y))
        (sqBase#(b, e, r) -> mult_int#(b, b), mult_int#(pos x, pos y) -> mult_nat#(x, y))
        (sqBase#(b, e, r) -> mult_int#(b, b), mult_int#(pos x, neg y) -> mult_nat#(x, y))
        (sqBase#(b, e, r) -> mult_int#(b, b), mult_int#(neg x, pos y) -> mult_nat#(x, y))
        (sqBase#(b, e, r) -> mult_int#(b, b), mult_int#(neg x, neg y) -> mult_nat#(x, y))
        (pow#(b, e) -> condLoop#(greater_int(e, pos 0()), b, e, pos s 0()), condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r))
        (pow#(b, e) -> condLoop#(greater_int(e, pos 0()), b, e, pos s 0()), condLoop#(true(), b, e, r) -> equal_int#(mod_int(e, pos s s 0()), pos s 0()))
        (pow#(b, e) -> condLoop#(greater_int(e, pos 0()), b, e, pos s 0()), condLoop#(true(), b, e, r) -> mod_int#(e, pos s s 0()))
        (minus_nat_s#(s x, s y) -> minus_nat_s#(x, y), minus_nat_s#(s x, s y) -> minus_nat_s#(x, y))
        (plus_nat#(s x, y) -> plus_nat#(x, y), plus_nat#(s x, y) -> plus_nat#(x, y))
        (mod_int#(neg x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x))
        (mod_int#(neg x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> greatereq_int#(pos x, pos y))
        (mod_int#(neg x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> minus_nat_s#(x, y))
        (mod_int#(neg x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y))
        (mod_int#(pos x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x))
        (mod_int#(pos x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> greatereq_int#(pos x, pos y))
        (mod_int#(pos x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> minus_nat_s#(x, y))
        (mod_int#(pos x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y))
        (mult_int#(neg x, pos y) -> mult_nat#(x, y), mult_nat#(s x, s y) -> mult_nat#(x, s y))
        (mult_int#(neg x, pos y) -> mult_nat#(x, y), mult_nat#(s x, s y) -> plus_nat#(mult_nat(x, s y), s y))
        (mult_int#(pos x, pos y) -> mult_nat#(x, y), mult_nat#(s x, s y) -> mult_nat#(x, s y))
        (mult_int#(pos x, pos y) -> mult_nat#(x, y), mult_nat#(s x, s y) -> plus_nat#(mult_nat(x, s y), s y))
       }
       EDG:
        {
         (mult_int#(pos x, neg y) -> mult_nat#(x, y), mult_nat#(s x, s y) -> plus_nat#(mult_nat(x, s y), s y))
         (mult_int#(pos x, neg y) -> mult_nat#(x, y), mult_nat#(s x, s y) -> mult_nat#(x, s y))
         (mult_int#(neg x, neg y) -> mult_nat#(x, y), mult_nat#(s x, s y) -> plus_nat#(mult_nat(x, s y), s y))
         (mult_int#(neg x, neg y) -> mult_nat#(x, y), mult_nat#(s x, s y) -> mult_nat#(x, s y))
         (mod_int#(pos x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y))
         (mod_int#(pos x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> minus_nat_s#(x, y))
         (mod_int#(pos x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> greatereq_int#(pos x, pos y))
         (mod_int#(pos x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x))
         (mod_int#(neg x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y))
         (mod_int#(neg x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> minus_nat_s#(x, y))
         (mod_int#(neg x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> greatereq_int#(pos x, pos y))
         (mod_int#(neg x, neg y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x))
         (div_nat#(s x, s y) -> minus_nat_s#(x, y), minus_nat_s#(s x, s y) -> minus_nat_s#(x, y))
         (mod_nat#(s x, s y) -> minus_nat_s#(x, y), minus_nat_s#(s x, s y) -> minus_nat_s#(x, y))
         (condMod#(true(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)), condLoop#(true(), b, e, r) -> mod_int#(e, pos s s 0()))
         (condMod#(true(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)), condLoop#(true(), b, e, r) -> equal_int#(mod_int(e, pos s s 0()), pos s 0()))
         (condMod#(true(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)), condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r))
         (condMod#(true(), b, e, r) -> mult_int#(b, b), mult_int#(neg x, neg y) -> mult_nat#(x, y))
         (condMod#(true(), b, e, r) -> mult_int#(b, b), mult_int#(neg x, pos y) -> mult_nat#(x, y))
         (condMod#(true(), b, e, r) -> mult_int#(b, b), mult_int#(pos x, neg y) -> mult_nat#(x, y))
         (condMod#(true(), b, e, r) -> mult_int#(b, b), mult_int#(pos x, pos y) -> mult_nat#(x, y))
         (condMod#(false(), b, e, r) -> mult_int#(b, b), mult_int#(neg x, neg y) -> mult_nat#(x, y))
         (condMod#(false(), b, e, r) -> mult_int#(b, b), mult_int#(neg x, pos y) -> mult_nat#(x, y))
         (condMod#(false(), b, e, r) -> mult_int#(b, b), mult_int#(pos x, neg y) -> mult_nat#(x, y))
         (condMod#(false(), b, e, r) -> mult_int#(b, b), mult_int#(pos x, pos y) -> mult_nat#(x, y))
         (sqBase#(b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r), condLoop#(true(), b, e, r) -> mod_int#(e, pos s s 0()))
         (sqBase#(b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r), condLoop#(true(), b, e, r) -> equal_int#(mod_int(e, pos s s 0()), pos s 0()))
         (sqBase#(b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r), condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r))
         (condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r), condMod#(false(), b, e, r) -> div_int#(e, pos s s 0()))
         (condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r), condMod#(false(), b, e, r) -> greater_int#(e, pos 0()))
         (condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r), condMod#(false(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r))
         (condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r), condMod#(false(), b, e, r) -> mult_int#(b, b))
         (condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r), condMod#(true(), b, e, r) -> div_int#(e, pos s s 0()))
         (condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r), condMod#(true(), b, e, r) -> greater_int#(e, pos 0()))
         (condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r), condMod#(true(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)))
         (condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r), condMod#(true(), b, e, r) -> mult_int#(r, b))
         (condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r), condMod#(true(), b, e, r) -> mult_int#(b, b))
         (greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
         (div_int#(pos x, neg s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> minus_nat_s#(x, y))
         (div_int#(pos x, neg s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> greatereq_int#(pos x, pos y))
         (div_int#(pos x, neg s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()))
         (div_int#(pos x, neg s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y))
         (div_int#(neg x, neg s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> minus_nat_s#(x, y))
         (div_int#(neg x, neg s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> greatereq_int#(pos x, pos y))
         (div_int#(neg x, neg s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()))
         (div_int#(neg x, neg s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y))
         (equal_int#(neg s x, neg s y) -> equal_int#(neg x, neg y), equal_int#(neg s x, neg s y) -> equal_int#(neg x, neg y))
         (mult_nat#(s x, s y) -> plus_nat#(mult_nat(x, s y), s y), plus_nat#(s x, y) -> plus_nat#(x, y))
         (div_nat#(s x, s y) -> greatereq_int#(pos x, pos y), greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y))
         (greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y), greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y))
         (mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y), mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y))
         (mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y), mod_nat#(s x, s y) -> minus_nat_s#(x, y))
         (mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y), mod_nat#(s x, s y) -> greatereq_int#(pos x, pos y))
         (mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y), mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x))
         (halfExp#(b, e, r) -> div_int#(e, pos s s 0()), div_int#(neg x, pos s y) -> div_nat#(x, s y))
         (halfExp#(b, e, r) -> div_int#(e, pos s s 0()), div_int#(pos x, pos s y) -> div_nat#(x, s y))
         (sqBase#(b, e, r) -> div_int#(e, pos s s 0()), div_int#(neg x, pos s y) -> div_nat#(x, s y))
         (sqBase#(b, e, r) -> div_int#(e, pos s s 0()), div_int#(pos x, pos s y) -> div_nat#(x, s y))
         (condMod#(true(), b, e, r) -> div_int#(e, pos s s 0()), div_int#(neg x, pos s y) -> div_nat#(x, s y))
         (condMod#(true(), b, e, r) -> div_int#(e, pos s s 0()), div_int#(pos x, pos s y) -> div_nat#(x, s y))
         (condMod#(false(), b, e, r) -> div_int#(e, pos s s 0()), div_int#(neg x, pos s y) -> div_nat#(x, s y))
         (condMod#(false(), b, e, r) -> div_int#(e, pos s s 0()), div_int#(pos x, pos s y) -> div_nat#(x, s y))
         (condLoop#(true(), b, e, r) -> mod_int#(e, pos s s 0()), mod_int#(neg x, pos y) -> mod_nat#(x, y))
         (condLoop#(true(), b, e, r) -> mod_int#(e, pos s s 0()), mod_int#(pos x, pos y) -> mod_nat#(x, y))
         (condLoop#(true(), b, e, r) -> equal_int#(mod_int(e, pos s s 0()), pos s 0()), equal_int#(pos s x, pos s y) -> equal_int#(pos x, pos y))
         (mod_nat#(s x, s y) -> greatereq_int#(pos x, pos y), greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y))
         (greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y), greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y))
         (div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y), div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y))
         (div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y), div_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()))
         (div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y), div_nat#(s x, s y) -> greatereq_int#(pos x, pos y))
         (div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y), div_nat#(s x, s y) -> minus_nat_s#(x, y))
         (mult_nat#(s x, s y) -> mult_nat#(x, s y), mult_nat#(s x, s y) -> mult_nat#(x, s y))
         (mult_nat#(s x, s y) -> mult_nat#(x, s y), mult_nat#(s x, s y) -> plus_nat#(mult_nat(x, s y), s y))
         (equal_int#(pos s x, pos s y) -> equal_int#(pos x, pos y), equal_int#(pos s x, pos s y) -> equal_int#(pos x, pos y))
         (div_int#(neg x, pos s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y))
         (div_int#(neg x, pos s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()))
         (div_int#(neg x, pos s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> greatereq_int#(pos x, pos y))
         (div_int#(neg x, pos s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> minus_nat_s#(x, y))
         (div_int#(pos x, pos s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y))
         (div_int#(pos x, pos s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()))
         (div_int#(pos x, pos s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> greatereq_int#(pos x, pos y))
         (div_int#(pos x, pos s y) -> div_nat#(x, s y), div_nat#(s x, s y) -> minus_nat_s#(x, y))
         (greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
         (condMod#(false(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r), condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r))
         (condMod#(false(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r), condLoop#(true(), b, e, r) -> equal_int#(mod_int(e, pos s s 0()), pos s 0()))
         (condMod#(false(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r), condLoop#(true(), b, e, r) -> mod_int#(e, pos s s 0()))
         (halfExp#(b, e, r) -> condLoop#(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r), condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r))
         (halfExp#(b, e, r) -> condLoop#(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r), condLoop#(true(), b, e, r) -> equal_int#(mod_int(e, pos s s 0()), pos s 0()))
         (halfExp#(b, e, r) -> condLoop#(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r), condLoop#(true(), b, e, r) -> mod_int#(e, pos s s 0()))
         (condMod#(true(), b, e, r) -> mult_int#(r, b), mult_int#(pos x, pos y) -> mult_nat#(x, y))
         (condMod#(true(), b, e, r) -> mult_int#(r, b), mult_int#(pos x, neg y) -> mult_nat#(x, y))
         (condMod#(true(), b, e, r) -> mult_int#(r, b), mult_int#(neg x, pos y) -> mult_nat#(x, y))
         (condMod#(true(), b, e, r) -> mult_int#(r, b), mult_int#(neg x, neg y) -> mult_nat#(x, y))
         (sqBase#(b, e, r) -> mult_int#(b, b), mult_int#(pos x, pos y) -> mult_nat#(x, y))
         (sqBase#(b, e, r) -> mult_int#(b, b), mult_int#(pos x, neg y) -> mult_nat#(x, y))
         (sqBase#(b, e, r) -> mult_int#(b, b), mult_int#(neg x, pos y) -> mult_nat#(x, y))
         (sqBase#(b, e, r) -> mult_int#(b, b), mult_int#(neg x, neg y) -> mult_nat#(x, y))
         (pow#(b, e) -> condLoop#(greater_int(e, pos 0()), b, e, pos s 0()), condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r))
         (pow#(b, e) -> condLoop#(greater_int(e, pos 0()), b, e, pos s 0()), condLoop#(true(), b, e, r) -> equal_int#(mod_int(e, pos s s 0()), pos s 0()))
         (pow#(b, e) -> condLoop#(greater_int(e, pos 0()), b, e, pos s 0()), condLoop#(true(), b, e, r) -> mod_int#(e, pos s s 0()))
         (minus_nat_s#(s x, s y) -> minus_nat_s#(x, y), minus_nat_s#(s x, s y) -> minus_nat_s#(x, y))
         (plus_nat#(s x, y) -> plus_nat#(x, y), plus_nat#(s x, y) -> plus_nat#(x, y))
         (mod_int#(neg x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x))
         (mod_int#(neg x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> greatereq_int#(pos x, pos y))
         (mod_int#(neg x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> minus_nat_s#(x, y))
         (mod_int#(neg x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y))
         (mod_int#(pos x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> if#(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x))
         (mod_int#(pos x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> greatereq_int#(pos x, pos y))
         (mod_int#(pos x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> minus_nat_s#(x, y))
         (mod_int#(pos x, pos y) -> mod_nat#(x, y), mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y))
         (mult_int#(neg x, pos y) -> mult_nat#(x, y), mult_nat#(s x, s y) -> mult_nat#(x, s y))
         (mult_int#(neg x, pos y) -> mult_nat#(x, y), mult_nat#(s x, s y) -> plus_nat#(mult_nat(x, s y), s y))
         (mult_int#(pos x, pos y) -> mult_nat#(x, y), mult_nat#(s x, s y) -> mult_nat#(x, s y))
         (mult_int#(pos x, pos y) -> mult_nat#(x, y), mult_nat#(s x, s y) -> plus_nat#(mult_nat(x, s y), s y))
        }
        SCCS (12):
         Scc:
          {mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y)}
         Scc:
          {minus_nat_s#(s x, s y) -> minus_nat_s#(x, y)}
         Scc:
          {greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y)}
         Scc:
          {greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y)}
         Scc:
          {div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y)}
         Scc:
          {plus_nat#(s x, y) -> plus_nat#(x, y)}
         Scc:
          {mult_nat#(s x, s y) -> mult_nat#(x, s y)}
         Scc:
          {equal_int#(neg s x, neg s y) -> equal_int#(neg x, neg y)}
         Scc:
          {equal_int#(pos s x, pos s y) -> equal_int#(pos x, pos y)}
         Scc:
          {greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y)}
         Scc:
          {greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y)}
         Scc:
          { condMod#(true(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)),
           condMod#(false(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
            condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r)}
         SCC:
          Strict:
           {mod_nat#(s x, s y) -> mod_nat#(minus_nat_s(x, y), s y)}
          Weak:
          {               halfExp(b, e, r) -> condLoop(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r),
                    mult_int(pos x, pos y) -> pos mult_nat(x, y),
                    mult_int(pos x, neg y) -> neg mult_nat(x, y),
                    mult_int(neg x, pos y) -> neg mult_nat(x, y),
                    mult_int(neg x, neg y) -> pos mult_nat(x, y),
                           sqBase(b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                  condMod(true(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)),
                 condMod(false(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                 condLoop(true(), b, e, r) -> condMod(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r),
                condLoop(false(), b, e, r) -> r,
             greater_int(pos 0(), pos 0()) -> false(),
             greater_int(pos 0(), pos s y) -> false(),
             greater_int(pos 0(), neg 0()) -> false(),
             greater_int(pos 0(), neg s y) -> true(),
             greater_int(pos s x, pos 0()) -> true(),
             greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
             greater_int(pos s x, neg 0()) -> true(),
             greater_int(pos s x, neg s y) -> true(),
             greater_int(neg 0(), pos 0()) -> false(),
             greater_int(neg 0(), pos s y) -> false(),
             greater_int(neg 0(), neg 0()) -> false(),
             greater_int(neg 0(), neg s y) -> true(),
             greater_int(neg s x, pos 0()) -> false(),
             greater_int(neg s x, pos s y) -> false(),
             greater_int(neg s x, neg 0()) -> false(),
             greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                   div_int(pos x, pos s y) -> pos div_nat(x, s y),
                   div_int(pos x, neg s y) -> neg div_nat(x, s y),
                   div_int(neg x, pos s y) -> neg div_nat(x, s y),
                   div_int(neg x, neg s y) -> pos div_nat(x, s y),
                                 pow(b, e) -> condLoop(greater_int(e, pos 0()), b, e, pos s 0()),
               equal_int(pos 0(), pos 0()) -> true(),
               equal_int(pos 0(), pos s y) -> false(),
               equal_int(pos 0(), neg 0()) -> true(),
               equal_int(pos 0(), neg s y) -> false(),
               equal_int(pos s x, pos 0()) -> false(),
               equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
               equal_int(pos s x, neg 0()) -> false(),
               equal_int(pos s x, neg s y) -> false(),
               equal_int(neg 0(), pos 0()) -> true(),
               equal_int(neg 0(), pos s y) -> false(),
               equal_int(neg 0(), neg 0()) -> true(),
               equal_int(neg 0(), neg s y) -> false(),
               equal_int(neg s x, pos 0()) -> false(),
               equal_int(neg s x, pos s y) -> false(),
               equal_int(neg s x, neg 0()) -> false(),
               equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
                     mod_int(pos x, pos y) -> pos mod_nat(x, y),
                     mod_int(pos x, neg y) -> pos mod_nat(x, y),
                     mod_int(neg x, pos y) -> neg mod_nat(x, y),
                     mod_int(neg x, neg y) -> neg mod_nat(x, y),
                          mult_nat(0(), y) -> 0(),
                        mult_nat(s x, 0()) -> 0(),
                        mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                          plus_nat(0(), x) -> x,
                          plus_nat(s x, y) -> s plus_nat(x, y),
                         div_nat(0(), s y) -> 0(),
                         div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                          if(true(), x, y) -> x,
                         if(false(), x, y) -> y,
             greatereq_int(pos x, pos 0()) -> true(),
               greatereq_int(pos x, neg y) -> true(),
           greatereq_int(pos 0(), pos s y) -> false(),
           greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
             greatereq_int(neg x, pos s y) -> false(),
           greatereq_int(neg 0(), pos 0()) -> true(),
             greatereq_int(neg 0(), neg y) -> true(),
           greatereq_int(neg s x, pos 0()) -> false(),
           greatereq_int(neg s x, neg 0()) -> false(),
           greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
                       minus_nat_s(x, 0()) -> x,
                     minus_nat_s(0(), s y) -> 0(),
                     minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                         mod_nat(0(), s x) -> 0(),
                         mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x)}
          UR:
           {  minus_nat_s(x, 0()) -> x,
            minus_nat_s(0(), s y) -> 0(),
            minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                          a(z, w) -> z,
                          a(z, w) -> w}
           ARCTIC:
            Argument Filtering:
             pi(a) = [0,1], pi(mod_nat#) = [0], pi(minus_nat_s) = [0], pi(s) = [0], pi(0) = []
            Usable Rules:
             {  minus_nat_s(x, 0()) -> x,
              minus_nat_s(0(), s y) -> 0(),
              minus_nat_s(s x, s y) -> minus_nat_s(x, y)}
            Interpretation:
             [minus_nat_s](x0) = 2x0 + 2,
             
             [s](x0) = 3x0 + 4,
             
             [0] = 0,
             
             [mod_nat#](x0) = -2x0 + 0
            Strict:
             {}
            Weak:
             {  minus_nat_s(x, 0()) -> x,
              minus_nat_s(0(), s y) -> 0(),
              minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                            a(z, w) -> z,
                            a(z, w) -> w}
            Qed
         SCC:
          Strict:
           {minus_nat_s#(s x, s y) -> minus_nat_s#(x, y)}
          Weak:
          {               halfExp(b, e, r) -> condLoop(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r),
                    mult_int(pos x, pos y) -> pos mult_nat(x, y),
                    mult_int(pos x, neg y) -> neg mult_nat(x, y),
                    mult_int(neg x, pos y) -> neg mult_nat(x, y),
                    mult_int(neg x, neg y) -> pos mult_nat(x, y),
                           sqBase(b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                  condMod(true(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)),
                 condMod(false(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                 condLoop(true(), b, e, r) -> condMod(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r),
                condLoop(false(), b, e, r) -> r,
             greater_int(pos 0(), pos 0()) -> false(),
             greater_int(pos 0(), pos s y) -> false(),
             greater_int(pos 0(), neg 0()) -> false(),
             greater_int(pos 0(), neg s y) -> true(),
             greater_int(pos s x, pos 0()) -> true(),
             greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
             greater_int(pos s x, neg 0()) -> true(),
             greater_int(pos s x, neg s y) -> true(),
             greater_int(neg 0(), pos 0()) -> false(),
             greater_int(neg 0(), pos s y) -> false(),
             greater_int(neg 0(), neg 0()) -> false(),
             greater_int(neg 0(), neg s y) -> true(),
             greater_int(neg s x, pos 0()) -> false(),
             greater_int(neg s x, pos s y) -> false(),
             greater_int(neg s x, neg 0()) -> false(),
             greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                   div_int(pos x, pos s y) -> pos div_nat(x, s y),
                   div_int(pos x, neg s y) -> neg div_nat(x, s y),
                   div_int(neg x, pos s y) -> neg div_nat(x, s y),
                   div_int(neg x, neg s y) -> pos div_nat(x, s y),
                                 pow(b, e) -> condLoop(greater_int(e, pos 0()), b, e, pos s 0()),
               equal_int(pos 0(), pos 0()) -> true(),
               equal_int(pos 0(), pos s y) -> false(),
               equal_int(pos 0(), neg 0()) -> true(),
               equal_int(pos 0(), neg s y) -> false(),
               equal_int(pos s x, pos 0()) -> false(),
               equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
               equal_int(pos s x, neg 0()) -> false(),
               equal_int(pos s x, neg s y) -> false(),
               equal_int(neg 0(), pos 0()) -> true(),
               equal_int(neg 0(), pos s y) -> false(),
               equal_int(neg 0(), neg 0()) -> true(),
               equal_int(neg 0(), neg s y) -> false(),
               equal_int(neg s x, pos 0()) -> false(),
               equal_int(neg s x, pos s y) -> false(),
               equal_int(neg s x, neg 0()) -> false(),
               equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
                     mod_int(pos x, pos y) -> pos mod_nat(x, y),
                     mod_int(pos x, neg y) -> pos mod_nat(x, y),
                     mod_int(neg x, pos y) -> neg mod_nat(x, y),
                     mod_int(neg x, neg y) -> neg mod_nat(x, y),
                          mult_nat(0(), y) -> 0(),
                        mult_nat(s x, 0()) -> 0(),
                        mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                          plus_nat(0(), x) -> x,
                          plus_nat(s x, y) -> s plus_nat(x, y),
                         div_nat(0(), s y) -> 0(),
                         div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                          if(true(), x, y) -> x,
                         if(false(), x, y) -> y,
             greatereq_int(pos x, pos 0()) -> true(),
               greatereq_int(pos x, neg y) -> true(),
           greatereq_int(pos 0(), pos s y) -> false(),
           greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
             greatereq_int(neg x, pos s y) -> false(),
           greatereq_int(neg 0(), pos 0()) -> true(),
             greatereq_int(neg 0(), neg y) -> true(),
           greatereq_int(neg s x, pos 0()) -> false(),
           greatereq_int(neg s x, neg 0()) -> false(),
           greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
                       minus_nat_s(x, 0()) -> x,
                     minus_nat_s(0(), s y) -> 0(),
                     minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                         mod_nat(0(), s x) -> 0(),
                         mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x)}
          SPSC:
           Simple Projection:
            pi(minus_nat_s#) = 1
           Strict:
            {}
           Qed
         SCC:
          Strict:
           {greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y)}
          Weak:
          {               halfExp(b, e, r) -> condLoop(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r),
                    mult_int(pos x, pos y) -> pos mult_nat(x, y),
                    mult_int(pos x, neg y) -> neg mult_nat(x, y),
                    mult_int(neg x, pos y) -> neg mult_nat(x, y),
                    mult_int(neg x, neg y) -> pos mult_nat(x, y),
                           sqBase(b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                  condMod(true(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)),
                 condMod(false(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                 condLoop(true(), b, e, r) -> condMod(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r),
                condLoop(false(), b, e, r) -> r,
             greater_int(pos 0(), pos 0()) -> false(),
             greater_int(pos 0(), pos s y) -> false(),
             greater_int(pos 0(), neg 0()) -> false(),
             greater_int(pos 0(), neg s y) -> true(),
             greater_int(pos s x, pos 0()) -> true(),
             greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
             greater_int(pos s x, neg 0()) -> true(),
             greater_int(pos s x, neg s y) -> true(),
             greater_int(neg 0(), pos 0()) -> false(),
             greater_int(neg 0(), pos s y) -> false(),
             greater_int(neg 0(), neg 0()) -> false(),
             greater_int(neg 0(), neg s y) -> true(),
             greater_int(neg s x, pos 0()) -> false(),
             greater_int(neg s x, pos s y) -> false(),
             greater_int(neg s x, neg 0()) -> false(),
             greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                   div_int(pos x, pos s y) -> pos div_nat(x, s y),
                   div_int(pos x, neg s y) -> neg div_nat(x, s y),
                   div_int(neg x, pos s y) -> neg div_nat(x, s y),
                   div_int(neg x, neg s y) -> pos div_nat(x, s y),
                                 pow(b, e) -> condLoop(greater_int(e, pos 0()), b, e, pos s 0()),
               equal_int(pos 0(), pos 0()) -> true(),
               equal_int(pos 0(), pos s y) -> false(),
               equal_int(pos 0(), neg 0()) -> true(),
               equal_int(pos 0(), neg s y) -> false(),
               equal_int(pos s x, pos 0()) -> false(),
               equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
               equal_int(pos s x, neg 0()) -> false(),
               equal_int(pos s x, neg s y) -> false(),
               equal_int(neg 0(), pos 0()) -> true(),
               equal_int(neg 0(), pos s y) -> false(),
               equal_int(neg 0(), neg 0()) -> true(),
               equal_int(neg 0(), neg s y) -> false(),
               equal_int(neg s x, pos 0()) -> false(),
               equal_int(neg s x, pos s y) -> false(),
               equal_int(neg s x, neg 0()) -> false(),
               equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
                     mod_int(pos x, pos y) -> pos mod_nat(x, y),
                     mod_int(pos x, neg y) -> pos mod_nat(x, y),
                     mod_int(neg x, pos y) -> neg mod_nat(x, y),
                     mod_int(neg x, neg y) -> neg mod_nat(x, y),
                          mult_nat(0(), y) -> 0(),
                        mult_nat(s x, 0()) -> 0(),
                        mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                          plus_nat(0(), x) -> x,
                          plus_nat(s x, y) -> s plus_nat(x, y),
                         div_nat(0(), s y) -> 0(),
                         div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                          if(true(), x, y) -> x,
                         if(false(), x, y) -> y,
             greatereq_int(pos x, pos 0()) -> true(),
               greatereq_int(pos x, neg y) -> true(),
           greatereq_int(pos 0(), pos s y) -> false(),
           greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
             greatereq_int(neg x, pos s y) -> false(),
           greatereq_int(neg 0(), pos 0()) -> true(),
             greatereq_int(neg 0(), neg y) -> true(),
           greatereq_int(neg s x, pos 0()) -> false(),
           greatereq_int(neg s x, neg 0()) -> false(),
           greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
                       minus_nat_s(x, 0()) -> x,
                     minus_nat_s(0(), s y) -> 0(),
                     minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                         mod_nat(0(), s x) -> 0(),
                         mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x)}
          UR:
           {}
           ARCTIC:
            Argument Filtering:
             pi(greatereq_int#) = [1], pi(neg) = [0], pi(s) = [0]
            Usable Rules:
             {}
            Interpretation:
             [neg](x0) = -4x0 + 0,
             
             [s](x0) = 5x0 + 9,
             
             [greatereq_int#](x0) = -4x0 + 0
            Strict:
             {}
            Weak:
             {}
            Qed
         SCC:
          Strict:
           {greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y)}
          Weak:
          {               halfExp(b, e, r) -> condLoop(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r),
                    mult_int(pos x, pos y) -> pos mult_nat(x, y),
                    mult_int(pos x, neg y) -> neg mult_nat(x, y),
                    mult_int(neg x, pos y) -> neg mult_nat(x, y),
                    mult_int(neg x, neg y) -> pos mult_nat(x, y),
                           sqBase(b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                  condMod(true(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)),
                 condMod(false(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                 condLoop(true(), b, e, r) -> condMod(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r),
                condLoop(false(), b, e, r) -> r,
             greater_int(pos 0(), pos 0()) -> false(),
             greater_int(pos 0(), pos s y) -> false(),
             greater_int(pos 0(), neg 0()) -> false(),
             greater_int(pos 0(), neg s y) -> true(),
             greater_int(pos s x, pos 0()) -> true(),
             greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
             greater_int(pos s x, neg 0()) -> true(),
             greater_int(pos s x, neg s y) -> true(),
             greater_int(neg 0(), pos 0()) -> false(),
             greater_int(neg 0(), pos s y) -> false(),
             greater_int(neg 0(), neg 0()) -> false(),
             greater_int(neg 0(), neg s y) -> true(),
             greater_int(neg s x, pos 0()) -> false(),
             greater_int(neg s x, pos s y) -> false(),
             greater_int(neg s x, neg 0()) -> false(),
             greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                   div_int(pos x, pos s y) -> pos div_nat(x, s y),
                   div_int(pos x, neg s y) -> neg div_nat(x, s y),
                   div_int(neg x, pos s y) -> neg div_nat(x, s y),
                   div_int(neg x, neg s y) -> pos div_nat(x, s y),
                                 pow(b, e) -> condLoop(greater_int(e, pos 0()), b, e, pos s 0()),
               equal_int(pos 0(), pos 0()) -> true(),
               equal_int(pos 0(), pos s y) -> false(),
               equal_int(pos 0(), neg 0()) -> true(),
               equal_int(pos 0(), neg s y) -> false(),
               equal_int(pos s x, pos 0()) -> false(),
               equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
               equal_int(pos s x, neg 0()) -> false(),
               equal_int(pos s x, neg s y) -> false(),
               equal_int(neg 0(), pos 0()) -> true(),
               equal_int(neg 0(), pos s y) -> false(),
               equal_int(neg 0(), neg 0()) -> true(),
               equal_int(neg 0(), neg s y) -> false(),
               equal_int(neg s x, pos 0()) -> false(),
               equal_int(neg s x, pos s y) -> false(),
               equal_int(neg s x, neg 0()) -> false(),
               equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
                     mod_int(pos x, pos y) -> pos mod_nat(x, y),
                     mod_int(pos x, neg y) -> pos mod_nat(x, y),
                     mod_int(neg x, pos y) -> neg mod_nat(x, y),
                     mod_int(neg x, neg y) -> neg mod_nat(x, y),
                          mult_nat(0(), y) -> 0(),
                        mult_nat(s x, 0()) -> 0(),
                        mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                          plus_nat(0(), x) -> x,
                          plus_nat(s x, y) -> s plus_nat(x, y),
                         div_nat(0(), s y) -> 0(),
                         div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                          if(true(), x, y) -> x,
                         if(false(), x, y) -> y,
             greatereq_int(pos x, pos 0()) -> true(),
               greatereq_int(pos x, neg y) -> true(),
           greatereq_int(pos 0(), pos s y) -> false(),
           greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
             greatereq_int(neg x, pos s y) -> false(),
           greatereq_int(neg 0(), pos 0()) -> true(),
             greatereq_int(neg 0(), neg y) -> true(),
           greatereq_int(neg s x, pos 0()) -> false(),
           greatereq_int(neg s x, neg 0()) -> false(),
           greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
                       minus_nat_s(x, 0()) -> x,
                     minus_nat_s(0(), s y) -> 0(),
                     minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                         mod_nat(0(), s x) -> 0(),
                         mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x)}
          UR:
           {}
           ARCTIC:
            Argument Filtering:
             pi(greatereq_int#) = 1, pi(s) = [0], pi(pos) = 0
            Usable Rules:
             {}
            Interpretation:
             [s](x0) = 1x0
            Strict:
             {}
            Weak:
             {}
            Qed
         SCC:
          Strict:
           {div_nat#(s x, s y) -> div_nat#(minus_nat_s(x, y), s y)}
          Weak:
          {               halfExp(b, e, r) -> condLoop(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r),
                    mult_int(pos x, pos y) -> pos mult_nat(x, y),
                    mult_int(pos x, neg y) -> neg mult_nat(x, y),
                    mult_int(neg x, pos y) -> neg mult_nat(x, y),
                    mult_int(neg x, neg y) -> pos mult_nat(x, y),
                           sqBase(b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                  condMod(true(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)),
                 condMod(false(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                 condLoop(true(), b, e, r) -> condMod(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r),
                condLoop(false(), b, e, r) -> r,
             greater_int(pos 0(), pos 0()) -> false(),
             greater_int(pos 0(), pos s y) -> false(),
             greater_int(pos 0(), neg 0()) -> false(),
             greater_int(pos 0(), neg s y) -> true(),
             greater_int(pos s x, pos 0()) -> true(),
             greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
             greater_int(pos s x, neg 0()) -> true(),
             greater_int(pos s x, neg s y) -> true(),
             greater_int(neg 0(), pos 0()) -> false(),
             greater_int(neg 0(), pos s y) -> false(),
             greater_int(neg 0(), neg 0()) -> false(),
             greater_int(neg 0(), neg s y) -> true(),
             greater_int(neg s x, pos 0()) -> false(),
             greater_int(neg s x, pos s y) -> false(),
             greater_int(neg s x, neg 0()) -> false(),
             greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                   div_int(pos x, pos s y) -> pos div_nat(x, s y),
                   div_int(pos x, neg s y) -> neg div_nat(x, s y),
                   div_int(neg x, pos s y) -> neg div_nat(x, s y),
                   div_int(neg x, neg s y) -> pos div_nat(x, s y),
                                 pow(b, e) -> condLoop(greater_int(e, pos 0()), b, e, pos s 0()),
               equal_int(pos 0(), pos 0()) -> true(),
               equal_int(pos 0(), pos s y) -> false(),
               equal_int(pos 0(), neg 0()) -> true(),
               equal_int(pos 0(), neg s y) -> false(),
               equal_int(pos s x, pos 0()) -> false(),
               equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
               equal_int(pos s x, neg 0()) -> false(),
               equal_int(pos s x, neg s y) -> false(),
               equal_int(neg 0(), pos 0()) -> true(),
               equal_int(neg 0(), pos s y) -> false(),
               equal_int(neg 0(), neg 0()) -> true(),
               equal_int(neg 0(), neg s y) -> false(),
               equal_int(neg s x, pos 0()) -> false(),
               equal_int(neg s x, pos s y) -> false(),
               equal_int(neg s x, neg 0()) -> false(),
               equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
                     mod_int(pos x, pos y) -> pos mod_nat(x, y),
                     mod_int(pos x, neg y) -> pos mod_nat(x, y),
                     mod_int(neg x, pos y) -> neg mod_nat(x, y),
                     mod_int(neg x, neg y) -> neg mod_nat(x, y),
                          mult_nat(0(), y) -> 0(),
                        mult_nat(s x, 0()) -> 0(),
                        mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                          plus_nat(0(), x) -> x,
                          plus_nat(s x, y) -> s plus_nat(x, y),
                         div_nat(0(), s y) -> 0(),
                         div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                          if(true(), x, y) -> x,
                         if(false(), x, y) -> y,
             greatereq_int(pos x, pos 0()) -> true(),
               greatereq_int(pos x, neg y) -> true(),
           greatereq_int(pos 0(), pos s y) -> false(),
           greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
             greatereq_int(neg x, pos s y) -> false(),
           greatereq_int(neg 0(), pos 0()) -> true(),
             greatereq_int(neg 0(), neg y) -> true(),
           greatereq_int(neg s x, pos 0()) -> false(),
           greatereq_int(neg s x, neg 0()) -> false(),
           greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
                       minus_nat_s(x, 0()) -> x,
                     minus_nat_s(0(), s y) -> 0(),
                     minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                         mod_nat(0(), s x) -> 0(),
                         mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x)}
          UR:
           {  minus_nat_s(x, 0()) -> x,
            minus_nat_s(0(), s y) -> 0(),
            minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                          a(z, w) -> z,
                          a(z, w) -> w}
           ARCTIC:
            Argument Filtering:
             pi(a) = [0,1], pi(minus_nat_s) = 0, pi(div_nat#) = 0, pi(s) = [0], pi(0) = []
            Usable Rules:
             {  minus_nat_s(x, 0()) -> x,
              minus_nat_s(0(), s y) -> 0(),
              minus_nat_s(s x, s y) -> minus_nat_s(x, y)}
            Interpretation:
             [s](x0) = 1x0,
             
             [0] = 0
            Strict:
             {}
            Weak:
             {  minus_nat_s(x, 0()) -> x,
              minus_nat_s(0(), s y) -> 0(),
              minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                            a(z, w) -> z,
                            a(z, w) -> w}
            Qed
         SCC:
          Strict:
           {plus_nat#(s x, y) -> plus_nat#(x, y)}
          Weak:
          {               halfExp(b, e, r) -> condLoop(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r),
                    mult_int(pos x, pos y) -> pos mult_nat(x, y),
                    mult_int(pos x, neg y) -> neg mult_nat(x, y),
                    mult_int(neg x, pos y) -> neg mult_nat(x, y),
                    mult_int(neg x, neg y) -> pos mult_nat(x, y),
                           sqBase(b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                  condMod(true(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)),
                 condMod(false(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                 condLoop(true(), b, e, r) -> condMod(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r),
                condLoop(false(), b, e, r) -> r,
             greater_int(pos 0(), pos 0()) -> false(),
             greater_int(pos 0(), pos s y) -> false(),
             greater_int(pos 0(), neg 0()) -> false(),
             greater_int(pos 0(), neg s y) -> true(),
             greater_int(pos s x, pos 0()) -> true(),
             greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
             greater_int(pos s x, neg 0()) -> true(),
             greater_int(pos s x, neg s y) -> true(),
             greater_int(neg 0(), pos 0()) -> false(),
             greater_int(neg 0(), pos s y) -> false(),
             greater_int(neg 0(), neg 0()) -> false(),
             greater_int(neg 0(), neg s y) -> true(),
             greater_int(neg s x, pos 0()) -> false(),
             greater_int(neg s x, pos s y) -> false(),
             greater_int(neg s x, neg 0()) -> false(),
             greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                   div_int(pos x, pos s y) -> pos div_nat(x, s y),
                   div_int(pos x, neg s y) -> neg div_nat(x, s y),
                   div_int(neg x, pos s y) -> neg div_nat(x, s y),
                   div_int(neg x, neg s y) -> pos div_nat(x, s y),
                                 pow(b, e) -> condLoop(greater_int(e, pos 0()), b, e, pos s 0()),
               equal_int(pos 0(), pos 0()) -> true(),
               equal_int(pos 0(), pos s y) -> false(),
               equal_int(pos 0(), neg 0()) -> true(),
               equal_int(pos 0(), neg s y) -> false(),
               equal_int(pos s x, pos 0()) -> false(),
               equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
               equal_int(pos s x, neg 0()) -> false(),
               equal_int(pos s x, neg s y) -> false(),
               equal_int(neg 0(), pos 0()) -> true(),
               equal_int(neg 0(), pos s y) -> false(),
               equal_int(neg 0(), neg 0()) -> true(),
               equal_int(neg 0(), neg s y) -> false(),
               equal_int(neg s x, pos 0()) -> false(),
               equal_int(neg s x, pos s y) -> false(),
               equal_int(neg s x, neg 0()) -> false(),
               equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
                     mod_int(pos x, pos y) -> pos mod_nat(x, y),
                     mod_int(pos x, neg y) -> pos mod_nat(x, y),
                     mod_int(neg x, pos y) -> neg mod_nat(x, y),
                     mod_int(neg x, neg y) -> neg mod_nat(x, y),
                          mult_nat(0(), y) -> 0(),
                        mult_nat(s x, 0()) -> 0(),
                        mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                          plus_nat(0(), x) -> x,
                          plus_nat(s x, y) -> s plus_nat(x, y),
                         div_nat(0(), s y) -> 0(),
                         div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                          if(true(), x, y) -> x,
                         if(false(), x, y) -> y,
             greatereq_int(pos x, pos 0()) -> true(),
               greatereq_int(pos x, neg y) -> true(),
           greatereq_int(pos 0(), pos s y) -> false(),
           greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
             greatereq_int(neg x, pos s y) -> false(),
           greatereq_int(neg 0(), pos 0()) -> true(),
             greatereq_int(neg 0(), neg y) -> true(),
           greatereq_int(neg s x, pos 0()) -> false(),
           greatereq_int(neg s x, neg 0()) -> false(),
           greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
                       minus_nat_s(x, 0()) -> x,
                     minus_nat_s(0(), s y) -> 0(),
                     minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                         mod_nat(0(), s x) -> 0(),
                         mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x)}
          SPSC:
           Simple Projection:
            pi(plus_nat#) = 0
           Strict:
            {}
           Qed
         SCC:
          Strict:
           {mult_nat#(s x, s y) -> mult_nat#(x, s y)}
          Weak:
          {               halfExp(b, e, r) -> condLoop(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r),
                    mult_int(pos x, pos y) -> pos mult_nat(x, y),
                    mult_int(pos x, neg y) -> neg mult_nat(x, y),
                    mult_int(neg x, pos y) -> neg mult_nat(x, y),
                    mult_int(neg x, neg y) -> pos mult_nat(x, y),
                           sqBase(b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                  condMod(true(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)),
                 condMod(false(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                 condLoop(true(), b, e, r) -> condMod(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r),
                condLoop(false(), b, e, r) -> r,
             greater_int(pos 0(), pos 0()) -> false(),
             greater_int(pos 0(), pos s y) -> false(),
             greater_int(pos 0(), neg 0()) -> false(),
             greater_int(pos 0(), neg s y) -> true(),
             greater_int(pos s x, pos 0()) -> true(),
             greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
             greater_int(pos s x, neg 0()) -> true(),
             greater_int(pos s x, neg s y) -> true(),
             greater_int(neg 0(), pos 0()) -> false(),
             greater_int(neg 0(), pos s y) -> false(),
             greater_int(neg 0(), neg 0()) -> false(),
             greater_int(neg 0(), neg s y) -> true(),
             greater_int(neg s x, pos 0()) -> false(),
             greater_int(neg s x, pos s y) -> false(),
             greater_int(neg s x, neg 0()) -> false(),
             greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                   div_int(pos x, pos s y) -> pos div_nat(x, s y),
                   div_int(pos x, neg s y) -> neg div_nat(x, s y),
                   div_int(neg x, pos s y) -> neg div_nat(x, s y),
                   div_int(neg x, neg s y) -> pos div_nat(x, s y),
                                 pow(b, e) -> condLoop(greater_int(e, pos 0()), b, e, pos s 0()),
               equal_int(pos 0(), pos 0()) -> true(),
               equal_int(pos 0(), pos s y) -> false(),
               equal_int(pos 0(), neg 0()) -> true(),
               equal_int(pos 0(), neg s y) -> false(),
               equal_int(pos s x, pos 0()) -> false(),
               equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
               equal_int(pos s x, neg 0()) -> false(),
               equal_int(pos s x, neg s y) -> false(),
               equal_int(neg 0(), pos 0()) -> true(),
               equal_int(neg 0(), pos s y) -> false(),
               equal_int(neg 0(), neg 0()) -> true(),
               equal_int(neg 0(), neg s y) -> false(),
               equal_int(neg s x, pos 0()) -> false(),
               equal_int(neg s x, pos s y) -> false(),
               equal_int(neg s x, neg 0()) -> false(),
               equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
                     mod_int(pos x, pos y) -> pos mod_nat(x, y),
                     mod_int(pos x, neg y) -> pos mod_nat(x, y),
                     mod_int(neg x, pos y) -> neg mod_nat(x, y),
                     mod_int(neg x, neg y) -> neg mod_nat(x, y),
                          mult_nat(0(), y) -> 0(),
                        mult_nat(s x, 0()) -> 0(),
                        mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                          plus_nat(0(), x) -> x,
                          plus_nat(s x, y) -> s plus_nat(x, y),
                         div_nat(0(), s y) -> 0(),
                         div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                          if(true(), x, y) -> x,
                         if(false(), x, y) -> y,
             greatereq_int(pos x, pos 0()) -> true(),
               greatereq_int(pos x, neg y) -> true(),
           greatereq_int(pos 0(), pos s y) -> false(),
           greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
             greatereq_int(neg x, pos s y) -> false(),
           greatereq_int(neg 0(), pos 0()) -> true(),
             greatereq_int(neg 0(), neg y) -> true(),
           greatereq_int(neg s x, pos 0()) -> false(),
           greatereq_int(neg s x, neg 0()) -> false(),
           greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
                       minus_nat_s(x, 0()) -> x,
                     minus_nat_s(0(), s y) -> 0(),
                     minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                         mod_nat(0(), s x) -> 0(),
                         mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x)}
          SPSC:
           Simple Projection:
            pi(mult_nat#) = 0
           Strict:
            {}
           Qed
         SCC:
          Strict:
           {equal_int#(neg s x, neg s y) -> equal_int#(neg x, neg y)}
          Weak:
          {               halfExp(b, e, r) -> condLoop(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r),
                    mult_int(pos x, pos y) -> pos mult_nat(x, y),
                    mult_int(pos x, neg y) -> neg mult_nat(x, y),
                    mult_int(neg x, pos y) -> neg mult_nat(x, y),
                    mult_int(neg x, neg y) -> pos mult_nat(x, y),
                           sqBase(b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                  condMod(true(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)),
                 condMod(false(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                 condLoop(true(), b, e, r) -> condMod(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r),
                condLoop(false(), b, e, r) -> r,
             greater_int(pos 0(), pos 0()) -> false(),
             greater_int(pos 0(), pos s y) -> false(),
             greater_int(pos 0(), neg 0()) -> false(),
             greater_int(pos 0(), neg s y) -> true(),
             greater_int(pos s x, pos 0()) -> true(),
             greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
             greater_int(pos s x, neg 0()) -> true(),
             greater_int(pos s x, neg s y) -> true(),
             greater_int(neg 0(), pos 0()) -> false(),
             greater_int(neg 0(), pos s y) -> false(),
             greater_int(neg 0(), neg 0()) -> false(),
             greater_int(neg 0(), neg s y) -> true(),
             greater_int(neg s x, pos 0()) -> false(),
             greater_int(neg s x, pos s y) -> false(),
             greater_int(neg s x, neg 0()) -> false(),
             greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                   div_int(pos x, pos s y) -> pos div_nat(x, s y),
                   div_int(pos x, neg s y) -> neg div_nat(x, s y),
                   div_int(neg x, pos s y) -> neg div_nat(x, s y),
                   div_int(neg x, neg s y) -> pos div_nat(x, s y),
                                 pow(b, e) -> condLoop(greater_int(e, pos 0()), b, e, pos s 0()),
               equal_int(pos 0(), pos 0()) -> true(),
               equal_int(pos 0(), pos s y) -> false(),
               equal_int(pos 0(), neg 0()) -> true(),
               equal_int(pos 0(), neg s y) -> false(),
               equal_int(pos s x, pos 0()) -> false(),
               equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
               equal_int(pos s x, neg 0()) -> false(),
               equal_int(pos s x, neg s y) -> false(),
               equal_int(neg 0(), pos 0()) -> true(),
               equal_int(neg 0(), pos s y) -> false(),
               equal_int(neg 0(), neg 0()) -> true(),
               equal_int(neg 0(), neg s y) -> false(),
               equal_int(neg s x, pos 0()) -> false(),
               equal_int(neg s x, pos s y) -> false(),
               equal_int(neg s x, neg 0()) -> false(),
               equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
                     mod_int(pos x, pos y) -> pos mod_nat(x, y),
                     mod_int(pos x, neg y) -> pos mod_nat(x, y),
                     mod_int(neg x, pos y) -> neg mod_nat(x, y),
                     mod_int(neg x, neg y) -> neg mod_nat(x, y),
                          mult_nat(0(), y) -> 0(),
                        mult_nat(s x, 0()) -> 0(),
                        mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                          plus_nat(0(), x) -> x,
                          plus_nat(s x, y) -> s plus_nat(x, y),
                         div_nat(0(), s y) -> 0(),
                         div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                          if(true(), x, y) -> x,
                         if(false(), x, y) -> y,
             greatereq_int(pos x, pos 0()) -> true(),
               greatereq_int(pos x, neg y) -> true(),
           greatereq_int(pos 0(), pos s y) -> false(),
           greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
             greatereq_int(neg x, pos s y) -> false(),
           greatereq_int(neg 0(), pos 0()) -> true(),
             greatereq_int(neg 0(), neg y) -> true(),
           greatereq_int(neg s x, pos 0()) -> false(),
           greatereq_int(neg s x, neg 0()) -> false(),
           greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
                       minus_nat_s(x, 0()) -> x,
                     minus_nat_s(0(), s y) -> 0(),
                     minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                         mod_nat(0(), s x) -> 0(),
                         mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x)}
          UR:
           {}
           ARCTIC:
            Argument Filtering:
             pi(neg) = 0, pi(equal_int#) = 1, pi(s) = [0]
            Usable Rules:
             {}
            Interpretation:
             [s](x0) = 1x0
            Strict:
             {}
            Weak:
             {}
            Qed
         SCC:
          Strict:
           {equal_int#(pos s x, pos s y) -> equal_int#(pos x, pos y)}
          Weak:
          {               halfExp(b, e, r) -> condLoop(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r),
                    mult_int(pos x, pos y) -> pos mult_nat(x, y),
                    mult_int(pos x, neg y) -> neg mult_nat(x, y),
                    mult_int(neg x, pos y) -> neg mult_nat(x, y),
                    mult_int(neg x, neg y) -> pos mult_nat(x, y),
                           sqBase(b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                  condMod(true(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)),
                 condMod(false(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                 condLoop(true(), b, e, r) -> condMod(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r),
                condLoop(false(), b, e, r) -> r,
             greater_int(pos 0(), pos 0()) -> false(),
             greater_int(pos 0(), pos s y) -> false(),
             greater_int(pos 0(), neg 0()) -> false(),
             greater_int(pos 0(), neg s y) -> true(),
             greater_int(pos s x, pos 0()) -> true(),
             greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
             greater_int(pos s x, neg 0()) -> true(),
             greater_int(pos s x, neg s y) -> true(),
             greater_int(neg 0(), pos 0()) -> false(),
             greater_int(neg 0(), pos s y) -> false(),
             greater_int(neg 0(), neg 0()) -> false(),
             greater_int(neg 0(), neg s y) -> true(),
             greater_int(neg s x, pos 0()) -> false(),
             greater_int(neg s x, pos s y) -> false(),
             greater_int(neg s x, neg 0()) -> false(),
             greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                   div_int(pos x, pos s y) -> pos div_nat(x, s y),
                   div_int(pos x, neg s y) -> neg div_nat(x, s y),
                   div_int(neg x, pos s y) -> neg div_nat(x, s y),
                   div_int(neg x, neg s y) -> pos div_nat(x, s y),
                                 pow(b, e) -> condLoop(greater_int(e, pos 0()), b, e, pos s 0()),
               equal_int(pos 0(), pos 0()) -> true(),
               equal_int(pos 0(), pos s y) -> false(),
               equal_int(pos 0(), neg 0()) -> true(),
               equal_int(pos 0(), neg s y) -> false(),
               equal_int(pos s x, pos 0()) -> false(),
               equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
               equal_int(pos s x, neg 0()) -> false(),
               equal_int(pos s x, neg s y) -> false(),
               equal_int(neg 0(), pos 0()) -> true(),
               equal_int(neg 0(), pos s y) -> false(),
               equal_int(neg 0(), neg 0()) -> true(),
               equal_int(neg 0(), neg s y) -> false(),
               equal_int(neg s x, pos 0()) -> false(),
               equal_int(neg s x, pos s y) -> false(),
               equal_int(neg s x, neg 0()) -> false(),
               equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
                     mod_int(pos x, pos y) -> pos mod_nat(x, y),
                     mod_int(pos x, neg y) -> pos mod_nat(x, y),
                     mod_int(neg x, pos y) -> neg mod_nat(x, y),
                     mod_int(neg x, neg y) -> neg mod_nat(x, y),
                          mult_nat(0(), y) -> 0(),
                        mult_nat(s x, 0()) -> 0(),
                        mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                          plus_nat(0(), x) -> x,
                          plus_nat(s x, y) -> s plus_nat(x, y),
                         div_nat(0(), s y) -> 0(),
                         div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                          if(true(), x, y) -> x,
                         if(false(), x, y) -> y,
             greatereq_int(pos x, pos 0()) -> true(),
               greatereq_int(pos x, neg y) -> true(),
           greatereq_int(pos 0(), pos s y) -> false(),
           greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
             greatereq_int(neg x, pos s y) -> false(),
           greatereq_int(neg 0(), pos 0()) -> true(),
             greatereq_int(neg 0(), neg y) -> true(),
           greatereq_int(neg s x, pos 0()) -> false(),
           greatereq_int(neg s x, neg 0()) -> false(),
           greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
                       minus_nat_s(x, 0()) -> x,
                     minus_nat_s(0(), s y) -> 0(),
                     minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                         mod_nat(0(), s x) -> 0(),
                         mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x)}
          UR:
           {}
           ARCTIC:
            Argument Filtering:
             pi(equal_int#) = [1], pi(s) = [0], pi(pos) = [0]
            Usable Rules:
             {}
            Interpretation:
             [s](x0) = 5x0 + 9,
             
             [pos](x0) = -4x0 + 0,
             
             [equal_int#](x0) = -4x0 + 0
            Strict:
             {}
            Weak:
             {}
            Qed
         SCC:
          Strict:
           {greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y)}
          Weak:
          {               halfExp(b, e, r) -> condLoop(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r),
                    mult_int(pos x, pos y) -> pos mult_nat(x, y),
                    mult_int(pos x, neg y) -> neg mult_nat(x, y),
                    mult_int(neg x, pos y) -> neg mult_nat(x, y),
                    mult_int(neg x, neg y) -> pos mult_nat(x, y),
                           sqBase(b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                  condMod(true(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)),
                 condMod(false(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                 condLoop(true(), b, e, r) -> condMod(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r),
                condLoop(false(), b, e, r) -> r,
             greater_int(pos 0(), pos 0()) -> false(),
             greater_int(pos 0(), pos s y) -> false(),
             greater_int(pos 0(), neg 0()) -> false(),
             greater_int(pos 0(), neg s y) -> true(),
             greater_int(pos s x, pos 0()) -> true(),
             greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
             greater_int(pos s x, neg 0()) -> true(),
             greater_int(pos s x, neg s y) -> true(),
             greater_int(neg 0(), pos 0()) -> false(),
             greater_int(neg 0(), pos s y) -> false(),
             greater_int(neg 0(), neg 0()) -> false(),
             greater_int(neg 0(), neg s y) -> true(),
             greater_int(neg s x, pos 0()) -> false(),
             greater_int(neg s x, pos s y) -> false(),
             greater_int(neg s x, neg 0()) -> false(),
             greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                   div_int(pos x, pos s y) -> pos div_nat(x, s y),
                   div_int(pos x, neg s y) -> neg div_nat(x, s y),
                   div_int(neg x, pos s y) -> neg div_nat(x, s y),
                   div_int(neg x, neg s y) -> pos div_nat(x, s y),
                                 pow(b, e) -> condLoop(greater_int(e, pos 0()), b, e, pos s 0()),
               equal_int(pos 0(), pos 0()) -> true(),
               equal_int(pos 0(), pos s y) -> false(),
               equal_int(pos 0(), neg 0()) -> true(),
               equal_int(pos 0(), neg s y) -> false(),
               equal_int(pos s x, pos 0()) -> false(),
               equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
               equal_int(pos s x, neg 0()) -> false(),
               equal_int(pos s x, neg s y) -> false(),
               equal_int(neg 0(), pos 0()) -> true(),
               equal_int(neg 0(), pos s y) -> false(),
               equal_int(neg 0(), neg 0()) -> true(),
               equal_int(neg 0(), neg s y) -> false(),
               equal_int(neg s x, pos 0()) -> false(),
               equal_int(neg s x, pos s y) -> false(),
               equal_int(neg s x, neg 0()) -> false(),
               equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
                     mod_int(pos x, pos y) -> pos mod_nat(x, y),
                     mod_int(pos x, neg y) -> pos mod_nat(x, y),
                     mod_int(neg x, pos y) -> neg mod_nat(x, y),
                     mod_int(neg x, neg y) -> neg mod_nat(x, y),
                          mult_nat(0(), y) -> 0(),
                        mult_nat(s x, 0()) -> 0(),
                        mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                          plus_nat(0(), x) -> x,
                          plus_nat(s x, y) -> s plus_nat(x, y),
                         div_nat(0(), s y) -> 0(),
                         div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                          if(true(), x, y) -> x,
                         if(false(), x, y) -> y,
             greatereq_int(pos x, pos 0()) -> true(),
               greatereq_int(pos x, neg y) -> true(),
           greatereq_int(pos 0(), pos s y) -> false(),
           greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
             greatereq_int(neg x, pos s y) -> false(),
           greatereq_int(neg 0(), pos 0()) -> true(),
             greatereq_int(neg 0(), neg y) -> true(),
           greatereq_int(neg s x, pos 0()) -> false(),
           greatereq_int(neg s x, neg 0()) -> false(),
           greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
                       minus_nat_s(x, 0()) -> x,
                     minus_nat_s(0(), s y) -> 0(),
                     minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                         mod_nat(0(), s x) -> 0(),
                         mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x)}
          UR:
           {}
           ARCTIC:
            Argument Filtering:
             pi(neg) = 0, pi(s) = [0], pi(greater_int#) = 1
            Usable Rules:
             {}
            Interpretation:
             [s](x0) = 1x0
            Strict:
             {}
            Weak:
             {}
            Qed
         SCC:
          Strict:
           {greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y)}
          Weak:
          {               halfExp(b, e, r) -> condLoop(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r),
                    mult_int(pos x, pos y) -> pos mult_nat(x, y),
                    mult_int(pos x, neg y) -> neg mult_nat(x, y),
                    mult_int(neg x, pos y) -> neg mult_nat(x, y),
                    mult_int(neg x, neg y) -> pos mult_nat(x, y),
                           sqBase(b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                  condMod(true(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)),
                 condMod(false(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                 condLoop(true(), b, e, r) -> condMod(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r),
                condLoop(false(), b, e, r) -> r,
             greater_int(pos 0(), pos 0()) -> false(),
             greater_int(pos 0(), pos s y) -> false(),
             greater_int(pos 0(), neg 0()) -> false(),
             greater_int(pos 0(), neg s y) -> true(),
             greater_int(pos s x, pos 0()) -> true(),
             greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
             greater_int(pos s x, neg 0()) -> true(),
             greater_int(pos s x, neg s y) -> true(),
             greater_int(neg 0(), pos 0()) -> false(),
             greater_int(neg 0(), pos s y) -> false(),
             greater_int(neg 0(), neg 0()) -> false(),
             greater_int(neg 0(), neg s y) -> true(),
             greater_int(neg s x, pos 0()) -> false(),
             greater_int(neg s x, pos s y) -> false(),
             greater_int(neg s x, neg 0()) -> false(),
             greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                   div_int(pos x, pos s y) -> pos div_nat(x, s y),
                   div_int(pos x, neg s y) -> neg div_nat(x, s y),
                   div_int(neg x, pos s y) -> neg div_nat(x, s y),
                   div_int(neg x, neg s y) -> pos div_nat(x, s y),
                                 pow(b, e) -> condLoop(greater_int(e, pos 0()), b, e, pos s 0()),
               equal_int(pos 0(), pos 0()) -> true(),
               equal_int(pos 0(), pos s y) -> false(),
               equal_int(pos 0(), neg 0()) -> true(),
               equal_int(pos 0(), neg s y) -> false(),
               equal_int(pos s x, pos 0()) -> false(),
               equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
               equal_int(pos s x, neg 0()) -> false(),
               equal_int(pos s x, neg s y) -> false(),
               equal_int(neg 0(), pos 0()) -> true(),
               equal_int(neg 0(), pos s y) -> false(),
               equal_int(neg 0(), neg 0()) -> true(),
               equal_int(neg 0(), neg s y) -> false(),
               equal_int(neg s x, pos 0()) -> false(),
               equal_int(neg s x, pos s y) -> false(),
               equal_int(neg s x, neg 0()) -> false(),
               equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
                     mod_int(pos x, pos y) -> pos mod_nat(x, y),
                     mod_int(pos x, neg y) -> pos mod_nat(x, y),
                     mod_int(neg x, pos y) -> neg mod_nat(x, y),
                     mod_int(neg x, neg y) -> neg mod_nat(x, y),
                          mult_nat(0(), y) -> 0(),
                        mult_nat(s x, 0()) -> 0(),
                        mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                          plus_nat(0(), x) -> x,
                          plus_nat(s x, y) -> s plus_nat(x, y),
                         div_nat(0(), s y) -> 0(),
                         div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                          if(true(), x, y) -> x,
                         if(false(), x, y) -> y,
             greatereq_int(pos x, pos 0()) -> true(),
               greatereq_int(pos x, neg y) -> true(),
           greatereq_int(pos 0(), pos s y) -> false(),
           greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
             greatereq_int(neg x, pos s y) -> false(),
           greatereq_int(neg 0(), pos 0()) -> true(),
             greatereq_int(neg 0(), neg y) -> true(),
           greatereq_int(neg s x, pos 0()) -> false(),
           greatereq_int(neg s x, neg 0()) -> false(),
           greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
                       minus_nat_s(x, 0()) -> x,
                     minus_nat_s(0(), s y) -> 0(),
                     minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                         mod_nat(0(), s x) -> 0(),
                         mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x)}
          UR:
           {}
           ARCTIC:
            Argument Filtering:
             pi(s) = [0], pi(pos) = [0], pi(greater_int#) = [1]
            Usable Rules:
             {}
            Interpretation:
             [s](x0) = 5x0 + 9,
             
             [pos](x0) = -4x0 + 0,
             
             [greater_int#](x0) = -4x0 + 0
            Strict:
             {}
            Weak:
             {}
            Qed
         SCC:
          Strict:
           { condMod#(true(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)),
            condMod#(false(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
             condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r)}
          Weak:
          {               halfExp(b, e, r) -> condLoop(greater_int(e, pos 0()), b, div_int(e, pos s s 0()), r),
                    mult_int(pos x, pos y) -> pos mult_nat(x, y),
                    mult_int(pos x, neg y) -> neg mult_nat(x, y),
                    mult_int(neg x, pos y) -> neg mult_nat(x, y),
                    mult_int(neg x, neg y) -> pos mult_nat(x, y),
                           sqBase(b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                  condMod(true(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b)),
                 condMod(false(), b, e, r) -> condLoop(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r),
                 condLoop(true(), b, e, r) -> condMod(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r),
                condLoop(false(), b, e, r) -> r,
             greater_int(pos 0(), pos 0()) -> false(),
             greater_int(pos 0(), pos s y) -> false(),
             greater_int(pos 0(), neg 0()) -> false(),
             greater_int(pos 0(), neg s y) -> true(),
             greater_int(pos s x, pos 0()) -> true(),
             greater_int(pos s x, pos s y) -> greater_int(pos x, pos y),
             greater_int(pos s x, neg 0()) -> true(),
             greater_int(pos s x, neg s y) -> true(),
             greater_int(neg 0(), pos 0()) -> false(),
             greater_int(neg 0(), pos s y) -> false(),
             greater_int(neg 0(), neg 0()) -> false(),
             greater_int(neg 0(), neg s y) -> true(),
             greater_int(neg s x, pos 0()) -> false(),
             greater_int(neg s x, pos s y) -> false(),
             greater_int(neg s x, neg 0()) -> false(),
             greater_int(neg s x, neg s y) -> greater_int(neg x, neg y),
                   div_int(pos x, pos s y) -> pos div_nat(x, s y),
                   div_int(pos x, neg s y) -> neg div_nat(x, s y),
                   div_int(neg x, pos s y) -> neg div_nat(x, s y),
                   div_int(neg x, neg s y) -> pos div_nat(x, s y),
                                 pow(b, e) -> condLoop(greater_int(e, pos 0()), b, e, pos s 0()),
               equal_int(pos 0(), pos 0()) -> true(),
               equal_int(pos 0(), pos s y) -> false(),
               equal_int(pos 0(), neg 0()) -> true(),
               equal_int(pos 0(), neg s y) -> false(),
               equal_int(pos s x, pos 0()) -> false(),
               equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
               equal_int(pos s x, neg 0()) -> false(),
               equal_int(pos s x, neg s y) -> false(),
               equal_int(neg 0(), pos 0()) -> true(),
               equal_int(neg 0(), pos s y) -> false(),
               equal_int(neg 0(), neg 0()) -> true(),
               equal_int(neg 0(), neg s y) -> false(),
               equal_int(neg s x, pos 0()) -> false(),
               equal_int(neg s x, pos s y) -> false(),
               equal_int(neg s x, neg 0()) -> false(),
               equal_int(neg s x, neg s y) -> equal_int(neg x, neg y),
                     mod_int(pos x, pos y) -> pos mod_nat(x, y),
                     mod_int(pos x, neg y) -> pos mod_nat(x, y),
                     mod_int(neg x, pos y) -> neg mod_nat(x, y),
                     mod_int(neg x, neg y) -> neg mod_nat(x, y),
                          mult_nat(0(), y) -> 0(),
                        mult_nat(s x, 0()) -> 0(),
                        mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                          plus_nat(0(), x) -> x,
                          plus_nat(s x, y) -> s plus_nat(x, y),
                         div_nat(0(), s y) -> 0(),
                         div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                          if(true(), x, y) -> x,
                         if(false(), x, y) -> y,
             greatereq_int(pos x, pos 0()) -> true(),
               greatereq_int(pos x, neg y) -> true(),
           greatereq_int(pos 0(), pos s y) -> false(),
           greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
             greatereq_int(neg x, pos s y) -> false(),
           greatereq_int(neg 0(), pos 0()) -> true(),
             greatereq_int(neg 0(), neg y) -> true(),
           greatereq_int(neg s x, pos 0()) -> false(),
           greatereq_int(neg s x, neg 0()) -> false(),
           greatereq_int(neg s x, neg s y) -> greatereq_int(neg x, neg y),
                       minus_nat_s(x, 0()) -> x,
                     minus_nat_s(0(), s y) -> 0(),
                     minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                         mod_nat(0(), s x) -> 0(),
                         mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x)}
          UR:
           {         mult_int(pos x, pos y) -> pos mult_nat(x, y),
                     mult_int(pos x, neg y) -> neg mult_nat(x, y),
                     mult_int(neg x, pos y) -> neg mult_nat(x, y),
                     mult_int(neg x, neg y) -> pos mult_nat(x, y),
              greater_int(pos 0(), pos 0()) -> false(),
              greater_int(pos s x, pos 0()) -> true(),
              greater_int(neg 0(), pos 0()) -> false(),
              greater_int(neg s x, pos 0()) -> false(),
                    div_int(pos x, pos s y) -> pos div_nat(x, s y),
                    div_int(neg x, pos s y) -> neg div_nat(x, s y),
                equal_int(pos 0(), pos 0()) -> true(),
                equal_int(pos 0(), pos s y) -> false(),
                equal_int(pos s x, pos 0()) -> false(),
                equal_int(pos s x, pos s y) -> equal_int(pos x, pos y),
                equal_int(neg 0(), pos s y) -> false(),
                equal_int(neg s x, pos s y) -> false(),
                      mod_int(pos x, pos y) -> pos mod_nat(x, y),
                      mod_int(neg x, pos y) -> neg mod_nat(x, y),
                           mult_nat(0(), y) -> 0(),
                         mult_nat(s x, 0()) -> 0(),
                         mult_nat(s x, s y) -> plus_nat(mult_nat(x, s y), s y),
                           plus_nat(0(), x) -> x,
                           plus_nat(s x, y) -> s plus_nat(x, y),
                          div_nat(0(), s y) -> 0(),
                          div_nat(s x, s y) -> if(greatereq_int(pos x, pos y), div_nat(minus_nat_s(x, y), s y), 0()),
                           if(true(), x, y) -> x,
                          if(false(), x, y) -> y,
              greatereq_int(pos x, pos 0()) -> true(),
            greatereq_int(pos 0(), pos s y) -> false(),
            greatereq_int(pos s x, pos s y) -> greatereq_int(pos x, pos y),
                        minus_nat_s(x, 0()) -> x,
                      minus_nat_s(0(), s y) -> 0(),
                      minus_nat_s(s x, s y) -> minus_nat_s(x, y),
                          mod_nat(0(), s x) -> 0(),
                          mod_nat(s x, s y) -> if(greatereq_int(pos x, pos y), mod_nat(minus_nat_s(x, y), s y), s x),
                                    a(v, u) -> v,
                                    a(v, u) -> u}
           POLY:
            Mode: weak, max_in=7, output_bits=5, dnum=1, ur=true
            Interpretation:
             [if](x0, x1, x2) = 4x0 + x1,
             
             [mult_int](x0, x1) = 0,
             
             [greater_int](x0, x1) = x0,
             
             [div_int](x0, x1) = 0,
             
             [equal_int](x0, x1) = 0,
             
             [mod_int](x0, x1) = 0,
             
             [mult_nat](x0, x1) = 0,
             
             [plus_nat](x0, x1) = 0,
             
             [div_nat](x0, x1) = 0,
             
             [greatereq_int](x0, x1) = x0,
             
             [minus_nat_s](x0, x1) = 0,
             
             [mod_nat](x0, x1) = 0,
             
             [a](x0, x1) = 0,
             
             [pos](x0) = 4x0,
             
             [s](x0) = 4,
             
             [neg](x0) = 4x0,
             
             [true] = 1,
             
             [0] = 0,
             
             [false] = 0,
             
             [condMod#](x0, x1, x2, x3) = x0 + 1,
             
             [condLoop#](x0, x1, x2, x3) = x0 + x1
            Strict:
             condLoop#(true(), b, e, r) -> condMod#(equal_int(mod_int(e, pos s s 0()), pos s 0()), b, e, r)
             1 + 0b + 1e + 0r >= 1 + 0b + 1e + 0r
             condMod#(false(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), r)
             1 + 0b + 1e + 0r >= 0 + 0b + 1e + 0r
             condMod#(true(), b, e, r) -> condLoop#(greater_int(e, pos 0()), mult_int(b, b), div_int(e, pos s s 0()), mult_int(r, b))
             1 + 0b + 1e + 0r >= 0 + 0b + 1e + 0r
            Weak:
             
           SCCS (0):
            
            Qed