1. На языке WhyML напишите функцию, которая находит минимальный делитель данного целого неотрицательного числа. Напишите формальную спецификацию и докажите полную корректность при помощи WhyML и солверов.

  2. Решите предыдущую задачу, заменив циклы на рекурсию.

  3. Оформите решение задач из прошлой темы как лемма-функции и докажите полную корректность лемма-функций относительно их спецификаций.