Progress with for/par result.

Move some things around to keep them tidy.

Also now believe I have a good characterisation of the correctness
condition required of the wave array.

Substitutions and variable names are a slight issue: the statement of
correctness now includes assumptions stating that new variable names
have to be suitably fresh.