PCP: Brief Instructions and Description  Peter Jipsen, 2001  The
PCP system splits the browser window vertically into two frames.
The left frame contains the (partial) proof, and the narrower
right frame contains the possible choices available for the next
step.  Initially the proof frame contains a list of axioms and
formulas to be proved, with the latter preceded by a line of the
form ...^...v...  This line indicates a gap in a proof and the
two arrow symbols point at the line above and below the gap
respectively. Each symbol is a button that can be clicked to
direct the focus of subsequent actions to that line of the
proof. The line with the current focus has an undo button
instead of one of the arrow symbols, and also a hide/show
button.  The undo button deletes the focus step of the proof
(although main level proof steps cannot be undone presently).
The hide/show button allows subproofs and other gaps to be
hidden so that the user can focus on the part of the proof that
is currently of interest.  Each p