Start of a file reproving earlier result over array ops that might fail.

If everything gets partial because indexing and updating outside of
array bounds are illegal, the results should be much the same, but
perhaps harder to prove.

Most of this is a commented out copy of simpleLoopScript.sml.
(Commented out because the old proofs don't quite work.)
Data-dependent loop primitive defined.

Also
- some trivial lemmas about ddepR; and
- statement of correctness for the desired loop transformation
  captured.

Still assuming that the δ mapping will preserve domains:

  [0,N) <-> [0,N)

in fact.