Докажите, что эта блок-схема (картинка) завершается на этом предусловии при помощи метода фундированных множеств. Решение присылайте на почту до 12:00 5 марта в виде двух файлов: файла *.py с индуктивными утверждениями и оценочными функциями в формате PyFloyd и файла *.prf с PVS доказательством истинности условий верификации.
Обратите внимание, что инструмент PyFloyd поддерживает (пока) единственное фундированное множество: неотрицательные целые числа и арифметическое сравнение «меньше», а множеством значений всех оценочных функций является множество всех целых чисел.