MAYBE
TRS:
 {               if(true(), x, y) -> averIter(y, x, y),
                if(false(), x, y) -> averIter(x, y, x),
                       ge(x, 0()) -> true(),
                   ge(s(x), s(y)) -> ge(x, y),
                    ge(0(), s(y)) -> false(),
                    average(x, y) -> if(ge(x, y), x, y),
                averIter(x, y, z) -> ifIter(ge(x, y), x, y, z),
          ifIter(true(), x, y, z) -> z,
         ifIter(false(), x, y, z) -> averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))),
                    plus(s(x), y) -> s(plus(x, y)),
                     plus(0(), y) -> y,
                 append(nil(), y) -> y,
            append(cons(n, x), y) -> cons(n, app(x, y)),
                    low(n, nil()) -> nil(),
               low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)),
    if_low(true(), n, cons(m, x)) -> low(n, x),
   if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)),
                   high(n, nil()) -> nil(),
              high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)),
   if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)),
  if_high(false(), n, cons(m, x)) -> high(n, x),
               ifquick(true(), x) -> nil(),
              ifquick(false(), x) -> append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))),
                   isempty(nil()) -> true(),
              isempty(cons(n, x)) -> false(),
                     quicksort(x) -> ifquick(isempty(x), x),
                      head(nil()) -> error(),
                 head(cons(n, x)) -> n,
                      tail(nil()) -> nil(),
                 tail(cons(n, x)) -> x,
                              a() -> b(),
                              a() -> c()}
 DP:
  Strict:
   {               if#(true(), x, y) -> averIter#(y, x, y),
                  if#(false(), x, y) -> averIter#(x, y, x),
                     ge#(s(x), s(y)) -> ge#(x, y),
                      average#(x, y) -> if#(ge(x, y), x, y),
                      average#(x, y) -> ge#(x, y),
                  averIter#(x, y, z) -> ge#(x, y),
                  averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z),
           ifIter#(false(), x, y, z) -> averIter#(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))),
           ifIter#(false(), x, y, z) -> plus#(x, s(s(s(0())))),
           ifIter#(false(), x, y, z) -> plus#(y, s(0())),
           ifIter#(false(), x, y, z) -> plus#(z, s(0())),
                      plus#(s(x), y) -> plus#(x, y),
                 low#(n, cons(m, x)) -> ge#(m, n),
                 low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x)),
      if_low#(true(), n, cons(m, x)) -> low#(n, x),
     if_low#(false(), n, cons(m, x)) -> low#(n, x),
                high#(n, cons(m, x)) -> ge#(m, n),
                high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)),
     if_high#(true(), n, cons(m, x)) -> average#(m, m),
     if_high#(true(), n, cons(m, x)) -> high#(n, x),
    if_high#(false(), n, cons(m, x)) -> high#(n, x),
                ifquick#(false(), x) -> append#(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))),
                ifquick#(false(), x) -> low#(head(x), tail(x)),
                ifquick#(false(), x) -> high#(head(x), tail(x)),
                ifquick#(false(), x) -> quicksort#(low(head(x), tail(x))),
                ifquick#(false(), x) -> quicksort#(high(head(x), tail(x))),
                ifquick#(false(), x) -> head#(x),
                ifquick#(false(), x) -> tail#(x),
                       quicksort#(x) -> ifquick#(isempty(x), x),
                       quicksort#(x) -> isempty#(x)}
  Weak:
  {               if(true(), x, y) -> averIter(y, x, y),
                 if(false(), x, y) -> averIter(x, y, x),
                        ge(x, 0()) -> true(),
                    ge(s(x), s(y)) -> ge(x, y),
                     ge(0(), s(y)) -> false(),
                     average(x, y) -> if(ge(x, y), x, y),
                 averIter(x, y, z) -> ifIter(ge(x, y), x, y, z),
           ifIter(true(), x, y, z) -> z,
          ifIter(false(), x, y, z) -> averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))),
                     plus(s(x), y) -> s(plus(x, y)),
                      plus(0(), y) -> y,
                  append(nil(), y) -> y,
             append(cons(n, x), y) -> cons(n, app(x, y)),
                     low(n, nil()) -> nil(),
                low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)),
     if_low(true(), n, cons(m, x)) -> low(n, x),
    if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)),
                    high(n, nil()) -> nil(),
               high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)),
    if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)),
   if_high(false(), n, cons(m, x)) -> high(n, x),
                ifquick(true(), x) -> nil(),
               ifquick(false(), x) -> append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))),
                    isempty(nil()) -> true(),
               isempty(cons(n, x)) -> false(),
                      quicksort(x) -> ifquick(isempty(x), x),
                       head(nil()) -> error(),
                  head(cons(n, x)) -> n,
                       tail(nil()) -> nil(),
                  tail(cons(n, x)) -> x,
                               a() -> b(),
                               a() -> c()}
  EDG:
   {(ifIter#(false(), x, y, z) -> plus#(y, s(0())), plus#(s(x), y) -> plus#(x, y))
    (ifquick#(false(), x) -> low#(head(x), tail(x)), low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x)))
    (ifquick#(false(), x) -> low#(head(x), tail(x)), low#(n, cons(m, x)) -> ge#(m, n))
    (if#(true(), x, y) -> averIter#(y, x, y), averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z))
    (if#(true(), x, y) -> averIter#(y, x, y), averIter#(x, y, z) -> ge#(x, y))
    (quicksort#(x) -> ifquick#(isempty(x), x), ifquick#(false(), x) -> tail#(x))
    (quicksort#(x) -> ifquick#(isempty(x), x), ifquick#(false(), x) -> head#(x))
    (quicksort#(x) -> ifquick#(isempty(x), x), ifquick#(false(), x) -> quicksort#(high(head(x), tail(x))))
    (quicksort#(x) -> ifquick#(isempty(x), x), ifquick#(false(), x) -> quicksort#(low(head(x), tail(x))))
    (quicksort#(x) -> ifquick#(isempty(x), x), ifquick#(false(), x) -> high#(head(x), tail(x)))
    (quicksort#(x) -> ifquick#(isempty(x), x), ifquick#(false(), x) -> low#(head(x), tail(x)))
    (quicksort#(x) -> ifquick#(isempty(x), x), ifquick#(false(), x) -> append#(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))))
    (low#(n, cons(m, x)) -> ge#(m, n), ge#(s(x), s(y)) -> ge#(x, y))
    (averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z), ifIter#(false(), x, y, z) -> plus#(z, s(0())))
    (averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z), ifIter#(false(), x, y, z) -> plus#(y, s(0())))
    (averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z), ifIter#(false(), x, y, z) -> plus#(x, s(s(s(0())))))
    (averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z), ifIter#(false(), x, y, z) -> averIter#(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))))
    (ge#(s(x), s(y)) -> ge#(x, y), ge#(s(x), s(y)) -> ge#(x, y))
    (averIter#(x, y, z) -> ge#(x, y), ge#(s(x), s(y)) -> ge#(x, y))
    (low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x)), if_low#(false(), n, cons(m, x)) -> low#(n, x))
    (low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x)), if_low#(true(), n, cons(m, x)) -> low#(n, x))
    (if#(false(), x, y) -> averIter#(x, y, x), averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z))
    (if#(false(), x, y) -> averIter#(x, y, x), averIter#(x, y, z) -> ge#(x, y))
    (if_low#(false(), n, cons(m, x)) -> low#(n, x), low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x)))
    (if_low#(false(), n, cons(m, x)) -> low#(n, x), low#(n, cons(m, x)) -> ge#(m, n))
    (if_high#(false(), n, cons(m, x)) -> high#(n, x), high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)))
    (if_high#(false(), n, cons(m, x)) -> high#(n, x), high#(n, cons(m, x)) -> ge#(m, n))
    (ifquick#(false(), x) -> quicksort#(high(head(x), tail(x))), quicksort#(x) -> isempty#(x))
    (ifquick#(false(), x) -> quicksort#(high(head(x), tail(x))), quicksort#(x) -> ifquick#(isempty(x), x))
    (ifquick#(false(), x) -> quicksort#(low(head(x), tail(x))), quicksort#(x) -> ifquick#(isempty(x), x))
    (ifquick#(false(), x) -> quicksort#(low(head(x), tail(x))), quicksort#(x) -> isempty#(x))
    (if_high#(true(), n, cons(m, x)) -> high#(n, x), high#(n, cons(m, x)) -> ge#(m, n))
    (if_high#(true(), n, cons(m, x)) -> high#(n, x), high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)))
    (if_low#(true(), n, cons(m, x)) -> low#(n, x), low#(n, cons(m, x)) -> ge#(m, n))
    (if_low#(true(), n, cons(m, x)) -> low#(n, x), low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x)))
    (high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)), if_high#(true(), n, cons(m, x)) -> average#(m, m))
    (high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)), if_high#(true(), n, cons(m, x)) -> high#(n, x))
    (high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)), if_high#(false(), n, cons(m, x)) -> high#(n, x))
    (plus#(s(x), y) -> plus#(x, y), plus#(s(x), y) -> plus#(x, y))
    (average#(x, y) -> ge#(x, y), ge#(s(x), s(y)) -> ge#(x, y))
    (ifIter#(false(), x, y, z) -> averIter#(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))), averIter#(x, y, z) -> ge#(x, y))
    (ifIter#(false(), x, y, z) -> averIter#(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))), averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z))
    (high#(n, cons(m, x)) -> ge#(m, n), ge#(s(x), s(y)) -> ge#(x, y))
    (if_high#(true(), n, cons(m, x)) -> average#(m, m), average#(x, y) -> if#(ge(x, y), x, y))
    (if_high#(true(), n, cons(m, x)) -> average#(m, m), average#(x, y) -> ge#(x, y))
    (average#(x, y) -> if#(ge(x, y), x, y), if#(true(), x, y) -> averIter#(y, x, y))
    (average#(x, y) -> if#(ge(x, y), x, y), if#(false(), x, y) -> averIter#(x, y, x))
    (ifquick#(false(), x) -> high#(head(x), tail(x)), high#(n, cons(m, x)) -> ge#(m, n))
    (ifquick#(false(), x) -> high#(head(x), tail(x)), high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)))
    (ifIter#(false(), x, y, z) -> plus#(z, s(0())), plus#(s(x), y) -> plus#(x, y))
    (ifIter#(false(), x, y, z) -> plus#(x, s(s(s(0())))), plus#(s(x), y) -> plus#(x, y))}
   SCCS:
    Scc:
     {ifquick#(false(), x) -> quicksort#(low(head(x), tail(x))),
      ifquick#(false(), x) -> quicksort#(high(head(x), tail(x))),
             quicksort#(x) -> ifquick#(isempty(x), x)}
    Scc:
     {            high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)),
       if_high#(true(), n, cons(m, x)) -> high#(n, x),
      if_high#(false(), n, cons(m, x)) -> high#(n, x)}
    Scc:
     {            low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x)),
       if_low#(true(), n, cons(m, x)) -> low#(n, x),
      if_low#(false(), n, cons(m, x)) -> low#(n, x)}
    Scc:
     {plus#(s(x), y) -> plus#(x, y)}
    Scc:
     {       averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z),
      ifIter#(false(), x, y, z) -> averIter#(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0())))}
    Scc:
     {ge#(s(x), s(y)) -> ge#(x, y)}
    SCC:
     Strict:
      {ifquick#(false(), x) -> quicksort#(low(head(x), tail(x))),
       ifquick#(false(), x) -> quicksort#(high(head(x), tail(x))),
              quicksort#(x) -> ifquick#(isempty(x), x)}
     Weak:
     {               if(true(), x, y) -> averIter(y, x, y),
                    if(false(), x, y) -> averIter(x, y, x),
                           ge(x, 0()) -> true(),
                       ge(s(x), s(y)) -> ge(x, y),
                        ge(0(), s(y)) -> false(),
                        average(x, y) -> if(ge(x, y), x, y),
                    averIter(x, y, z) -> ifIter(ge(x, y), x, y, z),
              ifIter(true(), x, y, z) -> z,
             ifIter(false(), x, y, z) -> averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))),
                        plus(s(x), y) -> s(plus(x, y)),
                         plus(0(), y) -> y,
                     append(nil(), y) -> y,
                append(cons(n, x), y) -> cons(n, app(x, y)),
                        low(n, nil()) -> nil(),
                   low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)),
        if_low(true(), n, cons(m, x)) -> low(n, x),
       if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)),
                       high(n, nil()) -> nil(),
                  high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)),
       if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)),
      if_high(false(), n, cons(m, x)) -> high(n, x),
                   ifquick(true(), x) -> nil(),
                  ifquick(false(), x) -> append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))),
                       isempty(nil()) -> true(),
                  isempty(cons(n, x)) -> false(),
                         quicksort(x) -> ifquick(isempty(x), x),
                          head(nil()) -> error(),
                     head(cons(n, x)) -> n,
                          tail(nil()) -> nil(),
                     tail(cons(n, x)) -> x,
                                  a() -> b(),
                                  a() -> c()}
     Fail
    SCC:
     Strict:
      {            high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)),
        if_high#(true(), n, cons(m, x)) -> high#(n, x),
       if_high#(false(), n, cons(m, x)) -> high#(n, x)}
     Weak:
     {               if(true(), x, y) -> averIter(y, x, y),
                    if(false(), x, y) -> averIter(x, y, x),
                           ge(x, 0()) -> true(),
                       ge(s(x), s(y)) -> ge(x, y),
                        ge(0(), s(y)) -> false(),
                        average(x, y) -> if(ge(x, y), x, y),
                    averIter(x, y, z) -> ifIter(ge(x, y), x, y, z),
              ifIter(true(), x, y, z) -> z,
             ifIter(false(), x, y, z) -> averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))),
                        plus(s(x), y) -> s(plus(x, y)),
                         plus(0(), y) -> y,
                     append(nil(), y) -> y,
                append(cons(n, x), y) -> cons(n, app(x, y)),
                        low(n, nil()) -> nil(),
                   low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)),
        if_low(true(), n, cons(m, x)) -> low(n, x),
       if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)),
                       high(n, nil()) -> nil(),
                  high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)),
       if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)),
      if_high(false(), n, cons(m, x)) -> high(n, x),
                   ifquick(true(), x) -> nil(),
                  ifquick(false(), x) -> append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))),
                       isempty(nil()) -> true(),
                  isempty(cons(n, x)) -> false(),
                         quicksort(x) -> ifquick(isempty(x), x),
                          head(nil()) -> error(),
                     head(cons(n, x)) -> n,
                          tail(nil()) -> nil(),
                     tail(cons(n, x)) -> x,
                                  a() -> b(),
                                  a() -> c()}
     SPSC:
      Simple Projection:
       pi(if_high#) = 2, pi(high#) = 1
      Strict:
       {           high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)),
        if_high#(true(), n, cons(m, x)) -> high#(n, x)}
      EDG:
       {(high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)), if_high#(true(), n, cons(m, x)) -> high#(n, x))
        (if_high#(true(), n, cons(m, x)) -> high#(n, x), high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)))}
       SCCS:
        Scc:
         {           high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)),
          if_high#(true(), n, cons(m, x)) -> high#(n, x)}
        SCC:
         Strict:
          {           high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x)),
           if_high#(true(), n, cons(m, x)) -> high#(n, x)}
         Weak:
         {               if(true(), x, y) -> averIter(y, x, y),
                        if(false(), x, y) -> averIter(x, y, x),
                               ge(x, 0()) -> true(),
                           ge(s(x), s(y)) -> ge(x, y),
                            ge(0(), s(y)) -> false(),
                            average(x, y) -> if(ge(x, y), x, y),
                        averIter(x, y, z) -> ifIter(ge(x, y), x, y, z),
                  ifIter(true(), x, y, z) -> z,
                 ifIter(false(), x, y, z) -> averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))),
                            plus(s(x), y) -> s(plus(x, y)),
                             plus(0(), y) -> y,
                         append(nil(), y) -> y,
                    append(cons(n, x), y) -> cons(n, app(x, y)),
                            low(n, nil()) -> nil(),
                       low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)),
            if_low(true(), n, cons(m, x)) -> low(n, x),
           if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)),
                           high(n, nil()) -> nil(),
                      high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)),
           if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)),
          if_high(false(), n, cons(m, x)) -> high(n, x),
                       ifquick(true(), x) -> nil(),
                      ifquick(false(), x) -> append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))),
                           isempty(nil()) -> true(),
                      isempty(cons(n, x)) -> false(),
                             quicksort(x) -> ifquick(isempty(x), x),
                              head(nil()) -> error(),
                         head(cons(n, x)) -> n,
                              tail(nil()) -> nil(),
                         tail(cons(n, x)) -> x,
                                      a() -> b(),
                                      a() -> c()}
         SPSC:
          Simple Projection:
           pi(if_high#) = 2, pi(high#) = 1
          Strict:
           {high#(n, cons(m, x)) -> if_high#(ge(m, n), n, cons(m, x))}
          EDG:
           {}
           SCCS:
            
            Qed
    SCC:
     Strict:
      {            low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x)),
        if_low#(true(), n, cons(m, x)) -> low#(n, x),
       if_low#(false(), n, cons(m, x)) -> low#(n, x)}
     Weak:
     {               if(true(), x, y) -> averIter(y, x, y),
                    if(false(), x, y) -> averIter(x, y, x),
                           ge(x, 0()) -> true(),
                       ge(s(x), s(y)) -> ge(x, y),
                        ge(0(), s(y)) -> false(),
                        average(x, y) -> if(ge(x, y), x, y),
                    averIter(x, y, z) -> ifIter(ge(x, y), x, y, z),
              ifIter(true(), x, y, z) -> z,
             ifIter(false(), x, y, z) -> averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))),
                        plus(s(x), y) -> s(plus(x, y)),
                         plus(0(), y) -> y,
                     append(nil(), y) -> y,
                append(cons(n, x), y) -> cons(n, app(x, y)),
                        low(n, nil()) -> nil(),
                   low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)),
        if_low(true(), n, cons(m, x)) -> low(n, x),
       if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)),
                       high(n, nil()) -> nil(),
                  high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)),
       if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)),
      if_high(false(), n, cons(m, x)) -> high(n, x),
                   ifquick(true(), x) -> nil(),
                  ifquick(false(), x) -> append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))),
                       isempty(nil()) -> true(),
                  isempty(cons(n, x)) -> false(),
                         quicksort(x) -> ifquick(isempty(x), x),
                          head(nil()) -> error(),
                     head(cons(n, x)) -> n,
                          tail(nil()) -> nil(),
                     tail(cons(n, x)) -> x,
                                  a() -> b(),
                                  a() -> c()}
     SPSC:
      Simple Projection:
       pi(if_low#) = 2, pi(low#) = 1
      Strict:
       {            low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x)),
        if_low#(false(), n, cons(m, x)) -> low#(n, x)}
      EDG:
       {(low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x)), if_low#(false(), n, cons(m, x)) -> low#(n, x))
        (if_low#(false(), n, cons(m, x)) -> low#(n, x), low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x)))}
       SCCS:
        Scc:
         {            low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x)),
          if_low#(false(), n, cons(m, x)) -> low#(n, x)}
        SCC:
         Strict:
          {            low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x)),
           if_low#(false(), n, cons(m, x)) -> low#(n, x)}
         Weak:
         {               if(true(), x, y) -> averIter(y, x, y),
                        if(false(), x, y) -> averIter(x, y, x),
                               ge(x, 0()) -> true(),
                           ge(s(x), s(y)) -> ge(x, y),
                            ge(0(), s(y)) -> false(),
                            average(x, y) -> if(ge(x, y), x, y),
                        averIter(x, y, z) -> ifIter(ge(x, y), x, y, z),
                  ifIter(true(), x, y, z) -> z,
                 ifIter(false(), x, y, z) -> averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))),
                            plus(s(x), y) -> s(plus(x, y)),
                             plus(0(), y) -> y,
                         append(nil(), y) -> y,
                    append(cons(n, x), y) -> cons(n, app(x, y)),
                            low(n, nil()) -> nil(),
                       low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)),
            if_low(true(), n, cons(m, x)) -> low(n, x),
           if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)),
                           high(n, nil()) -> nil(),
                      high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)),
           if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)),
          if_high(false(), n, cons(m, x)) -> high(n, x),
                       ifquick(true(), x) -> nil(),
                      ifquick(false(), x) -> append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))),
                           isempty(nil()) -> true(),
                      isempty(cons(n, x)) -> false(),
                             quicksort(x) -> ifquick(isempty(x), x),
                              head(nil()) -> error(),
                         head(cons(n, x)) -> n,
                              tail(nil()) -> nil(),
                         tail(cons(n, x)) -> x,
                                      a() -> b(),
                                      a() -> c()}
         SPSC:
          Simple Projection:
           pi(if_low#) = 2, pi(low#) = 1
          Strict:
           {low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x))}
          EDG:
           {}
           SCCS:
            
            Qed
    SCC:
     Strict:
      {plus#(s(x), y) -> plus#(x, y)}
     Weak:
     {               if(true(), x, y) -> averIter(y, x, y),
                    if(false(), x, y) -> averIter(x, y, x),
                           ge(x, 0()) -> true(),
                       ge(s(x), s(y)) -> ge(x, y),
                        ge(0(), s(y)) -> false(),
                        average(x, y) -> if(ge(x, y), x, y),
                    averIter(x, y, z) -> ifIter(ge(x, y), x, y, z),
              ifIter(true(), x, y, z) -> z,
             ifIter(false(), x, y, z) -> averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))),
                        plus(s(x), y) -> s(plus(x, y)),
                         plus(0(), y) -> y,
                     append(nil(), y) -> y,
                append(cons(n, x), y) -> cons(n, app(x, y)),
                        low(n, nil()) -> nil(),
                   low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)),
        if_low(true(), n, cons(m, x)) -> low(n, x),
       if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)),
                       high(n, nil()) -> nil(),
                  high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)),
       if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)),
      if_high(false(), n, cons(m, x)) -> high(n, x),
                   ifquick(true(), x) -> nil(),
                  ifquick(false(), x) -> append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))),
                       isempty(nil()) -> true(),
                  isempty(cons(n, x)) -> false(),
                         quicksort(x) -> ifquick(isempty(x), x),
                          head(nil()) -> error(),
                     head(cons(n, x)) -> n,
                          tail(nil()) -> nil(),
                     tail(cons(n, x)) -> x,
                                  a() -> b(),
                                  a() -> c()}
     SPSC:
      Simple Projection:
       pi(plus#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {       averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z),
       ifIter#(false(), x, y, z) -> averIter#(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0())))}
     Weak:
     {               if(true(), x, y) -> averIter(y, x, y),
                    if(false(), x, y) -> averIter(x, y, x),
                           ge(x, 0()) -> true(),
                       ge(s(x), s(y)) -> ge(x, y),
                        ge(0(), s(y)) -> false(),
                        average(x, y) -> if(ge(x, y), x, y),
                    averIter(x, y, z) -> ifIter(ge(x, y), x, y, z),
              ifIter(true(), x, y, z) -> z,
             ifIter(false(), x, y, z) -> averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))),
                        plus(s(x), y) -> s(plus(x, y)),
                         plus(0(), y) -> y,
                     append(nil(), y) -> y,
                append(cons(n, x), y) -> cons(n, app(x, y)),
                        low(n, nil()) -> nil(),
                   low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)),
        if_low(true(), n, cons(m, x)) -> low(n, x),
       if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)),
                       high(n, nil()) -> nil(),
                  high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)),
       if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)),
      if_high(false(), n, cons(m, x)) -> high(n, x),
                   ifquick(true(), x) -> nil(),
                  ifquick(false(), x) -> append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))),
                       isempty(nil()) -> true(),
                  isempty(cons(n, x)) -> false(),
                         quicksort(x) -> ifquick(isempty(x), x),
                          head(nil()) -> error(),
                     head(cons(n, x)) -> n,
                          tail(nil()) -> nil(),
                     tail(cons(n, x)) -> x,
                                  a() -> b(),
                                  a() -> c()}
     Fail
    SCC:
     Strict:
      {ge#(s(x), s(y)) -> ge#(x, y)}
     Weak:
     {               if(true(), x, y) -> averIter(y, x, y),
                    if(false(), x, y) -> averIter(x, y, x),
                           ge(x, 0()) -> true(),
                       ge(s(x), s(y)) -> ge(x, y),
                        ge(0(), s(y)) -> false(),
                        average(x, y) -> if(ge(x, y), x, y),
                    averIter(x, y, z) -> ifIter(ge(x, y), x, y, z),
              ifIter(true(), x, y, z) -> z,
             ifIter(false(), x, y, z) -> averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))),
                        plus(s(x), y) -> s(plus(x, y)),
                         plus(0(), y) -> y,
                     append(nil(), y) -> y,
                append(cons(n, x), y) -> cons(n, app(x, y)),
                        low(n, nil()) -> nil(),
                   low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)),
        if_low(true(), n, cons(m, x)) -> low(n, x),
       if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)),
                       high(n, nil()) -> nil(),
                  high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)),
       if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)),
      if_high(false(), n, cons(m, x)) -> high(n, x),
                   ifquick(true(), x) -> nil(),
                  ifquick(false(), x) -> append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))),
                       isempty(nil()) -> true(),
                  isempty(cons(n, x)) -> false(),
                         quicksort(x) -> ifquick(isempty(x), x),
                          head(nil()) -> error(),
                     head(cons(n, x)) -> n,
                          tail(nil()) -> nil(),
                     tail(cons(n, x)) -> x,
                                  a() -> b(),
                                  a() -> c()}
     SPSC:
      Simple Projection:
       pi(ge#) = 0
      Strict:
       {}
      Qed