Progress towards handling Atomic in the symbolic evaluator.

It turns out that this requires a "simple" lemma first:

  - if there is a graph for a statement, then this statement can
    indeed evolve as the graph says it can (all the way to Done)

The previous correctness statement says something slightly weaker,
namely

  - if there is a graph for a statement *and* that statement evolves
    to Done, then the statement must reach the same point as the graph
    predicts.