From 94d22c3c285724d0e337f26fb04885d90d4f7c96 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 30 May 2003 15:20:28 +0000 Subject: [PATCH] ... --- helm/papers/calculemus-2003/hbugs-calculemus-2003.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex index 945740cf8..b79b81a74 100644 --- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex +++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex @@ -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 -- 2.39.2