ACL2-PC::DIVE

(primitive) ` `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 that
```
For 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.

Note: `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`.