Time: 4.807610
TRS:
 {                     app(nil(), zs) -> zs,
                 app(cons(x, ys), zs) -> cons(x, app(ys, zs)),
                     qsort ins(x, ys) -> if_3(split(x, ys), x, ys),
                            qsort e() -> nil(),
            if_3(pair(yl, yh), x, ys) -> app(qsort yl, cons(x, qsort yh)),
  Cond_if_1(true(), zl, zh, x, y, zs) -> pair(ins(y, zl), zh),
        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),
         if_1(pair(zl, zh), x, y, zs) -> Cond_if_1(greater_int(x, y), zl, zh, x, y, zs),
                 split(x, ins(y, zs)) -> Cond_split(greater_int(x, y), x, y, zs),
                 split(x, ins(y, zs)) -> Cond_split1(greatereq_int(y, x), x, y, zs),
                        split(x, e()) -> pair(e(), e()),
  Cond_if_2(true(), zl, zh, x, y, zs) -> pair(zl, ins(y, zh)),
        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),
         if_2(pair(zl, zh), x, y, zs) -> Cond_if_2(greatereq_int(y, x), zl, zh, x, y, zs),
         Cond_split(true(), x, y, zs) -> if_1(split(x, zs), x, y, zs),
        Cond_split1(true(), x, y, zs) -> if_2(split(x, zs), x, y, zs)}
 SRS: We consider a TRS.
  Trs:
   {                     app(nil(), zs) -> zs,
                   app(cons(x, ys), zs) -> cons(x, app(ys, zs)),
                       qsort ins(x, ys) -> if_3(split(x, ys), x, ys),
                              qsort e() -> nil(),
              if_3(pair(yl, yh), x, ys) -> app(qsort yl, cons(x, qsort yh)),
    Cond_if_1(true(), zl, zh, x, y, zs) -> pair(ins(y, zl), zh),
          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),
           if_1(pair(zl, zh), x, y, zs) -> Cond_if_1(greater_int(x, y), zl, zh, x, y, zs),
                   split(x, ins(y, zs)) -> Cond_split(greater_int(x, y), x, y, zs),
                   split(x, ins(y, zs)) -> Cond_split1(greatereq_int(y, x), x, y, zs),
                          split(x, e()) -> pair(e(), e()),
    Cond_if_2(true(), zl, zh, x, y, zs) -> pair(zl, ins(y, zh)),
          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),
           if_2(pair(zl, zh), x, y, zs) -> Cond_if_2(greatereq_int(y, x), zl, zh, x, y, zs),
           Cond_split(true(), x, y, zs) -> if_1(split(x, zs), x, y, zs),
          Cond_split1(true(), x, y, zs) -> if_2(split(x, zs), x, y, zs)}
  APP: We consider a non-applicative system.
   Trs:
    {                     app(nil(), zs) -> zs,
                    app(cons(x, ys), zs) -> cons(x, app(ys, zs)),
                        qsort ins(x, ys) -> if_3(split(x, ys), x, ys),
                               qsort e() -> nil(),
               if_3(pair(yl, yh), x, ys) -> app(qsort yl, cons(x, qsort yh)),
     Cond_if_1(true(), zl, zh, x, y, zs) -> pair(ins(y, zl), zh),
           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),
            if_1(pair(zl, zh), x, y, zs) -> Cond_if_1(greater_int(x, y), zl, zh, x, y, zs),
                    split(x, ins(y, zs)) -> Cond_split(greater_int(x, y), x, y, zs),
                    split(x, ins(y, zs)) -> Cond_split1(greatereq_int(y, x), x, y, zs),
                           split(x, e()) -> pair(e(), e()),
     Cond_if_2(true(), zl, zh, x, y, zs) -> pair(zl, ins(y, zh)),
           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),
            if_2(pair(zl, zh), x, y, zs) -> Cond_if_2(greatereq_int(y, x), zl, zh, x, y, zs),
            Cond_split(true(), x, y, zs) -> if_1(split(x, zs), x, y, zs),
           Cond_split1(true(), x, y, zs) -> if_2(split(x, zs), x, y, zs)}
   DP:
    DP:
     {       app#(cons(x, ys), zs) -> app#(ys, zs),
                    qsort# ins(x, ys) -> if_3#(split(x, ys), x, ys),
                    qsort# ins(x, ys) -> split#(x, ys),
         if_3#(pair(yl, yh), x, ys) -> app#(qsort yl, cons(x, qsort yh)),
         if_3#(pair(yl, yh), x, ys) -> qsort# yl,
         if_3#(pair(yl, yh), x, ys) -> qsort# yh,
            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),
      if_1#(pair(zl, zh), x, y, zs) -> Cond_if_1#(greater_int(x, y), zl, zh, x, y, zs),
      if_1#(pair(zl, zh), x, y, zs) -> greater_int#(x, y),
               split#(x, ins(y, zs)) -> greater_int#(x, y),
               split#(x, ins(y, zs)) -> greatereq_int#(y, x),
               split#(x, ins(y, zs)) -> Cond_split#(greater_int(x, y), x, y, zs),
               split#(x, ins(y, zs)) -> Cond_split1#(greatereq_int(y, x), x, y, zs),
            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),
      if_2#(pair(zl, zh), x, y, zs) -> Cond_if_2#(greatereq_int(y, x), zl, zh, x, y, zs),
      if_2#(pair(zl, zh), x, y, zs) -> greatereq_int#(y, x),
            Cond_split#(true(), x, y, zs) -> if_1#(split(x, zs), x, y, zs),
            Cond_split#(true(), x, y, zs) -> split#(x, zs),
            Cond_split1#(true(), x, y, zs) -> split#(x, zs),
            Cond_split1#(true(), x, y, zs) -> if_2#(split(x, zs), x, y, zs)}
    TRS:
    {                     app(nil(), zs) -> zs,
                    app(cons(x, ys), zs) -> cons(x, app(ys, zs)),
                        qsort ins(x, ys) -> if_3(split(x, ys), x, ys),
                               qsort e() -> nil(),
               if_3(pair(yl, yh), x, ys) -> app(qsort yl, cons(x, qsort yh)),
     Cond_if_1(true(), zl, zh, x, y, zs) -> pair(ins(y, zl), zh),
           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),
            if_1(pair(zl, zh), x, y, zs) -> Cond_if_1(greater_int(x, y), zl, zh, x, y, zs),
                    split(x, ins(y, zs)) -> Cond_split(greater_int(x, y), x, y, zs),
                    split(x, ins(y, zs)) -> Cond_split1(greatereq_int(y, x), x, y, zs),
                           split(x, e()) -> pair(e(), e()),
     Cond_if_2(true(), zl, zh, x, y, zs) -> pair(zl, ins(y, zh)),
           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),
            if_2(pair(zl, zh), x, y, zs) -> Cond_if_2(greatereq_int(y, x), zl, zh, x, y, zs),
            Cond_split(true(), x, y, zs) -> if_1(split(x, zs), x, y, zs),
           Cond_split1(true(), x, y, zs) -> if_2(split(x, zs), x, y, zs)}
    EDG:
     {(qsort# ins(x, ys) -> split#(x, ys), split#(x, ins(y, zs)) -> Cond_split1#(greatereq_int(y, x), x, y, zs))
      (qsort# ins(x, ys) -> split#(x, ys), split#(x, ins(y, zs)) -> Cond_split#(greater_int(x, y), x, y, zs))
      (qsort# ins(x, ys) -> split#(x, ys), split#(x, ins(y, zs)) -> greatereq_int#(y, x))
      (qsort# ins(x, ys) -> split#(x, ys), split#(x, ins(y, zs)) -> greater_int#(x, y))
      (if_3#(pair(yl, yh), x, ys) -> qsort# yh, qsort# ins(x, ys) -> split#(x, ys))
      (if_3#(pair(yl, yh), x, ys) -> qsort# yh, qsort# ins(x, ys) -> if_3#(split(x, ys), x, ys))
      (Cond_split#(true(), x, y, zs) -> split#(x, zs), split#(x, ins(y, zs)) -> Cond_split1#(greatereq_int(y, x), x, y, zs))
      (Cond_split#(true(), x, y, zs) -> split#(x, zs), split#(x, ins(y, zs)) -> Cond_split#(greater_int(x, y), x, y, zs))
      (Cond_split#(true(), x, y, zs) -> split#(x, zs), split#(x, ins(y, zs)) -> greatereq_int#(y, x))
      (Cond_split#(true(), x, y, zs) -> split#(x, zs), split#(x, ins(y, zs)) -> greater_int#(x, 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))
      (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))
      (split#(x, ins(y, zs)) -> greatereq_int#(y, x), greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y))
      (split#(x, ins(y, zs)) -> greatereq_int#(y, x), 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))
      (if_3#(pair(yl, yh), x, ys) -> app#(qsort yl, cons(x, qsort yh)), app#(cons(x, ys), zs) -> app#(ys, zs))
      (split#(x, ins(y, zs)) -> Cond_split1#(greatereq_int(y, x), x, y, zs), Cond_split1#(true(), x, y, zs) -> if_2#(split(x, zs), x, y, zs))
      (split#(x, ins(y, zs)) -> Cond_split1#(greatereq_int(y, x), x, y, zs), Cond_split1#(true(), x, y, zs) -> split#(x, zs))
      (Cond_split1#(true(), x, y, zs) -> if_2#(split(x, zs), x, y, zs), if_2#(pair(zl, zh), x, y, zs) -> greatereq_int#(y, x))
      (Cond_split1#(true(), x, y, zs) -> if_2#(split(x, zs), x, y, zs), if_2#(pair(zl, zh), x, y, zs) -> Cond_if_2#(greatereq_int(y, x), zl, zh, x, y, zs))
      (split#(x, ins(y, zs)) -> greater_int#(x, y), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
      (split#(x, ins(y, zs)) -> greater_int#(x, y), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
      (if_1#(pair(zl, zh), x, y, zs) -> greater_int#(x, y), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
      (if_1#(pair(zl, zh), x, y, zs) -> greater_int#(x, y), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
      (Cond_split#(true(), x, y, zs) -> if_1#(split(x, zs), x, y, zs), if_1#(pair(zl, zh), x, y, zs) -> Cond_if_1#(greater_int(x, y), zl, zh, x, y, zs))
      (Cond_split#(true(), x, y, zs) -> if_1#(split(x, zs), x, y, zs), if_1#(pair(zl, zh), x, y, zs) -> greater_int#(x, y))
      (split#(x, ins(y, zs)) -> Cond_split#(greater_int(x, y), x, y, zs), Cond_split#(true(), x, y, zs) -> if_1#(split(x, zs), x, y, zs))
      (split#(x, ins(y, zs)) -> Cond_split#(greater_int(x, y), x, y, zs), Cond_split#(true(), x, y, zs) -> split#(x, zs))
      (if_2#(pair(zl, zh), x, y, zs) -> greatereq_int#(y, x), greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y))
      (if_2#(pair(zl, zh), x, y, zs) -> greatereq_int#(y, x), 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))
      (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))
      (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))
      (Cond_split1#(true(), x, y, zs) -> split#(x, zs), split#(x, ins(y, zs)) -> greater_int#(x, y))
      (Cond_split1#(true(), x, y, zs) -> split#(x, zs), split#(x, ins(y, zs)) -> greatereq_int#(y, x))
      (Cond_split1#(true(), x, y, zs) -> split#(x, zs), split#(x, ins(y, zs)) -> Cond_split#(greater_int(x, y), x, y, zs))
      (Cond_split1#(true(), x, y, zs) -> split#(x, zs), split#(x, ins(y, zs)) -> Cond_split1#(greatereq_int(y, x), x, y, zs))
      (app#(cons(x, ys), zs) -> app#(ys, zs), app#(cons(x, ys), zs) -> app#(ys, zs))
      (if_3#(pair(yl, yh), x, ys) -> qsort# yl, qsort# ins(x, ys) -> if_3#(split(x, ys), x, ys))
      (if_3#(pair(yl, yh), x, ys) -> qsort# yl, qsort# ins(x, ys) -> split#(x, ys))
      (qsort# ins(x, ys) -> if_3#(split(x, ys), x, ys), if_3#(pair(yl, yh), x, ys) -> app#(qsort yl, cons(x, qsort yh)))
      (qsort# ins(x, ys) -> if_3#(split(x, ys), x, ys), if_3#(pair(yl, yh), x, ys) -> qsort# yl)
      (qsort# ins(x, ys) -> if_3#(split(x, ys), x, ys), if_3#(pair(yl, yh), x, ys) -> qsort# yh)}
     EDG:
      {(qsort# ins(x, ys) -> split#(x, ys), split#(x, ins(y, zs)) -> Cond_split1#(greatereq_int(y, x), x, y, zs))
       (qsort# ins(x, ys) -> split#(x, ys), split#(x, ins(y, zs)) -> Cond_split#(greater_int(x, y), x, y, zs))
       (qsort# ins(x, ys) -> split#(x, ys), split#(x, ins(y, zs)) -> greatereq_int#(y, x))
       (qsort# ins(x, ys) -> split#(x, ys), split#(x, ins(y, zs)) -> greater_int#(x, y))
       (if_3#(pair(yl, yh), x, ys) -> qsort# yh, qsort# ins(x, ys) -> split#(x, ys))
       (if_3#(pair(yl, yh), x, ys) -> qsort# yh, qsort# ins(x, ys) -> if_3#(split(x, ys), x, ys))
       (Cond_split#(true(), x, y, zs) -> split#(x, zs), split#(x, ins(y, zs)) -> Cond_split1#(greatereq_int(y, x), x, y, zs))
       (Cond_split#(true(), x, y, zs) -> split#(x, zs), split#(x, ins(y, zs)) -> Cond_split#(greater_int(x, y), x, y, zs))
       (Cond_split#(true(), x, y, zs) -> split#(x, zs), split#(x, ins(y, zs)) -> greatereq_int#(y, x))
       (Cond_split#(true(), x, y, zs) -> split#(x, zs), split#(x, ins(y, zs)) -> greater_int#(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))
       (split#(x, ins(y, zs)) -> greatereq_int#(y, x), greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y))
       (split#(x, ins(y, zs)) -> greatereq_int#(y, x), 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))
       (if_3#(pair(yl, yh), x, ys) -> app#(qsort yl, cons(x, qsort yh)), app#(cons(x, ys), zs) -> app#(ys, zs))
       (split#(x, ins(y, zs)) -> Cond_split1#(greatereq_int(y, x), x, y, zs), Cond_split1#(true(), x, y, zs) -> if_2#(split(x, zs), x, y, zs))
       (split#(x, ins(y, zs)) -> Cond_split1#(greatereq_int(y, x), x, y, zs), Cond_split1#(true(), x, y, zs) -> split#(x, zs))
       (Cond_split1#(true(), x, y, zs) -> if_2#(split(x, zs), x, y, zs), if_2#(pair(zl, zh), x, y, zs) -> greatereq_int#(y, x))
       (Cond_split1#(true(), x, y, zs) -> if_2#(split(x, zs), x, y, zs), if_2#(pair(zl, zh), x, y, zs) -> Cond_if_2#(greatereq_int(y, x), zl, zh, x, y, zs))
       (split#(x, ins(y, zs)) -> greater_int#(x, y), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
       (split#(x, ins(y, zs)) -> greater_int#(x, y), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
       (if_1#(pair(zl, zh), x, y, zs) -> greater_int#(x, y), greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y))
       (if_1#(pair(zl, zh), x, y, zs) -> greater_int#(x, y), greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y))
       (Cond_split#(true(), x, y, zs) -> if_1#(split(x, zs), x, y, zs), if_1#(pair(zl, zh), x, y, zs) -> Cond_if_1#(greater_int(x, y), zl, zh, x, y, zs))
       (Cond_split#(true(), x, y, zs) -> if_1#(split(x, zs), x, y, zs), if_1#(pair(zl, zh), x, y, zs) -> greater_int#(x, y))
       (split#(x, ins(y, zs)) -> Cond_split#(greater_int(x, y), x, y, zs), Cond_split#(true(), x, y, zs) -> if_1#(split(x, zs), x, y, zs))
       (split#(x, ins(y, zs)) -> Cond_split#(greater_int(x, y), x, y, zs), Cond_split#(true(), x, y, zs) -> split#(x, zs))
       (if_2#(pair(zl, zh), x, y, zs) -> greatereq_int#(y, x), greatereq_int#(pos s x, pos s y) -> greatereq_int#(pos x, pos y))
       (if_2#(pair(zl, zh), x, y, zs) -> greatereq_int#(y, x), 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))
       (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))
       (Cond_split1#(true(), x, y, zs) -> split#(x, zs), split#(x, ins(y, zs)) -> greater_int#(x, y))
       (Cond_split1#(true(), x, y, zs) -> split#(x, zs), split#(x, ins(y, zs)) -> greatereq_int#(y, x))
       (Cond_split1#(true(), x, y, zs) -> split#(x, zs), split#(x, ins(y, zs)) -> Cond_split#(greater_int(x, y), x, y, zs))
       (Cond_split1#(true(), x, y, zs) -> split#(x, zs), split#(x, ins(y, zs)) -> Cond_split1#(greatereq_int(y, x), x, y, zs))
       (app#(cons(x, ys), zs) -> app#(ys, zs), app#(cons(x, ys), zs) -> app#(ys, zs))
       (if_3#(pair(yl, yh), x, ys) -> qsort# yl, qsort# ins(x, ys) -> if_3#(split(x, ys), x, ys))
       (if_3#(pair(yl, yh), x, ys) -> qsort# yl, qsort# ins(x, ys) -> split#(x, ys))
       (qsort# ins(x, ys) -> if_3#(split(x, ys), x, ys), if_3#(pair(yl, yh), x, ys) -> app#(qsort yl, cons(x, qsort yh)))
       (qsort# ins(x, ys) -> if_3#(split(x, ys), x, ys), if_3#(pair(yl, yh), x, ys) -> qsort# yl)
       (qsort# ins(x, ys) -> if_3#(split(x, ys), x, ys), if_3#(pair(yl, yh), x, ys) -> qsort# yh)}
      SCCS (7):
       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:
        {   split#(x, ins(y, zs)) -> Cond_split#(greater_int(x, y), x, y, zs),
            split#(x, ins(y, zs)) -> Cond_split1#(greatereq_int(y, x), x, y, zs),
         Cond_split#(true(), x, y, zs) -> split#(x, zs),
         Cond_split1#(true(), x, y, zs) -> split#(x, zs)}
       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:
        {           qsort# ins(x, ys) -> if_3#(split(x, ys), x, ys),
         if_3#(pair(yl, yh), x, ys) -> qsort# yl,
         if_3#(pair(yl, yh), x, ys) -> qsort# yh}
       Scc:
        {app#(cons(x, ys), zs) -> app#(ys, zs)}
       SCC:
        Strict:
         {greatereq_int#(neg s x, neg s y) -> greatereq_int#(neg x, neg y)}
        Weak:
        {                     app(nil(), zs) -> zs,
                        app(cons(x, ys), zs) -> cons(x, app(ys, zs)),
                            qsort ins(x, ys) -> if_3(split(x, ys), x, ys),
                                   qsort e() -> nil(),
                   if_3(pair(yl, yh), x, ys) -> app(qsort yl, cons(x, qsort yh)),
         Cond_if_1(true(), zl, zh, x, y, zs) -> pair(ins(y, zl), zh),
               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),
                if_1(pair(zl, zh), x, y, zs) -> Cond_if_1(greater_int(x, y), zl, zh, x, y, zs),
                        split(x, ins(y, zs)) -> Cond_split(greater_int(x, y), x, y, zs),
                        split(x, ins(y, zs)) -> Cond_split1(greatereq_int(y, x), x, y, zs),
                               split(x, e()) -> pair(e(), e()),
         Cond_if_2(true(), zl, zh, x, y, zs) -> pair(zl, ins(y, zh)),
               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),
                if_2(pair(zl, zh), x, y, zs) -> Cond_if_2(greatereq_int(y, x), zl, zh, x, y, zs),
                Cond_split(true(), x, y, zs) -> if_1(split(x, zs), x, y, zs),
               Cond_split1(true(), x, y, zs) -> if_2(split(x, zs), x, y, zs)}
        UR:
         {}
         ARCTIC:
          Argument Filtering:
           pi(s) = [0], pi(neg) = [0], pi(greatereq_int#) = [1]
          Usable Rules:
           {}
          Interpretation:
           [s](x0) = 5x0 + 9,
           
           [neg](x0) = -4x0 + 0,
           
           [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:
        {                     app(nil(), zs) -> zs,
                        app(cons(x, ys), zs) -> cons(x, app(ys, zs)),
                            qsort ins(x, ys) -> if_3(split(x, ys), x, ys),
                                   qsort e() -> nil(),
                   if_3(pair(yl, yh), x, ys) -> app(qsort yl, cons(x, qsort yh)),
         Cond_if_1(true(), zl, zh, x, y, zs) -> pair(ins(y, zl), zh),
               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),
                if_1(pair(zl, zh), x, y, zs) -> Cond_if_1(greater_int(x, y), zl, zh, x, y, zs),
                        split(x, ins(y, zs)) -> Cond_split(greater_int(x, y), x, y, zs),
                        split(x, ins(y, zs)) -> Cond_split1(greatereq_int(y, x), x, y, zs),
                               split(x, e()) -> pair(e(), e()),
         Cond_if_2(true(), zl, zh, x, y, zs) -> pair(zl, ins(y, zh)),
               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),
                if_2(pair(zl, zh), x, y, zs) -> Cond_if_2(greatereq_int(y, x), zl, zh, x, y, zs),
                Cond_split(true(), x, y, zs) -> if_1(split(x, zs), x, y, zs),
               Cond_split1(true(), x, y, zs) -> if_2(split(x, zs), x, y, zs)}
        UR:
         {}
         ARCTIC:
          Argument Filtering:
           pi(s) = [0], pi(pos) = [0], pi(greatereq_int#) = [1]
          Usable Rules:
           {}
          Interpretation:
           [s](x0) = 5x0 + 9,
           
           [pos](x0) = -4x0 + 0,
           
           [greatereq_int#](x0) = -4x0 + 0
          Strict:
           {}
          Weak:
           {}
          Qed
       SCC:
        Strict:
         {   split#(x, ins(y, zs)) -> Cond_split#(greater_int(x, y), x, y, zs),
             split#(x, ins(y, zs)) -> Cond_split1#(greatereq_int(y, x), x, y, zs),
          Cond_split#(true(), x, y, zs) -> split#(x, zs),
          Cond_split1#(true(), x, y, zs) -> split#(x, zs)}
        Weak:
        {                     app(nil(), zs) -> zs,
                        app(cons(x, ys), zs) -> cons(x, app(ys, zs)),
                            qsort ins(x, ys) -> if_3(split(x, ys), x, ys),
                                   qsort e() -> nil(),
                   if_3(pair(yl, yh), x, ys) -> app(qsort yl, cons(x, qsort yh)),
         Cond_if_1(true(), zl, zh, x, y, zs) -> pair(ins(y, zl), zh),
               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),
                if_1(pair(zl, zh), x, y, zs) -> Cond_if_1(greater_int(x, y), zl, zh, x, y, zs),
                        split(x, ins(y, zs)) -> Cond_split(greater_int(x, y), x, y, zs),
                        split(x, ins(y, zs)) -> Cond_split1(greatereq_int(y, x), x, y, zs),
                               split(x, e()) -> pair(e(), e()),
         Cond_if_2(true(), zl, zh, x, y, zs) -> pair(zl, ins(y, zh)),
               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),
                if_2(pair(zl, zh), x, y, zs) -> Cond_if_2(greatereq_int(y, x), zl, zh, x, y, zs),
                Cond_split(true(), x, y, zs) -> if_1(split(x, zs), x, y, zs),
               Cond_split1(true(), x, y, zs) -> if_2(split(x, zs), x, y, zs)}
        SPSC:
         Simple Projection:
          pi(Cond_split1#) = 3, pi(Cond_split#) = 3, pi(split#) = 1
         Strict:
          {   split#(x, ins(y, zs)) -> Cond_split1#(greatereq_int(y, x), x, y, zs),
           Cond_split#(true(), x, y, zs) -> split#(x, zs),
           Cond_split1#(true(), x, y, zs) -> split#(x, zs)}
         SCCS (1):
          Scc:
           {   split#(x, ins(y, zs)) -> Cond_split1#(greatereq_int(y, x), x, y, zs),
            Cond_split1#(true(), x, y, zs) -> split#(x, zs)}
          SCC:
           Strict:
            {   split#(x, ins(y, zs)) -> Cond_split1#(greatereq_int(y, x), x, y, zs),
             Cond_split1#(true(), x, y, zs) -> split#(x, zs)}
           Weak:
           {                     app(nil(), zs) -> zs,
                           app(cons(x, ys), zs) -> cons(x, app(ys, zs)),
                               qsort ins(x, ys) -> if_3(split(x, ys), x, ys),
                                      qsort e() -> nil(),
                      if_3(pair(yl, yh), x, ys) -> app(qsort yl, cons(x, qsort yh)),
            Cond_if_1(true(), zl, zh, x, y, zs) -> pair(ins(y, zl), zh),
                  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),
                   if_1(pair(zl, zh), x, y, zs) -> Cond_if_1(greater_int(x, y), zl, zh, x, y, zs),
                           split(x, ins(y, zs)) -> Cond_split(greater_int(x, y), x, y, zs),
                           split(x, ins(y, zs)) -> Cond_split1(greatereq_int(y, x), x, y, zs),
                                  split(x, e()) -> pair(e(), e()),
            Cond_if_2(true(), zl, zh, x, y, zs) -> pair(zl, ins(y, zh)),
                  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),
                   if_2(pair(zl, zh), x, y, zs) -> Cond_if_2(greatereq_int(y, x), zl, zh, x, y, zs),
                   Cond_split(true(), x, y, zs) -> if_1(split(x, zs), x, y, zs),
                  Cond_split1(true(), x, y, zs) -> if_2(split(x, zs), x, y, zs)}
           SPSC:
            Simple Projection:
             pi(Cond_split1#) = 3, pi(split#) = 1
            Strict:
             {Cond_split1#(true(), x, y, zs) -> split#(x, zs)}
            SCCS (0):
             
             Qed
       SCC:
        Strict:
         {greater_int#(neg s x, neg s y) -> greater_int#(neg x, neg y)}
        Weak:
        {                     app(nil(), zs) -> zs,
                        app(cons(x, ys), zs) -> cons(x, app(ys, zs)),
                            qsort ins(x, ys) -> if_3(split(x, ys), x, ys),
                                   qsort e() -> nil(),
                   if_3(pair(yl, yh), x, ys) -> app(qsort yl, cons(x, qsort yh)),
         Cond_if_1(true(), zl, zh, x, y, zs) -> pair(ins(y, zl), zh),
               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),
                if_1(pair(zl, zh), x, y, zs) -> Cond_if_1(greater_int(x, y), zl, zh, x, y, zs),
                        split(x, ins(y, zs)) -> Cond_split(greater_int(x, y), x, y, zs),
                        split(x, ins(y, zs)) -> Cond_split1(greatereq_int(y, x), x, y, zs),
                               split(x, e()) -> pair(e(), e()),
         Cond_if_2(true(), zl, zh, x, y, zs) -> pair(zl, ins(y, zh)),
               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),
                if_2(pair(zl, zh), x, y, zs) -> Cond_if_2(greatereq_int(y, x), zl, zh, x, y, zs),
                Cond_split(true(), x, y, zs) -> if_1(split(x, zs), x, y, zs),
               Cond_split1(true(), x, y, zs) -> if_2(split(x, zs), x, y, zs)}
        UR:
         {}
         ARCTIC:
          Argument Filtering:
           pi(s) = [0], pi(neg) = [0], pi(greater_int#) = [1]
          Usable Rules:
           {}
          Interpretation:
           [s](x0) = 5x0 + 9,
           
           [neg](x0) = -4x0 + 0,
           
           [greater_int#](x0) = -4x0 + 0
          Strict:
           {}
          Weak:
           {}
          Qed
       SCC:
        Strict:
         {greater_int#(pos s x, pos s y) -> greater_int#(pos x, pos y)}
        Weak:
        {                     app(nil(), zs) -> zs,
                        app(cons(x, ys), zs) -> cons(x, app(ys, zs)),
                            qsort ins(x, ys) -> if_3(split(x, ys), x, ys),
                                   qsort e() -> nil(),
                   if_3(pair(yl, yh), x, ys) -> app(qsort yl, cons(x, qsort yh)),
         Cond_if_1(true(), zl, zh, x, y, zs) -> pair(ins(y, zl), zh),
               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),
                if_1(pair(zl, zh), x, y, zs) -> Cond_if_1(greater_int(x, y), zl, zh, x, y, zs),
                        split(x, ins(y, zs)) -> Cond_split(greater_int(x, y), x, y, zs),
                        split(x, ins(y, zs)) -> Cond_split1(greatereq_int(y, x), x, y, zs),
                               split(x, e()) -> pair(e(), e()),
         Cond_if_2(true(), zl, zh, x, y, zs) -> pair(zl, ins(y, zh)),
               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),
                if_2(pair(zl, zh), x, y, zs) -> Cond_if_2(greatereq_int(y, x), zl, zh, x, y, zs),
                Cond_split(true(), x, y, zs) -> if_1(split(x, zs), x, y, zs),
               Cond_split1(true(), x, y, zs) -> if_2(split(x, zs), x, y, zs)}
        UR:
         {}
         ARCTIC:
          Argument Filtering:
           pi(s) = [0], pi(pos) = 0, pi(greater_int#) = 1
          Usable Rules:
           {}
          Interpretation:
           [s](x0) = 1x0
          Strict:
           {}
          Weak:
           {}
          Qed
       SCC:
        Strict:
         {           qsort# ins(x, ys) -> if_3#(split(x, ys), x, ys),
          if_3#(pair(yl, yh), x, ys) -> qsort# yl,
          if_3#(pair(yl, yh), x, ys) -> qsort# yh}
        Weak:
        {                     app(nil(), zs) -> zs,
                        app(cons(x, ys), zs) -> cons(x, app(ys, zs)),
                            qsort ins(x, ys) -> if_3(split(x, ys), x, ys),
                                   qsort e() -> nil(),
                   if_3(pair(yl, yh), x, ys) -> app(qsort yl, cons(x, qsort yh)),
         Cond_if_1(true(), zl, zh, x, y, zs) -> pair(ins(y, zl), zh),
               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),
                if_1(pair(zl, zh), x, y, zs) -> Cond_if_1(greater_int(x, y), zl, zh, x, y, zs),
                        split(x, ins(y, zs)) -> Cond_split(greater_int(x, y), x, y, zs),
                        split(x, ins(y, zs)) -> Cond_split1(greatereq_int(y, x), x, y, zs),
                               split(x, e()) -> pair(e(), e()),
         Cond_if_2(true(), zl, zh, x, y, zs) -> pair(zl, ins(y, zh)),
               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),
                if_2(pair(zl, zh), x, y, zs) -> Cond_if_2(greatereq_int(y, x), zl, zh, x, y, zs),
                Cond_split(true(), x, y, zs) -> if_1(split(x, zs), x, y, zs),
               Cond_split1(true(), x, y, zs) -> if_2(split(x, zs), x, y, zs)}
        UR:
         {Cond_if_1(true(), zl, zh, x, y, zs) -> pair(ins(y, zl), zh),
                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),
                 if_1(pair(zl, zh), x, y, zs) -> Cond_if_1(greater_int(x, y), zl, zh, x, y, zs),
                         split(x, ins(y, zs)) -> Cond_split(greater_int(x, y), x, y, zs),
                         split(x, ins(y, zs)) -> Cond_split1(greatereq_int(y, x), x, y, zs),
                                split(x, e()) -> pair(e(), e()),
          Cond_if_2(true(), zl, zh, x, y, zs) -> pair(zl, ins(y, zh)),
                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),
                 if_2(pair(zl, zh), x, y, zs) -> Cond_if_2(greatereq_int(y, x), zl, zh, x, y, zs),
                 Cond_split(true(), x, y, zs) -> if_1(split(x, zs), x, y, zs),
                Cond_split1(true(), x, y, zs) -> if_2(split(x, zs), x, y, zs),
                                      a(z, w) -> z,
                                      a(z, w) -> w}
         POLY:
          Mode: weak, max_in=7, output_bits=5, dnum=1, ur=true
          Interpretation:
           [Cond_if_1](x0, x1, x2, x3, x4, x5) = x0 + 3x1 + 2x2 + 4x3 + 1,
           
           [Cond_if_2](x0, x1, x2, x3, x4, x5) = x0 + 3x1 + 4x2 + 7,
           
           [if_1](x0, x1, x2, x3) = 3x0 + 6x1 + 1,
           
           [if_2](x0, x1, x2, x3) = 3x0 + 4x1 + 7,
           
           [Cond_split](x0, x1, x2, x3) = x0 + 6x1 + 6x2 + 6,
           
           [Cond_split1](x0, x1, x2, x3) = 2x0 + 4x1 + 6x2 + 5,
           
           [pair](x0, x1) = x0 + x1,
           
           [greater_int](x0, x1) = 2x0,
           
           [split](x0, x1) = 2x0 + 4,
           
           [ins](x0, x1) = 4x0 + 3x1 + 7,
           
           [greatereq_int](x0, x1) = x0,
           
           [a](x0, x1) = 0,
           
           [pos](x0) = x0 + 7,
           
           [neg](x0) = 2x0 + 4,
           
           [s](x0) = 4x0 + 2,
           
           [true] = 7,
           
           [e] = 6,
           
           [false] = 0,
           
           [0] = 2,
           
           [if_3#](x0, x1, x2) = 4x0 + 4x1 + 5,
           
           [qsort#](x0) = 3x0 + 5
          Strict:
           if_3#(pair(yl, yh), x, ys) -> qsort# yh
           5 + 4yl + 4x + 4yh + 0ys >= 5 + 3yh
           if_3#(pair(yl, yh), x, ys) -> qsort# yl
           5 + 4yl + 4x + 4yh + 0ys >= 5 + 3yl
           qsort# ins(x, ys) -> if_3#(split(x, ys), x, ys)
           26 + 12x + 9ys >= 21 + 4x + 8ys
          Weak:
           
         SCCS (0):
          
          Qed
      SCC:
       Strict:
        {app#(cons(x, ys), zs) -> app#(ys, zs)}
       Weak:
       {                     app(nil(), zs) -> zs,
                       app(cons(x, ys), zs) -> cons(x, app(ys, zs)),
                           qsort ins(x, ys) -> if_3(split(x, ys), x, ys),
                                  qsort e() -> nil(),
                  if_3(pair(yl, yh), x, ys) -> app(qsort yl, cons(x, qsort yh)),
        Cond_if_1(true(), zl, zh, x, y, zs) -> pair(ins(y, zl), zh),
              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),
               if_1(pair(zl, zh), x, y, zs) -> Cond_if_1(greater_int(x, y), zl, zh, x, y, zs),
                       split(x, ins(y, zs)) -> Cond_split(greater_int(x, y), x, y, zs),
                       split(x, ins(y, zs)) -> Cond_split1(greatereq_int(y, x), x, y, zs),
                              split(x, e()) -> pair(e(), e()),
        Cond_if_2(true(), zl, zh, x, y, zs) -> pair(zl, ins(y, zh)),
              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),
               if_2(pair(zl, zh), x, y, zs) -> Cond_if_2(greatereq_int(y, x), zl, zh, x, y, zs),
               Cond_split(true(), x, y, zs) -> if_1(split(x, zs), x, y, zs),
              Cond_split1(true(), x, y, zs) -> if_2(split(x, zs), x, y, zs)}
       SPSC:
        Simple Projection:
         pi(app#) = 0
        Strict:
         {}
        Qed