Complete revisions to Pseudo C "properties" theory.

The important lemma about writes ("actions") and expression evaluation
commuting has to pick up a new condition: the expression evaluation
can't involve any reads of whole arrays. As it happens, this is
guaranteed by the condition that the evaluation of the expression not
result in an error or an array value.