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
 <a href="patches/20140613.01.tpd.patch">20140613.01.tpd.patch</a>
 books/ProvingAxiomCorrect created
+<a href="patches/20140613.02.tpd.patch">20140613.02.tpd.patch</a>
+books/ProvingAxiomCorrect state the problem
  </body>
 </html>