and forall inAddress:
(main()
in MemVal) and (cache() = bottom)
or (exists in Address: A()
or A())
( = ) (() = )
and ( notequal ) (() = ())
and op' = "read" and adr' in Address
and Unchanged <main, cache>
andop' = "write" and adr' in Address
and val' in MemVal
and Unchanged <main, cache>