Started code/variants1Dloop.sml.  Does not typecheck.
More futzing with variants1Dloop.sml.
Make the orgcode evaluation work.
Sketched out bare bones C version

of transformed code in variants1Dloop.sml for cpack reordering of
iterations.
codevariant1 partially works, just need to implement the construct_explicit_relation and inspector functions now
construct_explicit_relation working for codevariant1
Leftoff thinking about how to do inspector.
Still working on the inspector.  Stuck in that don't know how to model visited flags in ML.
Inspector for code variant1 appears to be working, but more testing is needed.
Some progress towards "permutations suffice" result in HOL.
Add another HOL byproduct to .gitignore
Complete "Δ is a permutation" is sufficient for simplest reindexing proof

In other words, if the loop is of the form

  for(i = 0; i < N; i++)
    A[i] = ...stuff not involving A...

and Δ is a permutation over 0..N-1, then the above is equivalent to

  for(i = 0; i < N; i++)
    A[Δ[i]] = ...stuff not involving A with any
                 occurrences of i replaced by Δ[i]...
Merge branch 'master' of https://github.com/mn200/inspector-strategies
Added domain and range specification to mrel.

Can't assume that we will always have representative pairs for
everything in the range.  Really only need everything at the upper end
of the range, but this is still an issue.  Still not getting results I
expect with construct_explicit_relation when the computation domain is
smaller than the data index space.
Got variant 1 working in variants1Dloop.sml.
Shorted rsize routine names.  Implemented RFOR in primitives.sml.
RFOR is now being used in the cpack inspector.
Cleanup code is now in the cpack inspector.
Move "simple loop" stuff into separate theory; prove stronger map result.

A map loop is one that is allowed to look at the old value of the
array at the index being updated. This subsumes the older result
because one could use the new lemma with an f instantiated so as to
ignore the old value.
Prove a Hoare-like rule for FOR, and use it in a few proofs.

It causes much pain when attempting results of the form

  FOR (lo,hi) ... = FOR (lo,hi) ...

though. Easier in this circumstance to just induct on `hi - lo`.