> -- Comdiv писал(а):
> Этот элементарный пример ставит в ступор систему доказательства. Я знаю, как это доказать вручную, но утилите это не поможет. Попробовав разобраться с этим через документацию, я не получил результата. Подумал, что в Ada/SPARK должно быть проще, но там получил то же самое. Нашёл информацию, что есть специальная библиотека, позволяющая доказывать такие вещи, но в свободной поставке я её не нашёл.Кстати, этот код доказал другой разработчик, правда, грязно - введением дополнительной аксиоматики. Не уверен, что исходных аксиом не хватало.