...

[helm.git] / helm / papers / calculemus-2003 / hbugs-calculemus-2003.tex

diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
index 22036320c318cc0a0117ca56dc0db0936f8c8ca2..b79b81a7425c00c5181185eb54993a63b7b0b5fb 100644 (file)
--- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
+++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
@@ -247,8 +247,8 @@ x = \frac{(x+1)*(x+1) - 1 - x*x}{2}
 \end{displaymath}
 \end{exercise}
 
-\myincludegraphics{step1}{t}{12cm}{Example session, snapshot 1.}
-  {Example session, snapshot 1.}
+\myincludegraphics{step1}{t}{12cm}{Example session.}
+  {Example session.}
 %\myincludegraphics{step2}{t}{4cm}{Example session, snapshot 2.}
 % {Example session, snapshot 2.}
 
@@ -270,7 +270,7 @@ of the window in background in Fig. \ref{step1}.
 While the user is wondering how to proceed in the proof, the tutors are
 trying to progress in the proof. After a while, the tutors' suggestions
 start to appear in the lower part of the \hbugs{} interface window
-(the topmost window in Fig. \ref{prima}). In this case, the tutors are able
+(the topmost window in Fig. \ref{step1}). In this case, the tutors are able
 to produce 23 hints. The first and not very useful hint suggests to proceed in
 the proof by exchanging the two sides of the equality.
 The second hint suggests to reduce both sides of the equality to their normal
@@ -301,7 +301,7 @@ with the scalar.
 The user proceeds by istantiating the scalar with the number 2. The
 \texttt{Assumption} tutor now suggests to close the second goal by applying
 the hypothesis $H$. No useful suggestions, instead, are generated for the
-main goal $2x = 2*\frac{((x+1)*(x+1)-1-x*x)}{2}$.
+main goal $2x = 2*((x+1)*(x+1)-1-x*x)*2^{-1}$.
 To proceed in the proof, indeed, the user needs to symplify the
 expression using the lemma $Rinv\_r\_simpl\_m$ that states that
 $\forall x,y.\;y = x * y * x^{-1}$. Since we do not provide yet any tutor