Re: [tlaplus] About a Theorem in the Raw TLA

[Stephan Merz <stepha...@xxxxxxxxx>]

The implication

  A => ENABLED A

is indeed valid for any action A. Semantically, the proof is obvious from the definition of ENABLED and ordinary predicate logic. If you refer to proofs in the TLA+ Proof System, ENABLED is not yet supported [1]. We are currently reimplementing TLAPS, and one of our main motivations for doing so is to provide the basis for supporting reasoning about ENABLED.

Regards,

Stephan

[1] https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Unsupported_features.html

On 30 Apr 2017, at 17:42, belout...@xxxxxxxxx wrote:

Hi all,

In the Raw TLA can we state the following Theorem :

Theorem : For any action A, A ==> Enabled(A)

If it is valid , How we can prove it ?. If it is invalid , let me know the counterexample.

Once again, if the suggested statement is a theorem, can we add the following inference rule : For any A in Raw TLA.

                           A
                    --------------
                     A ==> Enabled(A)  

Thanks In advance

--
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 https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.