TRS: { eq(0(), 0()) -> true(), eq(0(), s(m)) -> false(), eq(s(n), 0()) -> false(), eq(s(n), s(m)) -> eq(n, m), le(0(), m) -> true(), le(s(n), 0()) -> false(), le(s(n), s(m)) -> le(n, m), min(cons(x, nil())) -> x, min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x))), if_min(true(), cons(n, cons(m, x))) -> min(cons(n, x)), if_min(false(), cons(n, cons(m, x))) -> min(cons(m, x)), replace(n, m, nil()) -> nil(), replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)), if_replace(true(), n, m, cons(k, x)) -> cons(m, x), if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)), empty(nil()) -> true(), empty(cons(n, x)) -> false(), head(cons(n, x)) -> n, tail(nil()) -> nil(), tail(cons(n, x)) -> x, sort(x) -> sortIter(x, nil()), sortIter(x, y) -> if(empty(x), x, y, append(y, cons(min(x), nil()))), if(true(), x, y, z) -> y, if(false(), x, y, z) -> sortIter(replace(min(x), head(x), tail(x)), z)} Fail