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

Re: [tlaplus] Missing theorem

Hello Frédéric,

thanks for the suggestion – we always value hints about which lemmas are missing in the standard library. In fact, the next release will see many additions to the SequenceProperties module.

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.


On 07 Nov 2014, at 15:50, fl <freder...@xxxxxxxxxxx> wrote:

A theorem that is missing in SequenceProperties. tla (in my opinion).
ASSUME NEW S, NEW J \in Nat, NEW seq \in [ 1 .. J -> S ]
PROVE seq \in Seq(S)

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.