from the domain of discourse. Construct a modified infostate s' by
adjusting the assignment function of each possibility so as to map the variable x to a.
Then update s' with φ. Finally, take the union over the results of
-doing this for every object a in the domain of discourse.
+doing this for every object a in the domain of discourse. If you're
+unsure about this, examine the [[code|code/gsv.ml]].
Negation is natural enough: