MAYBE
Time: 0.009135
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:
  DP:
   {               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}
  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()}
  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))
    (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_high#(true(), n, cons(m, x)) -> average#(m, m), average#(x, y) -> ge#(x, y))
    (if_high#(true(), n, cons(m, x)) -> average#(m, m), average#(x, y) -> if#(ge(x, y), x, y))
    (high#(n, cons(m, x)) -> ge#(m, n), ge#(s x, s y) -> ge#(x, y))
    (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))
    (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
    (if_low#(true(), 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), low#(n, cons(m, x)) -> ge#(m, n))
    (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)) -> 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#(true(), n, cons(m, x)) -> average#(m, m))
    (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#(false(), n, cons(m, x)) -> low#(n, x), low#(n, cons(m, x)) -> ge#(m, n))
    (if_low#(false(), n, cons(m, x)) -> low#(n, x), low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, 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))
    (low#(n, cons(m, x)) -> if_low#(ge(m, n), n, cons(m, x)), if_low#(false(), n, cons(m, x)) -> low#(n, x))
    (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))
    (average#(x, y) -> ge#(x, y), ge#(s x, s y) -> 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())))
    (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) -> plus#(y, s 0()))
    (averIter#(x, y, z) -> ifIter#(ge(x, y), x, y, z), ifIter#(false(), x, y, z) -> plus#(z, s 0()))
    (low#(n, cons(m, x)) -> ge#(m, n), ge#(s x, s y) -> ge#(x, y))
    (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))))
    (quicksort# x -> ifquick#(isempty x, x), ifquick#(false(), x) -> 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) -> quicksort# low(head x, tail 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) -> head# x)
    (quicksort# x -> ifquick#(isempty x, x), ifquick#(false(), x) -> tail# x)
    (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))}
   STATUS:
    arrows: 0.943333
    SCCS (6):
     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:
      {       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:
      {            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:
      {ge#(s x, s y) -> ge#(x, y)}
     Scc:
      {plus#(s x, y) -> plus#(x, y)}
     
     SCC (3):
      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()}
      Open
     
     
     
     
     
     SCC (3):
      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()}
      Open
     
     
     
     
     
     SCC (2):
      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()}
      Open
     
     
     
     SCC (3):
      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()}
      Open
     
     SCC (1):
      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()}
      Open
     
     
     
     SCC (1):
      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()}
      Open