Название слишком общее. Специфическая c проблема, с которой я сталкиваюсь, связана с рассуждением интегральных операций по модулю (%).
Предположим, я хочу доказать некоторые свойства члена a % b. Я считаю, что это будет легко, если я могу написать a как форму x * b + y для некоторых x и y, когда оба a и b положительны. Чтобы показать обоснованность допущения x * b + y к a, нам нужно доказать, что существуют целые числа x и y, удовлетворяющие некоторым ограничениям и x * b + y = a.
Итак, мой вопрос в том, что Можно ли добавить в ACL2 некоторые теоремы, которые показывают справедливость такой замены, и эти теоремы можно использовать для переписывания a на x * b + y?
Спасибо за внимание.