[Axiom-developer] Proving Axiom Correct

[daly]

The latest update contains the first proof of Axiom's Common Lisp
code using ACL2. ACL2 is a common lisp that has proof technology
and since Axiom is all common lisp (no boot code), this is a good
basis for proofs.

This update proves that the predicate isWrapped takes anything as
an argument and returns either t or nil. One caveat is that ACL2
does not handle floating point so (floatp x) is omitted but this
is fine for now. The signature line is 

   isWrapped: t -> (or t nil)

The plan of attack is to prove functions which use only common lisp
primitives in their implementation first and then work upward through
functions that use only the proven set. The base level functions are
already marked in the interpreter.

In the longer term ACL2 will be integrated into the build process so
each release has an ever-growing proven subset.

This is the first step in a very large task.

Tim