Rodin HandbookThis work is sponsored by the Deploy Project This work is sponsored by the ADVANCE Project This work is licensed under a Creative Commons Attribution 3.0 Unported License 
2.9.6 The First ProofIn this section, we will carry out proofs for the model of the Celebrity Problem. To do this, click on the box in the upper right hand corner that has a little plus sign and switch to the Proving Perspective. You can switch between perspectives using the shortcut bar as shown in Figure 2.17.
We should now see the window in Figure 2.18. The Proving Perspective contains three new important views:
Expand the Celebrity_1 machine in the EventB Explorer. Then expand the Proof Obligations section. We can see that the auto prover (3.1.7.5) did quite a good job. Only three proofs have not been completed^{1} (a completed proof is indicated by a green mark ).
Let’s start with the proof remove_1/inv2/INV of Celebrity_1. To do this, double click on the proof obligation remove_1/inv2/INV. We should now see the window as shown in Figure 2.19.
Here we need to prove that the event remove_1 preserves the invariant inv2, . The event’s action assigns the new value to . Because we know that invariant was valid before the assignment, it is sufficient to prove that we do not remove from , i.e. . Type this into the Proof Control View (3.1.7.4) and press the button.
Take a look at the Proof Tree View. The root node should now be labelled with ah (), which is the hypothesis that we just added. This node has three children: The first proves that is welldefined^{2}, which is and has already been trivially proven. The second is the proof of the hypotheses . The third is the proof of the original goal where the new hypotheses can be used. The new goal is . Now, try selecting the right hypotheses by yourself in order to complete the proof (Hint: What axiom states that the celebrity does not know anybody?). To do this, click on the button in the Proof Control View. On the left side we should see now the Search Hypotheses view (see Figure 2.20). If you cannot find the right hypotheses, you may also just select all hypotheses. To add the selected hypothesis to the Selected Hypotheses View just click on the button.
The correct hypothesis for this proof was (axiom 3 from the first context). If you were unable to figure this out, add this hypothesis to the selected hypothesis window now. Now click on the button to prove the goal with the Predicate prover on selected hypothesis. The goal should be discharged and in the Proof Tree you should see that the first two children of the root node are proven. The Proof Control View should now show the original goal and is now one of our hypotheses.^{3} Click a second time on the button in order to finalize the proof. The smiley in the Proof Control View should now become green indicating that all sequents of the proof tree are discharged as shown in Figure 2.21. After saving the proof, the proof obligation remove_1/inv2/INV in the EventB Explorer should now have a next to it.
In order to move to the next undischarged proof obligation, you may also use the Next Undischarged PO button ( ) of the Proof Control View (3.1.7.4). The next proof can be solved the same way as the last one.
Footnotes
