From bd7a45516d5d6337d7fcda4796dacef06d6c14a3 Mon Sep 17 00:00:00 2001
From: Joe Corneli <holtzermann17@gmail.com>
Date: Wed, 12 Jul 2017 00:28:47 +0100
Subject: [PATCH] rearrange slightly

---
 latex/arxana-merge.tex | 71 +++++++++++++++++++++++++++++---------------------
 1 file changed, 41 insertions(+), 30 deletions(-)

diff --git a/latex/arxana-merge.tex b/latex/arxana-merge.tex
index 24db1ed..a46bec0 100644
--- a/latex/arxana-merge.tex
+++ b/latex/arxana-merge.tex
@@ -2414,15 +2414,49 @@ Arxana.
 
 \subsection{``Modelling mathematics the way it is really done''} \label{farm-demo}
 
-\begin{notate}{A demonstration}
+\begin{notate}{Demonstrations}
 In a paper for the 5th ACM SIGPLAN International Workshop on
 Functional Art, Music, Modelling and Design (FARM 2017), we talk about
 how Arxana can be applied to model mathematical proofs.  A rather
 advanced form of ``mathematical knowledge management'' is proposed,
 that integrates dialogue, heuristics, and that ultimately moves in the
 direction of an AI system.  In this section, we should walk through
-this application.  Here are a couple of examples of the sorts of representations we will want to
-deal with.
+this application.
+\end{notate}
+
+\begin{notate}{A simple analogy}
+The first example is, on the face of it, a very simple analogy.
+The answer to the question posed is, however, more complicated.
+\end{notate}
+
+\begin{idea}
+(Assert (implies (and "G finite group"
+                      "H subgroup of G"
+                      "[G : H] finite")
+                 "G not equal to union of
+                  ghg^-1"))
+
+(Assert (analogy
+         (implies (and "G finite group"
+                       "H subgroup of G"
+                       "[G : H] finite")
+                  "G not equal to union of
+                   ghg^-1")
+         (implies (and "G infinite group"
+                       "H subgroup of G"
+                       "[G : H] finite")
+                  "G not equal to union of
+                   ghg^-1")))
+
+(Question (implies (and "G infinite group"
+                        "H subgroup of G"
+                        "[G : H] finite")
+                   "G not equal to union of
+                    ghg^-1"))
+\end{idea}
+
+\begin{notate}{A challenge problem}
+The second example is a full solution to a challenge problem.
 \end{notate}
 
 \begin{idea}
@@ -2520,9 +2554,11 @@ deal with.
 (Suggest (strategy "eliminate cross terms"))
 
 (Assert (expands "(sqrt(3)+sqrt(2))^2 + (sqrt(3)-sqrt(2))^2"
-                 "2 + 2 sqrt(2) sqrt(3) + 3 + 2 - 2 sqrt(2) sqrt(3) + 3"))
+                 "2 + 2 sqrt(2) sqrt(3) + 3
+                + 2 - 2 sqrt(2) sqrt(3) + 3"))
 
-(Assert (sums "2 + 2 sqrt(2) sqrt(3) + 3 + 2 - 2 sqrt(2) sqrt(3) + 3"
+(Assert (sums "2 + 2 sqrt(2) sqrt(3) + 3
+             + 2 - 2 sqrt(2) sqrt(3) + 3"
               "10"))
 
 ;; (sqrt(3)+sqrt(2))^2012 + (sqrt(3)-sqrt(2))^2012 is an integer
@@ -2591,31 +2627,6 @@ deal with.
          9s in its decimal expansion")
 \end{idea}
 
-\begin{idea}
-(Assert (implies (and "G finite group"
-                      "H subgroup of G"
-                      "[G : H] finite")
-                 "G not equal to union of
-                  ghg^-1"))
-
-(Assert (analogy
-         (implies (and "G finite group"
-                       "H subgroup of G"
-                       "[G : H] finite")
-                  "G not equal to union of
-                   ghg^-1")
-         (implies (and "G infinite group"
-                       "H subgroup of G"
-                       "[G : H] finite")
-                  "G not equal to union of
-                   ghg^-1")))
-
-(Question (implies (and "G infinite group"
-                        "H subgroup of G"
-                        "[G : H] finite")
-                   "G not equal to union of
-                    ghg^-1"))
-\end{idea}
 
 \section{Conclusion} \label{conclusion}
 
-- 
2.11.4.GIT