Complete reworking of PseudoC semantics to use one global memory.

This requires a bit of work to get isolation of local par-loop
variables (use a substitution primitive), and completely precludes
other sorts of local state.  Could probably get it back by renaming
parallelized variables apart, so I'm not seriously disturbed.

(Should maybe drop substitution, and do the rename apart for the loop
variables too.  For discussion.)
Start reworking of PseudoC properties theory.

Proof of termination for eval is mostly unchanged.
Still need to fix the nature of actions, and the graphOf function.