Walking About a Proof

You can move up and down a proof tree using the . Clicking in some subgoal of the proof window, makes that subgoal the goal of the window. Once you are below the top level of a proof, clicking in the goal of the window moves the proof window up to the parent goal. Click in the only subgoal generated by D 0 THENW Auto. The proof window should look like

$${\Bbb{P}}$$

$$\vdash \forall {\Bbb{P}} \neg \wedge \Longleftrightarrow \neg \vee \neg$$ BY <refinement rule>

Now Click in the goal of this window. The proof window moves back to where it was before. Feel free during the rest of this tutorial to go wandering around the proof tree using . Just make a note first of where you are, so you can find your way back and continue the tutorial. The top line of the proof window always gives the tree address of the node the proof window is at.