Proof Window Format

Each proof window  is associated with a node of a proof. It shows the goal sequent at that node, the refinement rule if any at that node and any immediate subgoals  .

  
Figure: Proof Window on Refined Proof Node

  
Figure: Proof Window on Unrefined Proof Node

Figure shows an example of a window onto a refined node of a proof, and Figure shows an example of a window onto an unrefined node of a proof.

The numbered parts of these windows are as follows:

The EDIT  indicates that the proof is being viewed in edit modeedit mode  . In this mode the proof can be changed. This is replaced by SHOW  if the proof is viewed in the read-only mode  . The THM indicates that a theorem object is being viewed, and cantor is the name of the theorem.

The #  indicates that this proof node is considered incomplete. Other symbols used here, are   for complete and -  for bad. the top 1 1 and the top 1 1 2 are tree addresses  of the nodes being viewed. Figure shows the 1st child of the 1st child of the root of the proof, and Figure shows the 2nd child of the proof node in Figure .

This is the goal sequent of the proof node.

This is a tactic which was executed on the goal above in order to generate the subgoals below. The BY  is part of the proof node display  , and is not part of the tactic.

This is the refinement rule placeholder.

These are the subgoals of the proof node. Each one is numbered. The * or # by the subgoal number shows the status of the subproof. The symbols are the same as those for the goal. Note that for brevity, only hypotheses which have changed or been added are displayed in the subgoal sequents.

Sometimes the proof window is too short to display all the goal, rule, and subgoals. In this case the cursor motion commands described in section 4.4.2.1 will automatically scroll the window. One can of course also resize the window.