Aproc <=> op = "ready" and op' = "read" and adr' in Addressand memory' = memory Aproc <=> op = "ready" and op' = "write" and adr' in Addressand val' in MemVal and memory' = memory Amem <=> op = "read" and op' = "ready" and val' = memory(adr) and memory' = memory Amem <=> op = "write" and op' = "ready" and A(adr, val)