` `

move to the indicated subterm
Major Section: PROOF-CHECKER-COMMANDS

Examples: (DIVE 1) -- assign the new current subterm to be the first argument of the existing current subterm (DIVE 1 2) -- assign the new current subterm to be the result of first taking the 1st argument of the existing current subterm, and then the 2nd argument of thatFor example, if the current subterm is

(* (+ a b) c),then after

`(dive 1)`

it is
(+ a b).If after that, then

`(dive 2)`

is invoked, the new current subterm
will be
b.Instead of

`(dive 1)`

followed by `(dive 2)`

, the same current subterm
could be obtained by instead submitting the single instruction
`(dive 1 2)`

.

General Form: (dive &rest naturals-list)If

`naturals-list`

is a non-empty list `(n_1 ... n_k)`

of natural
numbers, let the new current subterm be the result of selecting the
`n_1`

-st argument of the current subterm, and then the `n_2`

-th subterm
of that, ..., finally the `n_k`

-th subterm.**Remark:** `Dive`

is related to the command `pp`

, in that the diving
is done according to raw (translated, internal form) syntax. Use the
command `dv`

if you want to dive according to the syntax displayed by
the command `p`

. Note that `(dv n)`

can be abbreviated by simply `n`

.