A proof in Nuprl may be thought of as a tree . Associated with each node of the tree is a sequent and, if the node is not a leaf, a rule. A sequent is in turn composed of a numbered list of hypotheses and a goal. The children of a node are uniquely determined by the sequent and rule of that node. If no rule is present, or if the rule is incorrect or not applicable, the node has no children; otherwise, the children correspond to the subgoals generated by the application of the rule to the sequent. Note the departure from conventional usage; a proof need not be complete.

The following example from a Nuprl
session was obtained
by using the command ` view example` to create a window for
the theorem object ` example` and then using the refinement editor,
or * red* for short, to navigate through the proof tree.

,-------------------------------------, |EDIT THM example | |-------------------------------------| |# top 1 1 | |1. x:int | |2. y:int | |>> z:int->(x*(y+z)=x*y+x*z in int) | | | |BY intro | | | |1# 1. x:int | | 2. y:int | | 3. z:int | | >> (x*(y+z)=x*y+x*z in int) | | | |2# 1. x:int | | 2. y:int | | >> int in U1 | '-------------------------------------'

Displayed in the window above
is the sequent to be proven, or * main goal*,
associated with the current node,
the rule of the node
(preceded by ` BY`), and the
sequents corresponding to the two children
of the node. This is the way that
the system displays a proof tree in a theorem window;
it shows a sequent, the rule applied to it (if any), and
the immediate subgoals.
The location of the node in the tree is
given by the header, ` top 1 1` in this case; this means that
the node is the first child of the
first child of the root of the proof tree. The sign ``#'' indicates
that the * status* of the subproof is
* incomplete* . Other possible statuses are:
``` -`'' for * bad* , meaning that some descendant
(leaf) has an incorrect rule application, or that the
main goal was not acceptable; ``?'' for * raw* , which
is the status of the proof before the main goal has been
parsed; and ``*'' for * complete* , which indicates that the subproof
has been finished.

One usually visualizes a tree as having its root at the top (or bottom) with the branches going downward (upward). In Nuprl , however, a proof tree should be viewed as lying on its side, with the root at the left and with the first child of a given node being at the same height as its parent, and having its siblings below it. Keeping this in mind will make the commands for moving around in proof trees easier to remember.

Thu Sep 14 08:45:18 EDT 1995