#### `library(termdepth)`

Many resolution-based theorem provers impose a depth bound on the terms they create. Not the least of the reasons for this is to prevent infinite loops. `library(termdepth)` provides five predicates:

`term_depth(`+Term`, `-Depth`)`
Depth is unified with the depth of Term, calculated according to the following definition:
```          term_depth(Var) = 0
term_depth(Const) = 0
term_depth(F(T1,...,Tn)) =
1 + max(term_depth(T1), ..., term_depth(Tn))
```

`depth_bound(`+Term`, `+Bound`)`
This succeeds when the depth of Term, as calculated by `term_depth/2`, is less than or equal to Bound. Bound is assumed to be a strictly positive integer. Note that `depth_bound/2` will terminate even if Term is cyclic.
`term_size(`+Term`, `-Size`)`
Unify Size with the size of Term, where the size is the number of constants and function symbols in the term. (Note that this is a lower bound on the size of any term instantiated from Term, and that instantiating any variable to a non-variable must increase the size. This latter property is why variables are counted as 0 rather than as 1.) The definition is
```          term_size(Var) = 0
term_size(Const) = 1
term_size(F(T1,...,Tn)) =
1 + term_size(T1) + ... + term_size(Tn).
```

`size_bound(`+Term`, `+Bound`)`
This succeeds when the size of Term, as calculated by `term_size/2`, is less than or equal to Bound. Bound is assumed to be a non-negative integer. Note that `size_bound/2` will always terminate even if Term is cyclic.
`length_bound(`+List`, `+Bound`)`
is true when List is a list having at most Bound elements. Bound must be instantiated. If List ends with a variable, it will be instantiated to successively longer proper lists, up to the length permitted by Bound. Note that the depth of a list of constants is its length.