To use button mnemonics, hold alt and hit the corresponding key.  My apologies to lefties.  On some systems, mnemonics will not work for the first click.

Raw insert/insertion: If one object is selected, it inserts into that object.  Insertion only works on odd levels.

Raw delete/erasure: This behaves as one would expect.  Note that if the SOA is selected, its contents will not be deleted.  Erasure only works on even levels.

Insert double cut: Inserts a double cut around the selection.  If SOA is selected, inserts a double cut into the SOA.  This function attempts to maintain the order of the objects but (of course) this is only partially possible in the case of objects which are not adjacent being placed in a double cut.  If no objects are selected and exactly one cut is cited, inserts a double cut into the citation (as opposed to inserting it around a selection).

Iteration: Copies the cited cuts/premises into the selected cut.

Deiteration: Deletes the selected cuts/premises based on the cited cuts/premises.  Ignores unnecessary citations.

Remove double cut: Removes a double cut.  Inner or outer cut may be selected.  Will only work if exactly one cut is selected.

Selecting objects: Clicking an object selects it.  Right-clicking an object cites it.  Clicking an object again deselects/uncites it.  You can deselect and select an item in one step if you try to cite an already selected object or try to select an already cited object.  Selecting (or citing) an object with a different parent will clear all selections (or citations) before selecting the object.  Middle-clicking a cut (or the SOA) will clear all selections, clear all citations, and select every cut/premise inside of the cut that was clicked.  This is purely for convenience; the same task can be performed without middle-clicking.


Special rule notations:
RI: or RE:		Indicates reiteration.  The line in any proof is, "[.X]", where X is the conclusion.  X is derived from the previous line.  Used to deal with fencepost issues (see below)

RA:			Indicates "Raw" rules (Raw deletion and Raw insertion).


The inference graph:
Each node represents an inference step.  Individual inferences can be dragged around.  If an inference is selected, the premise and conclusion of the inference is displayed.  Mousing over an inference on the inference graph will change the status bar to indicate if the inference is valid.  Note that seemingly valid custom inferences might show as invalid if they are incorrectly applied at an odd or even level.  Links between inferences are color-coded as follows:
Green: The conclusion of the source matches the premise of the destination
Yellow: The conclusion of the source matches the conclusion of the destination.  If a link is yellow, it means the source
can link to anything the destination links to.  It also means the destination is redundant.  Yellow links are technically invalid but can be trivially fixed.
Red: The two inferences do not link.

If a single cut is selected when applying custom inferences, the program treats that as selecting the empty subgraph within that cut.  If you prefer to select the contents of the cut, select them.  A single cut cannot be selected.
Right click menu:
Right clicking nodes brings up a menu.  Note that it is useful to right click a node that is not selected.
Set Premise/Conclusion: This sets the selected node to be the premise or conclusion of the proof or custom inference.  Note
that the premise node refers to the premise of the node whereas the conclusion refers to the conclusion.  Setting a node to be both premise and conclusion is permissable and means your proof has exactly one inference.
Reiterate: Creates a reiteration node linking from the conclusion of the clicked node.
Pre-iterate: Creates a reiteration node linking to the premise of the clicked node.
Delete: Deletes the node.  You cannot delete a currently selected node.
Connect:Makes a connection from the currently selected node to the clicked node.  Note that custom inferences
can only have one connection in and one connection out.
Disconnect: Breaks a connection from the currently selected node to the clicked node.
Copy: Makes a copy of the node.
Customize: Customizes a custom inference.  This enables you to rename variables and add additional propositions to the inference.  To edit the custom inference, double click it.  Double click the black triangle to stop editting.

File menu:
Save/Load: Saves or loads a proof in XML format.
Export/Import Pegasus: Saves or loads a proof in Pegasus format.  Loading adds the Pegasus proof the the current inference graph.  Because Pegasus files are linear, you must mark a premise node and a conclusion node.  If no path between the two nodes exists, saving will fail.
Add custom inference: Adds a custom inference.  Custom inferences are regular xml proofs.

Tools:
Toggle Odd Mode: If the custom inference being created is for use on odd levels, toggle odd mode before starting the proof.  In odd mode, the sheet of assertion is treated as being a graph at an odd level.
Reverse Proof: This reverses the proof, making it into its contrapositive.  If editting a custom inference, only the inference will be reversed.   As a side effect, odd mode is toggled.  Reversing the proof may be useful if working from the conclusion seems easier than working from the premise.
Check proof: This checks the proof (or custom inference, if working on one).  You can check individual inferences by mousing over them.  Note that a custom inference with all valid steps may be invalid if it applied at an incorrect level.

Tip:Apparently valid applications of iterations may be internally stored without proper citation, resulting in an invalid inference.  This should not happen unless external programs are used to generate or edit proof files.