Cómo argumentar la corrección del tipo radix

Podrías hacer una prueba por inducción.

Supongamos que la raíz es base [matemática] b [/ matemática]. La hipótesis de inducción podría ser que después de ordenar los dígitos [matemáticos] d [/ matemáticos], se ordena la lista de números módulo [matemático] b ^ d [/ matemático].

Si puede probar esto, habrá terminado porque una vez que [math] d [/ math] es lo suficientemente alto, significa que toda la lista está ordenada.

Para demostrarlo, debe establecer (a) el caso base: demuestre que es cierto para [math] d = 1 [/ math], y (b) el paso de inducción: demuestre que si es cierto hasta cierto valor de [math] d [/ math], entonces también debe ser cierto para [math] d + 1 [/ math].

Para hacer esto, tenga en cuenta que dos números están en diferentes cubos, en cuyo caso están en el orden correcto, o están en el mismo cubo, pero luego estarán en el mismo orden que después de la iteración anterior, que por el La hipótesis de inducción era el orden correcto.

¡Buena suerte!

Use un asistente de prueba como coq.