- (forall '': /)
- [A] A or ( = )
- <A> A and (
notequal )
- Unchanged =
- eventually not always not
- always ( eventually )
- WF(A) (always eventually <A
>) or (always eventually not Enabled <A>)
- SF(A) (always eventually <A
>) or (eventually always not Enabled <A>)