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

Re: [tlaplus] TLAPS project status

You're right, of course. I had written down the proof for the initial condition a=0, then changed that condition without thinking properly. And since the proof is OMITTED, the prover couldn't check it for me. We really need to support these steps!

Thanks,
Stephan


On 12 Oct 2015, at 04:40, ka...@xxxxxxxxxxxxxxx wrote:

Nitpicking: <1>1 is not valid. Init could already set a > n.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.