So I'm getting to know the event-b specification language and the Rodin tool.
While doing that, I came across some weird behavior of the Rodin tool, and I'd love to get some help here.
I'm on the proving perspective, and I have two hypotheses:
- 1 <= v
- v <= n
my goal is:
- 1 <= n
I'd expect that the default auto prover will manage to handle it, but it is not.
My question is, should I configure something explicitly? Or maybe for some reason, this is not supposed to be discharged automatically?
The thing is that I can't even discharge it manually, since it's basic math.
Thats how it looks in the Rodin tool
Thank you!
There is a plug-in to use SMT solvers in proofs from within Rodin. There is also a plug-in to use Atelier B provers. You may want to try one of those.