ENABLED Operator Theorems

[kacem belout <belout...@xxxxxxxxx>]

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)

In the context of the Raw Logic (RTLA), for any Action A, we assert the following valid statements. Let me know if any one is not valid by giving a counterexample, thanks !.

Theorem 1 : A ==> ENABLED(A)

                 Proof : Now, I don't know How To formally and mechanically derive ENABLED(A) From A which is expressed in terms of primed variables and unprimed variables.

Theorem 2 : \Not ENABLED(A) ==> \Not A

                 Proof : Is equivalent to Theorm1 by propositional logic rule (implication equivalente to its contrapositive).

Theorem 3 : \Not A ==> \Not ENABLED(A)

Theorem 4 : \Not (ENABLED(A)) ==> ENABLED( \Not (A))

Theorem 5 :  ENABLED(A) <==> ENABLED(-1(A)) , where -1(A) == (A)-1 ; inverse of A.  (A)-1 == A ( v ' <- v , v <- v ')

Theorem 6 : For any state predicate P.  P <==> ENABLED(P)

Theorem 7 : For any state predicate P.  P ==> ENABLED((P) '), where ' == Prime operator.

Theorem 8 : For any state predicate P.  P ==> ENABLED(((p)')-1)

Another Thanks for your Help and Critics.