There is a postscript form of each proof that can be raised with the "PrintForm" button in the corner of any inference step page.
(You may need to configure your browser to view postscript files.)

For example, this is the print form for Thm* x:. y:. yyx & x < (y+1)(y+1).

If an inference step has only one subgoal, it appears aligned beneath the goal. If an inference has two or more subgoals they are all aligned with each other, but indented from the goal. Sequences of "|" and "\" characters are used to lead the eye to subgoals. So each "|" character to the left of a line in the proof leads downward to another goal that is neither an ancestor nor descendant. A simple "." character is used as a place holders where a "|" would have appeared had there been a goal for it to lead down to; this makes it easier to track ones nesting depth than if blank space were used, especially in a long proof with a lot of branching, such as this one.

The pages for individual Inference Steps form the organizational heart of proof presentation, but the print form for a proof has notable advantages.

The benefits of the print form are that the entire proof is shown, and indentation is used extensively, making large formulas more readable than our HTML pages (we will adopt better indentation controls later).

The printform has no links, so the only way to analyze the contents of a proof with the browser is through an individual Inference Step of a Proof .

Side proofs are printed after the main proof, in a preorder traversal.