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

*From*: belout...@xxxxxxxxx*Date*: Sun, 30 Apr 2017 08:42:51 -0700 (PDT)

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

**Follow-Ups**:**Re: [tlaplus] About a Theorem in the Raw TLA***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] theorems from instantiated modules in `tlapm` version 2** - Next by Date:
**Re: [tlaplus] About a Theorem in the Raw TLA** - Previous by thread:
**Re: [tlaplus] theorems from instantiated modules in `tlapm` version 2** - Next by thread:
**Re: [tlaplus] About a Theorem in the Raw TLA** - Index(es):