Editorial: Rework memory model relations

[syg]

This PR reworks the relations that define the memory model to read closer to existing memory model literature.

• Relations (e.g. happens-before) are no longer kept in slots in candidate executions, and instead look like "a happens-before b in execution". Currently relations are defined as basically Lists of pairs, and keeping them in internal slots like [[HappensBefore]] gives the misconception that these relations are algorithmically maintained. In reality the Relations are "manifested" as needed over the sets of events. What's kept in slots are the things that are in fact algorithmically maintained, like [[EventsList]].
• Rename relation names to start with a verb so the inline "a R b" form reads naturally.
• Remove aoids from the relations, since they aren't AOs.
• Relation names are dfn'd.
• Beef up some misc prose.

Closes #3320.