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

*From*: fl <freder...@xxxxxxxxxxx>*Date*: Fri, 7 Nov 2014 07:30:44 -0800 (PST)*References*: <35991e2d-322c-456c-adb2-2cf4653a6e90@googlegroups.com> <95EF01AC-6354-4CD5-BA1E-35DC4B78A274@gmail.com>

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?

--

FL

**References**:**Missing theorem***From:*fl

**Re: [tlaplus] Missing theorem***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Missing theorem** - Next by Date:
**Re: [tlaplus] Missing theorem** - Previous by thread:
**Re: [tlaplus] Missing theorem** - Next by thread:
**Re: [tlaplus] Missing theorem** - Index(es):