Reconcile store_thms with diverging names in db and val binding

Remove TABs from examples

Remove trailing whitespace in examples directory.

Some cleanups in the ACL2 example.

Attempt (and fail) to get fmap_encodeScript to build again.

Types based upon finite maps encode correctly and simple functions from the opsem script translate.
Some of the script has been translated in fmapExample.sml, however, translations now require conditional translation on successful evalation.

Added FMAP_MAP_COMPOSE. This completes the required type theorems. However, the encoder will need adjusting to deal with the extra ONE_ONE predicates

Added ENCMAPENC theorem and cured some polyml problems.

Fixed some theorems not working under PolyML.

Updated fmap_encode to use QSORT3 from sortingTheory.

Added rewrite for update and cleaned up sorting proofs

Added rewrites for element in map and lookup

Version of SEXP_LT that can be translated easily to ACL2. Unfortunately causes very slow proof times...

Completed encoding / decoding theorems

Encoding of decoding theorem complete

Completed encode-decode theorem

Added (unfinished) finite map encoding script.