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.

[bakkot]

This is great.

[jmdyck]

The scope of the negation is ambiguous.

it is not the case that A and B

could mean

(it is not the case that A) and B

or

it is not the case that (A and B)

(Though I'm guessing it's fairly clear to anyone interested in this section that the latter is intended.)

[syg]

I'll add a "both".

[michaelficarra]

I wouldn't be against adding an "Unless" form for cases like this.

[michaelficarra]

LGTM otherwise, though I'd like @bakkot to re-review since the changes were non-trivial.

changes addressed