The proof editor, red (for refinement editor), is invoked when the view command is given on a theorem object. The proof editor window always displays the current node of the proof. When the editor is first entered the current node is the root of the tree; in general, the current node can be changed by going into one of its subgoals or by going to its parent. For convenience there are also ways to jump to the next unproved leaf and to the root of the theorem.
Figure: A Sample Proof Editor Window
Figure shows a sample proof editor window. The parenthesized numbers it contains are referenced below.
b:int # ((a=b in int)|((a=b in int) -> void)) in U1.
((a=b in int) | ((a=b in int) -> void)) in U1.
Notice that lines (2), (6) and (7) have asterisks, which serve as status indicators. The asterisk in line (2) means that this entire subgoal has the status complete; similarly, the asterisks in lines (6) and (7) mean that the two subgoals also are complete. Other status indicators are # (incomplete), - (bad), and ? (raw).