TRS:
 {                      sort(nil()) -> nil(),
                   sort(cons(x, y)) -> insert(x, sort(y)),
                   insert(x, nil()) -> cons(x, nil()),
              insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v),
      choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)),
   choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w)),
  choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
 Fail