### ACL2-PC::DV

(atomic macro) ` `move to the indicated subterm
```Major Section:  PROOF-CHECKER-COMMANDS
```

```Examples:
(dv 1)    -- assign the new current subterm to be the first argument
of the existing current subterm
(dv 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 `(dv 1)` it is
```(+ a b).
```
If after that, then `(dv 2)` is invoked, the new current subterm will be
```b.
```
Instead of `(dv 1)` followed by `(dv 2)`, the same current subterm could be obtained by instead submitting the single instruction `(dv 1 2)`.

```General Form:
(dv &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: `(dv n)` may be abbreviated by simply `n`, so we could have typed `1` instead of `(dv 1)` in the first example above.

Remark: See also `dive`, which 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`. Thus, the command ```up`'' is the inverse of `dive`, not of `dv`. The following example illustrates this point.

```ACL2 !>(verify (equal (* a b c) x))
->: p ; print user-level term
(EQUAL (* A B C) X)
->: pp ; print internal-form (translated) term
(EQUAL (BINARY-* A (BINARY-* B C)) X)
->: exit
Exiting....
NIL
ACL2 !>(verify (equal (* a b c) x))
->: p
(EQUAL (* A B C) X)
->: 1 ; same as (dv 1)
->: p ; print user-level term
(* A B C)
->: pp ; print internal-form (translated) term
(BINARY-* A (BINARY-* B C))
->: 3 ; dive to third argument of (* A B C)
->: p
C
->: up ; go up one level in (BINARY-* A (BINARY-* B C))
->: p
(* B C)
->: pp
(BINARY-* B C)
->:
```