From: Claudio Sacerdoti Coen Date: Fri, 30 May 2003 17:17:58 +0000 (+0000) Subject: final ispell X-Git-Tag: submitted~1 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=f41a5585a648d57e4d8a24d664b0a5ce5d591148 final ispell --- diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex index 2625d6b7d..dd2ad61e8 100644 --- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex +++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex @@ -295,18 +295,18 @@ the user the scalar to use as an argument of the previous lemma; the second one states that the scalar is different from 0; the third lemma (the main one) asks to prove the equality between the two new members. % is shown in Fig. \ref{step2} where $?_3[H;x]$ stands for -% the still unkown scalar argument, which can have only $H$ and $x$ as +% the still unknown scalar argument, which can have only $H$ and $x$ as % free variables. -The user proceeds by istantiating the scalar with the number 2. The +The user proceeds by instantiating the scalar with the number 2. The \texttt{Assumption} tutor now suggests to close the second goal (that states that $2 \neq 0$) by applying the hypothesis $H$. No useful suggestions, instead, are generated for the main goal $2*x = 2*((x+1)*(x+1)-1-x*x)*2^{-1}$. -To proceed in the proof the user needs to symplify the +To proceed in the proof the user needs to simplify 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 -suggesting symplifications, the user must find out this symplication by +suggesting simplifications, the user must find out this simplification by himself. Once she founds it, the goal is reduced to proving that $2*x = (x+1)*(x+1) - 1 - x*x$. This equality is easily solved by the \texttt{Ring} tutor, that suggests\footnote{The \texttt{Ring} suggestion is