The command `(c-d)' is considered the "normal"; for detail, do a `show' or `(cm-(mouseright))' on the relevant commands.

Insertion of a term X on top of a term Y will have an effect conditioned on the settings of three user settable bits:

left/right mode `{(c-w)(m-w)(c-i)}' toggles insert/replace mode `{(c-r)(m-r)}' sets replace-mode display-/term-struct mode `(c-u){(c-r)(m-r)}' sets term-struct mode

`(c-b)' and term insertion commands restore these bits to normal, namely: left-mode, insert-mode, display-structure-mode

In insert-mode, the point Y will be replaced by X, then Y is put into the left-most(right-most) term-slot of X, if there is one.

In replace-mode `{(c-r)(m-r)}', the point Y will be replaced by X.
The text slots of X will then be filled by the text children of Y from left-to-right (right-to-left). It is similar for the term slots of X and the term children of Y.
However, what is meant by children of Y and the left/right order is determined by the setting of the display-/term-structure mode `(c-u){(c-r)(m-r)}'.

N.B.:

When a term is displayed, some of the text- or term-children of the underlying term may be elided from display, and the order of the children in display may differ from the order they have in the underlying term.

There are several possible sources for X, selected by the various edit commands.

the term clicked on	`(mouseleft)' on <term to insert> and its variants
the term at the point (if not a slot)	`(m-(mouseright))' `(c-c)' `(c-a)(c-c)'
top of stack (doc for cut n paste)	`(c-p)'
2nd from top (doc for cut n paste)	`{(m-p)(cm-p)}'
referenced operator instance	`;' immediately followed by object name `;;' on an ABS or DISP reference (doc for ob refs)

Lots of commands are defined explicitly to insert specific operators.
The commands `(c-a)(c-?)' and `(cm-(mousemiddle))' will often show a keyboard command for inserting the operator that is at the point.

EXCEPTIONS:

Replace-mode will usually be forced when inserting a 1-place text operator on top of an instance of a 1-place text operator. Thus, `(c-t)' will usually convert a text operator to the appropriate form. Pasting one inference steps is different; doc for proof refinement2.

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html