+\label{usage}
+In this section we describe a typical \hbugs{} session. The aim of the
+session is to solve the following easy exercise:
+\begin{exercise}
+Let $x$ be a generic real number. Using the \helm{} proof-engine,
+prove that
+\begin{displaymath}
+x = \frac{(x+1)*(x+1) - 1 - x*x}{2}
+\end{displaymath}
+\end{exercise}
+
+Let us suppose that the \hbugs{} broker is already running and that the
+tutors already registered themselves to the broker.
+When the user starts our proof-engine \texttt{gTopLevel}, the system registers itself to
+the broker, that sends back the list of available tutors. By default,
+\texttt{gTopLevel} notifies to the broker its intention of subscribing to every
+tutor available. The user can always open a configuration window where she
+is presented the list of available tutors and she can independently subscribe
+and unsubscribe herself to each tutor.
+
+\myincludegraphics{step1}{t}{12cm}{Example session.}
+ {Example session.}
+%\myincludegraphics{step2}{t}{4cm}{Example session, snapshot 2.}
+% {Example session, snapshot 2.}
+
+The user can now insert into the system the statement of the theorem and start
+proving it. Let us suppose that the first step of the user is proving
+that the denominator 2 is different from 0. Once that this technical result
+is proven, the user must prove the goal shown in the upper right corner
+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{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
+form by using only reductions which are justified by the ring structure of the
+real numbers; the two normal forms, though, are so different that the proof is
+not really simplified.
+All the residual 21 hints suggest to apply one lemma from the distributed
+library of \helm{}. The user can look at the statement of any lemma by clicking
+on its URI.
+
+The user can now look at the list of suggestions and realize that a good one is
+applying the lemma \texttt{r\_Rmult\_mult} that allows to multiply both equality
+members by the same scalar\footnote{Even if she does not receive the hint, the
+user probably already knows that this is the right way to proceed. The
+difficult part, accomplished by the hint, is guessing what is the name of the
+lemma to apply.}.
+Double-clicking on the hint automatically applies
+the lemma, reducing the proof to closing three new goals. The first one asks
+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 unknown scalar argument, which can have only $H$ and $x$ as
+% free variables.
+
+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 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 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
+just one of the 22 hints that the user receives. It is the only hint that
+does not open new goals, but the user right now does not have any way to know
+that.} to the user how to complete the proof in one macrostep.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Comandi da dare a gTopLevel %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% New proof:
+% !x.(not (eqT ? (Rplus R1 R1) R0)) -> (eqT ? x (Rdiv (Rminus (Rminus (Rmult (Rplus x R1) (Rplus x R1)) R1) (Rmult x x)) (Rplus R1 R1)))
+% Intros x H
+% Apply r_Rmult_mult
+% 3: Apply H
+% Simpl (per fare unfold di Rdiv)
+% Rewrite <-
+% (Rmult_assoc (Rplus R1 R1) (Rplus (Rplus (Rmult (Rplus x R1) (Rplus x R1)) (Ropp R1)) (Ropp (Rmult x x))) (Rinv (Rplus R1 R1)))
+% Rewrite ->
+% (Rinv_r_simpl_m (Rplus R1 R1) (Rplus (Rplus (Rmult (Rplus x R1) (Rplus x R1)) (Ropp R1)) (Ropp (Rmult x x))) H)
+% *** Ring
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%