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.