About a Theorem in the Raw TLA

[belout...@gmail.com]

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

[Stephan Merz]

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

--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.