The proofs that you will be asked to read have all been adapted to be
available and you will be reading them that way. (Note: If you are a
Nuprl user and would prefer to read these proofs in a different format,
that is fine but please indicate this to me.)
In the web presentation of a proof, each step of the proof is given
on a separate page and you traverse the proof tree by following links
that take you from node to node in the tree. Each page presents five
pieces of information about this step in the proof: the level, the
hypotheses, the conclusion, the applied tactic and the generated subgoals.
These five pieces of information are labeled on the page in red letters
and horizontal lines divide the page into four sections, one for the
level, one for the hypothesis and conclusion, one for the applied tactic
and one for generated subgoals. To see this, take a look at this
sample proof.
The hypotheses are given in a number list; they are the set of valid premises
to use for proving the current goal. The current goal is labeled as the
conclusion. The conclusion can be referred to by the number 0 in tactics as
if it were a hypothesis; hypotheses are only given numbers greater than 0.
the applied tactic is the tactic which the user has chosen to apply to the
current goal and hypothesis in order to make progress in the proof. The
generated subgoals are the new subgoals which need to be proved after the
tactic is applied to the current goal. The subgoals are also numbered; to
see how a subgoal is proved one clicks on the number next to the subgoal and
is taken to the page for that node of the proof tree. The level information
keeps track of where in the proof tree one is. The top of the proof tree is
indicated by the level label "Top" and each subsequent node which is
visited is indicated by the number of the subgoal which was followed to get
to the new node. In this way, one can traverse the entire proof tree by
clicking on subgoal numbers to descent into the proof tree and by using
the back button or by clicking on the level labels given in the top "Level"
section on the page to rise back up through the proof tree.
The top node of a proof tree shows the theorem to be proved as the conclusion
and there are no hypotheses. A leaf of the proof tree is reached when no
subgoals are generated after a tactic is applied.
If you explore the
sample proof
in this way you will find that it is a proof tree with three nodes and only
one branch at each node.
