Доказательство инструмента Родена - транзитивность

Question

Итак, я знакомлюсь с языком спецификации event-b и инструментом Rodin.

При этом я столкнулся с каким-то странным поведением инструмента Rodin, и я хотел бы получить здесь помощь.

Я занимаюсь доказыванием, и у меня есть две гипотезы:

• 1 <= v
• v <= п

моя цель:

• 1 <= п

Я ожидаю, что автодоказательство по умолчанию справится с этим, но это не так.

Мой вопрос: должен ли я что-то явно настраивать? А может быть по какой-то причине это не должно сбрасываться автоматически?

Дело в том, что я даже не могу его вручную разрядить, так как это элементарная математика.

Вот как это выглядит в инструменте Rodin

Спасибо!

Answer 1

Существует плагин для использования решателей SMT в доказательствах из Rodin. Существует также плагин для использования пруверов Atelier B. Возможно, вы захотите попробовать один из них.