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

About a Theorem in the Raw TLA

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 ==> Enabled(A)  

Thanks In advance