+ <sect1 id="proofstatus">
+ <title>The proof status</title>
+ <para>
+ During an interactive proof, the proof status is made of
+ the set of sequents to prove and the partial proof built so far.
+ </para>
+ <para>The partial proof can be <link linkend="aboutproof">inspected</link>
+ on demand in the CIC browser. It will be shown in pseudo-natural language
+ produced on the fly from the proof term.</para>
+ <para>The set of sequents to prove is shown in the notebook of the
+ <link linkend="authoringinterface">authoring interface</link>, in the
+ top-right corner of the main window of Matita. Each tab shows a different
+ sequent, named with a question mark followed by a number. The current
+ role of the sequent, according to the following description, is also
+ shown in the tab tag.
+ </para>
+ <orderedlist>
+ <listitem id="selectedsequents">
+ <para>
+ <emphasis role="bold">Selected sequents</emphasis>
+ (name in boldface, e.g. <emphasis role="bold">?3</emphasis>).
+ The next tactic will be applied to every selected sequent, producing
+ new selected sequents. <link linkend="tacticals">Tacticals</link>
+ such as branching ("<emphasis role="bold">[</emphasis>")
+ or "<emphasis role="bold">focus</emphasis>" can be used
+ to change the set of selected sequents.
+ </para>
+ </listitem>
+ <listitem id="siblingsequents">
+ <para>
+ <emphasis role="bold">Sibling sequents</emphasis>
+ (name prefixed by a vertical bar and their position, e.g.
+ |<subscript>3</subscript>?2). When the set of selected sequents
+ has more than one element, the user can decide to focus in turn on each
+ of them. The branching <link linkend="tacticals">tactical</link>
+ ("<emphasis role="bold">[</emphasis>") selects the first
+ sequent only, marking every previously selected sequent as a sibling
+ sequent. Each sibling sequent is given a different position. The
+ tactical "<emphasis role="bold">2,3:</emphasis>" can be used to
+ select one or more sibling sequents, different from the one proposed,
+ according to their position. Once the user starts to work on the
+ selected sibling sequents it becomes impossible to select a new
+ set of siblings until the ("<emphasis role="bold">|</emphasis>")
+ tactical is used to end work on the current one.
+ </para>
+ </listitem>
+ <listitem id="solvedsequents">
+ <para>
+ <emphasis role="bold">Automatically solved sibling sequents</emphasis>
+ (name strokethrough, e.g. |<subscript>3</subscript><emphasis role="strikethrough">?2</emphasis>).
+ Sometimes a tactic can close by side effects a sibling sequent the
+ user has not selected yet. The sequent is left in the automatically
+ solved status in order for the user to explicitly accept
+ (using the "<emphasis role="bold">skip</emphasis>"
+ <link linkend="tacticals">tactical</link>) the automatic
+ instantiation in the proof script. This way the correspondence between
+ the number of branches in the proof script and the number of sequents
+ generated in the proof is preserved.
+ </para>
+ </listitem>
+ </orderedlist>
+ </sect1>