Skip to main content
PRL Project

How to Step through a Proof


Here we illustrate how to step through a proof, using the following theorem as an example: ∀[A,B:ℙ]. (A ⇒ B ⇒ A)

⊢ ∀[A,B:ℙ]. (A ⇒ B ⇒ A) | BY (UD THENA Auto) | [1]. A:ℙ ⊢ ∀[B:ℙ]. (A ⇒ B ⇒ A) | BY (UD THENA Auto) | [2]. B:ℙ ⊢ A ⇒ B ⇒ A | BY (D 0 THENA Auto) | 3. A ⊢ B ⇒ A | BY (D 0 THENA Auto) | 4. B ⊢ A | BY NthHyp 3


To step through the proof in the frame below, start by clicking on the Proof link.




This should take you to the following frame, where you see the first step of the proof. This step results in a single branch to continue the proof. To see the next step, follow the first (and only) branch by clicking on the link labeled 1. If there were two subgoals to prove after this step, then there would be two links to follow, 1 and 2. You will see this in other proofs.




You should now see the following frame. You can continue stepping through the proof in this manner until you reach the end of a branch, when there are no more numbered links to follow. Note that the top line of the frame keeps a list of links to each of the proof steps, so that you can go back if necessary. The link labeled * will take you back to the first step, and the link labeled with the lemma name will take you out of the proof and back to the statement of the theorem.