Why use the operations var to express the a read have must have a write consistency?

[inevity]

Is it possible to use the temporal formula(using existing and universal symboler and action predicate and /\ and /) to express the consistency?
Look like the vars you specify is too many, specially about the observability vars?

[inevity]

It is helper var.