This page describes proof structure and browsing by inference step.
There are also Print Forms for Proofs .

The various links pertaining to a proof are accessed from its inference step pages.

Walking and Reading

In Nuprl, proofs are trees of assertions, each assertion being a sequence of assumptions and variable declarations together with a conclusion. Each node is considered as a goal whose subgoals are its children; a goal follows from its subgoals. The subgoals are generated from the goal by a justification called a "tactic" which is an executable explanation of how to justify the inference to the goal from the subgoals by means of various primitive inference rules.

A goal with an empty list of subgoals is completely proved. ( Example )

A proof object in Nuprl will be a proof tree whose topmost goal has no assumptions or variable declarations.

Proof objects are typically referred to by a citation of the main goal along with a link to the proof top. Normally, citations of lemmas in the justification of an inference are presented this way. ( Example )

Interactive examination of proofs must for now proceed one inference step at a time. Each page containing an inference step includes:

The goal.
The numbered subgoals.
The tactic justifying the inference.
The name of the object containing the inference step.
The address of the inference step within the whole proof tree.

The address is a list of integers, and each numeral in the address is presented as a link to the node with the appropriate address, which makes it easier to jump up to a higher node in the tree.

The subgoals of an inference are numbered, and if the proof of the subgoal is non-trivial, then the numeral is presented as a link to the inference having the subgoal as its goal. This is how you walk down the proof tree. ( Example -- the proof of subgoal 2 is considered trivial, and so is not accessible.)

To save space and ease reading, when an initial segment of the hypotheses and declarations is inherited from the goal, they are elided in the subgoal. If you follow the link into the subproof, the elided elements are restored in the goal of the subproof. ( Example )

Auxiliary Links

The usual right hand corner links may be expected, and the Definitions link is especially valuable for understanding the inference, as it shows all the definitions pertinent to the page content.
In addition to possible "Remarks", proofs may also be provided with informal glosses pointed at by "Gloss" ( for the proof that 2 has no rational square root ).

Proofs are also provided with a PrintForm link to a postscript file of the whole proof suitable for printing.
When a proof cites lemmas, a list of them can be found with the Lemmas button.

The tactic justifying an inference may mention or consist of a Side Proof , which may be read like an ordinary proof. Letters in place of numbers in proof step addresses indicate branches into side proofs.