Implement equality comparison for PseudoCOps.  Also adjust overloads.

Overloads are now over expressions so that it's possible to write

    IfStmt (e1 + e2 == e3) thencase elsecase

Previously, the overloading made the syntax nice for operations on
values, which seems less useful.
State simple old-code/executor equivalence result for parallel wavefronts

Simple because it iterates over all possible iterations within each
wave and just executes those that are enabled for the current wave.
(Simplification suggested at ColoState when I was visiting.)
Define strip_purereads fn, use it in forparConvert theorem statement.

The strip_purereads function walks over a hierarchical action graph
and throws away all atomic nodes that are only reads. Somewhat to my
surprise, doing so preserves meaning. Adding pure-read nodes can add
dependence links, but if it does they're unnecessary. For example:

       w := 3      v := u + 10
	 ^	    ^
	  \	   /
	   \	  /
          read v, w
             ^
             |
             |
           v := u + 3

All the read node in the middle is doing here is unnecessarily linking
the first v assignment to the w assignment. In its absence, those two
wouldn't be linked, perfectly reasonably, and the two v assignments
would still be linked.

If the bottom assignment read from w, then there would be a WAR
dependence between it and the w-assignment, and again, the middle
pure-read node isn't winning us anything.

This makes me tempted to go back to a world where action nodes must
include exactly one write and some number of reads, because allowing
for no writes and some reads doesn't seem to win us anything.