This appendix gives a more precise description of the direct computation rules than the one given in chapter 8. It should probably be ignored by those who find the previous description adequate, for the details are rather complicated.
The direct computation rules allow one to modify a goal by directing the system to perform certain reduction steps within the conclusion or a hypothesis. The ``direct'' in ``direct computation'' refers to the fact that no well--formedness subgoals are entailed. The present form of these rules, involving ``tagged terms'' as described in chapter 8, was chosen to provide the user with a high degree of control over what reductions are performed. The tagged terms may be somewhat inconvenient at the rule--box level, but it is expected that the vast majority of uses of these rules will be by tactics.
First, we define what it means
to compute a term for n steps (for n a
nonnegative integer).
To do this we define a
function 
on terms t.
Roughly speaking, 
is the result of doing
computation (as described in chapter 5) on t until it can
be done no further or until a total of n reductions have been
done, whichever comes first. The precise definition is as
follows.
If t is not a
term_of term and not a noncanonical term, or if n is
0, then 
is t. If t is
term_of(name) then 
is 
, where 
is the term extracted from the theorem
named name. If t is a noncanonical term with one
principal argument e then replace e in t by
to obtain 
, and let k be the number
of replacements of redices by contracta done by 
. If n>k, and 
is a redex, then
is 
, where 
is the
contractum of 
. If t is noncanonical with two
principal arguments (e.g., int_eq) then replace the
leftmost one, e, with 
to
obtain 
, and let k be the number of reductions done
by 
.
If 
is not a canonical term of the right
type then 
is 
; otherwise, it is
, where 
is treated as having one (the
second) principal argument.
Having now defined
we can define what it means to do the
computations indicated by a tagging. If T is a term
with tags then the computed form of T is
obtained by successively replacing
subterms of T of the form [[n;t]] or
[[*;t]], where t has no tags in it, by 
or 
, respectively, where
is defined in the obvious way.
It seems very plausible that one should be able to put
tags anywhere in a term.
Unfortunately, it has not yet been proved that this
would be sound, so there is at present a rather
complicated restriction, based on technical considerations,
on the set of subterm occurrences that can
legally be tagged .
Let T be a term and define a relation
on subterm occurrences of T by 
if and only if
u occurs
properly within v. A 
may be tagged
if there are u and v with 
such that:
r is a canonical term, and
