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

*From*: kacem belout <belout...@xxxxxxxxx>*Date*: Wed, 3 May 2017 10:46:00 +0200

Hallo,

I noticed the following theorems concerning the ENABLED Operator that I hopefully would like to prove them in a formal way ( i.e Formally ( Logically and/or symbolically) as using Inference Rules)Theorem 7 : For any state predicate P. P ==> ENABLED((P) '), where ' == Prime operator.

Another Thanks for your Help and Critics.

**Follow-Ups**:**Re: [tlaplus] ENABLED Operator Theorems***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Leibniz and ToBoolean Operators and Proof Fragment** - Next by Date:
**Re: [tlaplus] ENABLED Operator Theorems** - Previous by thread:
**Re: [tlaplus] Leibniz and ToBoolean Operators and Proof Fragment** - Next by thread:
**Re: [tlaplus] ENABLED Operator Theorems** - Index(es):