Formally add Volume 13: Proving Axiom Correct

This is a new volume where we will create a proof of a Spad algorithm
using Coq, ACL2, and an LLVM to ACL2 translator.
Fixup broken build issues

The prior dvipdfm fix used a bad file which ended up removing all
of the includegraphics. fixed.

Volume 4 and 10.3 contained a new quote by Manuel that caused a
syntax error. Fixed.

Volume 13 had a badly formed bibliography. Fixed.