About a Theorem in the Raw TLA

[belout...@xxxxxxxxx]

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