Rodin Proving Perspective

<prev: The Proof Obligation Explorer

>next: The Mathematical Language

^up: User_Manual_index

Loading a Proof

In order to load a proof, enter the Proof Obligation window, select the project, select and expand the component, finally select the proof obligation: the corresponding proof will be loaded. As a consequence:

• the proof tree is loaded in the Proof Tree window. As we shall see in section 6.2, each node of the proof tree is associated with a sequent.
• In case the proof tree has some "pending" nodes (whose sequents are not discharged yet) then the sequent corresponding to the first pending node is decomposed: its goal is loaded in the Goal window (section 6.3), whereas parts of its hypotheses (the "selected" ones) are loaded in the Selected Hypotheses window (section 6.3).
• In case the proof tree has no pending node, then the sequent of the root node is loaded as explained previously.