[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Missing theorem

However, I am a little reluctant to add the lemma that you propose, since it is just proved by OBVIOUS. If you have an instance of this lemma in the context of a larger proof where the prover was unable to prove such a step, I'd be interested in hearing about it.
Hi Stephan,
Which SMT do you use?