diff --git a/books/ProvingAxiomCorrect.pamphlet b/books/ProvingAxiomCorrect.pamphlet
index 55192fb..6ef366f 100644
--- a/books/ProvingAxiomCorrect.pamphlet
+++ b/books/ProvingAxiomCorrect.pamphlet
@@ -1,10 +1,74 @@
\documentclass[dvipdfm]{book}
-\newcommand{\VolumeName}{Volume 14: Proving Axiom Correct}
+\newcommand{\VolumeName}{Volume 13: Proving Axiom Correct}
\input{bookheader.tex}
\mainmatter
\setcounter{chapter}{0} % Chapter 1
-\chapter{Goals and Background}
+\chapter{Here is a problem}
+The goal is to prove that Axiom's implementation of
+the Euclidean GCD algorithm is correct.
+From category EuclideanDomain (EUCDOM) we find the implementation of
+the Euclidean GCD algorithm:
+\begin{verbatim}
+ gcd(x,y) == --Euclidean Algorithm
+ x:=unitCanonical x
+ y:=unitCanonical y
+ while not zero? y repeat
+ (x,y):= (y,x rem y)
+ y:=unitCanonical y -- this doesn't affect the
+ -- correctness of Euclid's algorithm,
+ -- but
+ -- a) may improve performance
+ -- b) ensures gcd(x,y)=gcd(y,x)
+ -- if canonicalUnitNormal
+ x
+\end{verbatim}
+The unitCanonical function comes from the category IntegralDomain (INTDOM)
+where we find:
+\begin{verbatim}
+ unitNormal: % -> Record(unit:%,canonical:%,associate:%)
+ ++ unitNormal(x) tries to choose a canonical element
+ ++ from the associate class of x.
+ ++ The attribute canonicalUnitNormal, if asserted, means that
+ ++ the "canonical" element is the same across all associates of x
+ ++ if \spad{unitNormal(x) = [u,c,a]} then
+ ++ \spad{u*c = x}, \spad{a*u = 1}.
+ unitCanonical: % -> %
+ ++ \spad{unitCanonical(x)} returns \spad{unitNormal(x).canonical}.
+\end{verbatim}
+implemented as
+\begin{verbatim}
+ UCA ==> Record(unit:%,canonical:%,associate:%)
+ if not (% has Field) then
+ unitNormal(x) == [1$%,x,1$%]$UCA -- the non-canonical definition
+ unitCanonical(x) == unitNormal(x).canonical -- always true
+ recip(x) == if zero? x then "failed" else _exquo(1$%,x)
+ unit?(x) == (recip x case "failed" => false; true)
+ if % has canonicalUnitNormal then
+ associates?(x,y) ==
+ (unitNormal x).canonical = (unitNormal y).canonical
+ else
+ associates?(x,y) ==
+ zero? x => zero? y
+ zero? y => false
+ x exquo y case "failed" => false
+ y exquo x case "failed" => false
+ true
+\end{verbatim}
+
+\section{Approaches}
+There are several systems that could be applied to approach the proof.
+
+I plan to initially look at Coq and ACL2. I suspect, from my initial
+understanding of both systems, that both systems are needed. Coq
+seems to be applicable at the Spad level. ACL2 seems to be applicable
+at the Lisp level. Both levels are necessary for a proper proof.
+
+\chapter{It is an interesting problem}
+\chapter{It is an unsolved problem}
+\chapter{Here is my idea}
+\chapter{My idea works}
+\chapter{Here is how my idea compares to others}
\begin{thebibliography}{99}
\bibitem[Bertot 04]{Bert04} Bertot, Yves; Cast\'eran, Pierre\\
``Interactive Theorem Proving and Program Development''\\
diff --git a/changelog b/changelog
index 14365a5..cd4c232 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20140613 tpd src/axiom-website/patches.html 20140613.02.tpd.patch
+20140613 tpd books/ProvingAxiomCorrect state the problem
20140613 tpd src/axiom-website/patches.html 20140613.01.tpd.patch
20140613 tpd books/ProvingAxiomCorrect created
20140612 tpd src/axiom-website/patches.html 20140612.01.tpd.patch
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index a7c2ab1..ec59716 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -4422,6 +4422,8 @@ books/bookvolbib add Le96a
books/bookvolbib add Proving Axiom Correct section, Bert04
20140613.01.tpd.patch
books/ProvingAxiomCorrect created
+20140613.02.tpd.patch
+books/ProvingAxiomCorrect state the problem