This is documentation for ACL2 Version 3.0
Copyright (C) 2006  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Written by:  Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.

FAILED-FORCING    how to deal with a proof failure in a forcing round

See FORCING-ROUND for a background discussion of the notion of
forcing rounds.  When a proof fails during a forcing round it means that
the "gist" of the proof succeeded but some "technical detail" failed.
The first question you must ask yourself is whether the forced goals are
indeed theorems.  We discuss the possibilities below.

If you believe the forced goals are theorems, you should follow the
usual methodology for "fixing" failed ACL2 proofs, e.g., the
identification of key lemmas and their timely and proper use as rules.
See FAILURE and see PROOF-TREE.

The rules designed for the goals of forcing rounds are often just what
is needed to prove the forced hypothesis at the time it is forced.
Thus, you may find that when the system has been "taught" how to prove
the goals of the forcing round no forcing round is needed.  This is
intended as a feature to help structure the discovery of the necessary
rules.

If a hint must be provided to prove a goal in a forcing round, the
appropriate "goal specifier" (the string used to identify the goal to
which the hint is to be applied) is just the text printed on the line
above the formula, e.g., "[1]Subgoal *1/3"".  See GOAL-SPEC.

If you solve a forcing problem by giving explicit hints for the goals of
forcing rounds, you might consider whether you could avoid forcing the
assumption in the first place by giving those hints in the appropriate
places of the main proof.  This is one reason that we print out the
origins of each forced assumption.  An argument against this style,
however, is that an assumption might be forced in hundreds of places in
the main goal and proved only once in the forcing round, so that by
delaying the proof you actually save time.

We now turn to the possibility that some goal in the forcing round is
not a theorem.

There are two possibilities to consider.  The first is that the original
theorem has insufficient hypotheses to ensure that all the forced
hypotheses are in fact always true.  The "fix" in this case is to amend
the original conjecture so that it has adequate hypotheses.

A more difficult situation can arise and that is when the conjecture has
sufficient hypotheses but they are not present in the forcing round
goal.  This can be caused by what we call "premature" forcing.

Because ACL2 rewrites from the inside out, it is possible that it will
force hypotheses while the context is insufficient to establish them.
Consider trying to prove (p x (foo x)).  We first rewrite the formula in
an empty context, i.e., assuming nothing.  Thus, we rewrite (foo x) in
an empty context.  If rewriting (foo x) forces anything, that forced
assumption will have to be proved in an empty context.  This will likely
be impossible.

On the other hand, suppose we did not attack (foo x) until after we had
expanded p.  We might find that the value of its second argument, (foo
x), is relevant only in some cases and in those cases we might be able
to establish the hypotheses forced by (foo x).  Our premature forcing is
thus seen to be a consequence of our "over eager" rewriting.

Here, just for concreteness, is an example you can try.  In this
example, (foo x) rewrites to x but has a forced hypothesis of (rationalp
x).  P does a case split on that very hypothesis and uses its second
argument only when x is known to be rational.  Thus, the hypothesis for
the (foo x) rewrite is satisfied.  On the false branch of its case
split, p simplies to (p1 x) which can be proved under the assumption
that x is not rational.

     (defun p1 (x) (not (rationalp x)))
     (defun p (x y)(if (rationalp x) (equal x y) (p1 x)))
     (defun foo (x) x)
     (defthm foo-rewrite (implies (force (rationalp x)) (equal (foo x) x)))
     (in-theory (disable foo))

The attempt then to do (thm (p x (foo x))) forces the unprovable goal
(rationalp x).

Since all "formulas" are presented to the theorem prover as single terms
with no hypotheses (e.g., since implies is a function), this problem
would occur routinely were it not for the fact that the theorem prover
expands certain "simple" definitions immediately without doing anything
that can cause a hypothesis to be forced.  See SIMPLE.  This
does not solve the problem, since it is possible to hide the
propositional structure arbitrarily deeply.  For example, one could
define p, above, recursively so that the test that x is rational and the
subsequent first "real" use of y occurred arbitrarily deeply.

Therefore, the problem remains: what do you do if an impossible goal is
forced and yet you know that the original conjecture was adequately
protected by hypotheses?

One alternative is to disable forcing entirely.  See
DISABLE-FORCING.  Another is to disable the rule that caused the
force.

A third alternative is to prove that the negation of the main goal
implies the forced hypothesis.  For example,

     (defthm not-p-implies-rationalp
       (implies (not (p x (foo x))) (rationalp x))
       :rule-classes nil)

Observe that we make no rules from this formula.  Instead, we merely
:use it in the subgoal where we must establish (rationalp x).

     (thm (p x (foo x))
          :hints (("Goal" :use not-p-implies-rationalp)))

When we said, above, that (p x (foo x)) is first rewritten in an empty
context we were misrepresenting the situation slightly.  When we rewrite
a literal we know what literal we are rewriting and we implicitly assume
it false.  This assumption is "dangerous" in that it can lead us to
simplify our goal to nil and give up -- we have even seen people make
the mistake of assuming the negation of what they wished to prove and
then via a very complicated series of transformations convince
themselves that the formula is false.  Because of this "tail biting" we
make very weak use of the negation of our goal.  But the use we make of
it is sufficient to establish the forced hypothesis above.

A fourth alternative is to weaken your desired theorem so as to make
explicit the required hypotheses, e.g., to prove

     (defthm rationalp-implies-main
       (implies (rationalp x) (p x (foo x)))
       :rule-classes nil)

This of course is unsatisfying because it is not what you originally
intended.  But all is not lost.  You can now prove your main theorem
from this one, letting the implies here provide the necessary case
split.

     (thm (p x (foo x))
          :hints (("Goal" :use rationalp-implies-main)))

FAILURE    how to deal with a proof failure

When ACL2 gives up it does not mean that the submitted conjecture is
invalid, even if the last formula ACL2 printed in its proof attempt is
manifestly false.  Since ACL2 sometimes generalizes the goal being
proved, it is possible it adopted an invalid subgoal as a legitimate
(but doomed) strategy for proving a valid goal.  Nevertheless,
conjectures submitted to ACL2 are often invalid and the proof attempt
often leads the careful reader to the realization that a hypothesis has
been omitted or that some special case has been forgotten.  It is good
practice to ask yourself, when you see a proof attempt fail, whether the
conjecture submitted is actually a theorem.

If you think the conjecture is a theorem, then you must figure out from
ACL2's output what you know that ACL2 doesn't about the functions in the
conjecture and how to impart that knowledge to ACL2 in the form of
rules.  However, see PROOF-TREE for a utility that may be very
helpful in locating parts of the failed proof that are of particular
interest.  See also the book "Computer-Aided Reasoning: An Approach"
(Kaufmann, Manolios, Moore), as well as the discussion of how to read
Nqthm proofs and how to use Nqthm rules in "A Computational Logic
Handbook" by Boyer and Moore (Academic Press, 1988).

If the failure occurred during a forcing round, see
FAILED-FORCING.

FIND-RULES-OF-RUNE    find the rules named rune

     General Form:
     (find-rules-of-rune rune wrld)

This function finds all the rules in wrld with :rune rune.  It returns a
list of rules in their internal form (generally as described by the
corresponding defrec).  Decyphering these rules is difficult since one
cannot always look at a rule object and decide what kind of record it is
without exploiting many system invariants (e.g., that :rewrite runes
only name rewrite-rules).

At the moment this function returns nil if the rune in question is a
:refinement rune, because there is no object representing :refinement
rules.  (:refinement rules cause changes in the 'coarsenings
properties.)  In addition, if the rune is an :equivalence rune, then
congruence rules with that rune will be returned -- because :equivalence
lemmas generate some congruence rules -- but the fact that a certain
function is now known to be an equivalence relation is not represented
by any rule object and so no such rule is returned.  (The fact that the
function is an equivalence relation is encoded entirely in its presence
as a 'coarsening of equal.)

FORCE    identity function used to force a hypothesis

When a hypothesis of a conditional rule has the form (force hyp) it is
logically equivalent to hyp but has a pragmatic effect.  In particular,
when the rule is considered, the needed instance of the hypothesis,
hyp', is assumed and a special case is generated, requiring the system
to prove that hyp' is true in the current context.  The proofs of all
such "forced assumptions" are delayed until the successful completion of
the main goal.  See FORCING-ROUND.

Forcing should only be used on hypotheses that are always expected to be
true, such as the guards of functions.  All the power of the theorem
prover is brought to bear on a forced hypothesis and no backtracking is
possible.  If the :executable-counterpart of the function force is
disabled, then no hypothesis is forced.  See ENABLE-FORCING and
see DISABLE-FORCING.  Forced goals can be attacked immediately
(see IMMEDIATE-FORCE-MODEP) or in a subsequent forcing round
(see FORCING-ROUND).  Also see CASE-SPLIT.

It sometimes happens that a conditional rule is not applied because some
hypothesis, hyp, could not be relieved, even though the required
instance of hyp, hyp', can be shown true in the context.  This happens
when insufficient resources are brought to bear on hyp' at the time we
try to relieve it.  A sometimes desirable alternative behavior is for
the system to assume hyp', apply the rule, and to generate explicitly a
special case to show that hyp' is true in the context.  This is called
"forcing" hyp.  It can be arranged by restating the rule so that the
offending hypothesis, hyp, is embedded in a call of force, as in (force
hyp).  By using the :corollary field of the rule-classes entry, a
hypothesis can be forced without changing the statement of the theorem
from which the rule is derived.

Technically, force is just a function of one argument that returns that
argument.  It is generally enabled and hence evaporates during
simplification.  But its presence among the hypotheses of a conditional
rule causes case splitting to occur if the hypothesis cannot be
conventionally relieved.

Since a forced hypothesis must be provable whenever the rule is
otherwise applicable, forcing should be used only on hypotheses that are
expected always to be true.

A particularly common situation in which some hypotheses should be
forced is in "most general" type-prescription lemmas.  If a single lemma
describes the "expected" type of a function, for all "expected"
arguments, then it is probably a good idea to force the hypotheses of
the lemma.  Thus, every time a term involving the function arises, the
term will be given the expected type and its arguments will be required
to be of the expected type.  In applying this advice it might be wise to
avoid forcing those hypotheses that are in fact just type predicates on
the arguments, since the routine that applies type-prescription lemmas
has fairly thorough knowledge of the types of all terms.

Force can have the additional benefit of causing the ACL2 typing
mechanism to interact with the ACL2 rewriter to establish the hypotheses
of type-prescription rules.  To understand this remark, think of the
ACL2 type reasoning system as a rather primitive rule-based theorem
prover for questions about Common Lisp types, e.g., "does this
expression produce a consp?"  "does this expression produce some kind of
ACL2 number, e.g., an integerp, a rationalp, or a complex-rationalp?"
etc.  It is driven by type-prescription rules.  To relieve the
hypotheses of such rules, the type system recursively invokes itself.
This can be done for any hypothesis, whether it is "type-like" or not,
since any proposition, p, can be phrased as the type-like question "does
p produce an object of type nil?"  However, as you might expect, the
type system is not very good at establishing hypotheses that are not
type-like, unless they happen to be assumed explicitly in the context in
which the question is posed, e.g., "If p produces a consp then does p
produce nil?"  If type reasoning alone is insufficient to prove some
instance of a hypothesis, then the instance will not be proved by the
type system and a type-prescription rule with that hypothesis will be
inapplicable in that case.  But by embedding such hypotheses in force
expressions you can effectively cause the type system to "punt" them to
the rest of the theorem prover.  Of course, as already noted, this
should only be done on hypotheses that are "always true."  In
particular, if rewriting is required to establish some hypothesis of a
type-prescription rule, then the rule will be found inapplicable because
the hypothesis will not be established by type reasoning alone.

The ACL2 rewriter uses the type reasoning system as a subsystem.  It is
therefore possible that the type system will force a hypothesis that the
rewriter could establish.  Before a forced hypothesis is reported out of
the rewriter, we try to establish it by rewriting.

This makes the following surprising behavior possible: A
type-prescription rule fails to apply because some true hypothesis is
not being relieved.  The user changes the rule so as to *force* the
hypothesis.  The system then applies the rule but reports no forcing.
How can this happen?  The type system "punted" the forced hypothesis to
the rewriter, which established it.

Finally, we should mention that the rewriter is never willing to force
when there is an if term present in the goal being simplified.  Since
and terms and or terms are merely abbreviations for if terms, they also
prevent forcing.  Note that if terms are ultimately eliminated using the
ordinary flow of the proof (but see SET-CASE-SPLIT-LIMITATIONS),
allowing force ultimately to function as intended.  Moreover, forcing
can be disabled, as described above; also see DISABLE-FORCING.

FORCING-ROUND    a section of a proof dealing with forced assumptions

If ACL2 "forces" some hypothesis of some rule to be true, it is obliged
later to prove the hypothesis.  See FORCE.  ACL2 delays the
consideration of forced hypotheses until the main goal has been proved.
It then undertakes a new round of proofs in which the main goal is
essentially the conjunction of all hypotheses forced in the preceding
proof.  Call this round of proofs the "Forcing Round."  Additional
hypotheses may be forced by the proofs in the Forcing Round.  The
attempt to prove these hypotheses is delayed until the Forcing Round has
been successfully completed.  Then a new Forcing Round is undertaken to
prove the recently forced hypotheses and this continues until no
hypotheses are forced.  Thus, there is a succession of Forcing Rounds.

The Forcing Rounds are enumerated starting from 1.  The Goals and
Subgoals of a Forcing Round are printed with the round's number
displayed in square brackets.  Thus, "[1]Subgoal 1.3" means that the
goal in question is Subgoal 1.3 of the 1st forcing round.  To supply a
hint for use in the proof of that subgoal, you should use the goal
specifier "[1]Subgoal 1.3".  See GOAL-SPEC.

When a round is successfully completed -- and for these purposes you may
think of the proof of the main goal as being the 0th forcing round --
the system collects all of the assumptions forced by the just-completed
round.  Here, an assumption should be thought of as an implication,
(implies context hyp), where context describes the context in which hyp
was assumed true.  Before undertaking the proofs of these assumptions,
we try to "clean them up" in an effort to reduce the amount of work
required.  This is often possible because the forced assumptions are
generated by the same rule being applied repeatedly in a given context.

For example, suppose the main goal is about some term (pred (xtrans i)
i) and that some rule rewriting pred contains a forced hypothesis that
the first argument is a good-inputp.  Suppose that during the proof of
Subgoal 14 of the main goal, (good-inputp (xtrans i)) is forced in a
context in which i is an integerp and x is a consp.  (Note that x is
irrelevant.)  Suppose finally that during the proof of Subgoal 28,
(good-inputp (xtrans i)) is forced "again," but this time in a context
in which i is a rationalp and x is a symbolp.  Since the forced
hypothesis does not mention x, we deem the contextual information about
x to be irrelevant and discard it from both contexts.  We are then left
with two forced assumptions: (implies (integerp i) (good-inputp (xtrans
i))) from Subgoal 14, and (implies (rationalp i) (good-inputp (xtrans
i))) from Subgoal 28.  Note that if we can prove the assumption required
by Subgoal 28 we can easily get that for Subgoal 14, since the context
of Subgoal 28 is the more general.  Thus, in the next forcing round we
will attempt to prove just

     (implies (rationalp i) (good-inputp (xtrans i)))

and "blame" both Subgoal 14 and Subgoal 28 of the previous round for
causing us to prove this.

By delaying and collecting the forced assumptions until the completion
of the "main goal" we gain two advantages.  First, the user gets
confirmation that the "gist" of the proof is complete and that all that
remains are "technical details."  Second, by delaying the proofs of the
forced assumptions ACL2 can undertake the proof of each assumption only
once, no matter how many times it was forced in the main goal.

In order to indicate which proof steps of the previous round were
responsible for which forced assumptions, we print a sentence explaining
the origins of each newly forced goal.  For example,

     [1]Subgoal 1, below, will focus on
     (GOOD-INPUTP (XTRANS I)),
     which was forced in
      Subgoal 14, above,
       by applying (:REWRITE PRED-CRUNCHER) to
       (PRED (XTRANS I) I),
      and
      Subgoal 28, above,
       by applying (:REWRITE PRED-CRUNCHER) to
       (PRED (XTRANS I) I).

In this entry, "[1]Subgoal 1" is the name of a goal which will be proved
in the next forcing round.  On the next line we display the forced
hypothesis, call it x, which is (good-inputp (xtrans i)) in this
example.  This term will be the conclusion of the new subgoal.  Since
the new subgoal will be printed in its entirety when its proof is
undertaken, we do not here exhibit the context in which x was forced.
The sentence then lists (possibly a succession of) a goal name from the
just-completed round and some step in the proof of that goal that forced
x.  In the example above we see that Subgoals 14 and 28 of the
just-completed proof forced (good-inputp (xtrans i)) by applying
(:rewrite pred-cruncher) to the term (pred (xtrans i) i).

If one were to inspect the theorem prover's description of the proof
steps applied to Subgoals 14 and 28 one would find the word "forced" (or
sometimes "forcibly") occurring in the commentary.  Whenever you see
that word in the output, you know you will get a subsequent forcing
round to deal with the hypotheses forced.  Similarly, if at the
beginning of a forcing round a rune is blamed for causing a force in
some subgoal, inspection of the commentary for that subgoal will reveal
the word "forced" after the rule name blamed.

Most forced hypotheses come from within the prover's simplifier.  When
the simplifier encounters a hypothesis of the form (force hyp) it first
attempts to establish it by rewriting hyp to, say, hyp'.  If the truth
or falsity of hyp' is known, forcing is not required.  Otherwise, the
simplifier actually forces hyp'.  That is, the x mentioned above is
hyp', not hyp, when the forced subgoal was generated by the simplifier.

Once the system has printed out the origins of the newly forced goals,
it proceeds to the next forcing round, where those goals are
individually displayed and attacked.

At the beginning of a forcing round, the enabled structure defaults to
the global enabled structure.  For example, suppose some rune, rune, is
globally enabled.  Suppose in some event you disable the rune at "Goal"
and successfully prove the goal but force "[1]Goal".  Then during the
proof of "[1]Goal", rune is enabled "again."  The right way to think
about this is that the rune is "still" enabled.  That is, it is enabled
globally and each forcing round resumes with the global enabled
structure.

GC$    invoke the garbage collector

This function is provided so that the user can call the garbage
collector of the underlying Lisp from inside the ACL2 loop.
Specifically, a call of gc$ is translated into a call of a function
below on the same arguments.

     Allegro CL:            excl:gc
     GCL                    si::gbc
     CLISP                  ext:gc
     CMU Common Lisp        system::gc
     SBCL                   sb-ext:gc
     Macintosh Common Lisp  ccl::gc

The arguments, if any, are as documented in the underlying Common Lisp.
It is up to the user to pass in the right arguments, although we may do
some rudimentary checks.

This function always returns nil.

GCL    tips on building and using ACL2 based on Gnu Common Lisp

See the installation instructions for basic information about building
ACL2 on top of GCL, including information about where to fetch GCL.
Here, we provide some tips that may be useful.

1. You can place forms to evaluate at start-up into file init.lsp in the
directory where you are starting ACL2 (GCL), or into file acl2-init.lsp
in your home directory.  For example, in order to evaluate both of the
lisp forms mentioned in 2 below, you could put them both into init.lsp
in the current directory or in ~/acl2-init.lsp (either way, without (lp)
or :q):

     (setq si::*optimize-maximum-pages* nil)
     (si::allocate 'cons 75000 t)

2. Suppose you run out of space, for example with an error like this:

        Error: The storage for CONS is exhausted.
          Currently, 59470 pages are allocated.
          Use ALLOCATE to expand the space.

The following suggestion from Camm Maguire will minimize the heap size,
at the cost of more garbage collection time.

     :q   ; exit the ACL2 loop
     (setq si::*optimize-maximum-pages* nil)
     (lp) ; re-enter the ACL2 loop

A second thing to try, suggested by several people, is to preallocate
more pages before the run, e.g.:

     :q   ; exit the ACL2 loop
     (si::allocate 'cons 75000 t)
     (lp) ; re-enter the ACL2 loop

3. Windows users have seen this error:

     cc1.exe: unrecognized option `-fno-zero-initialized-in-bss'

Camm Maguire suggests that a solution may be to evaluate the following
in GCL before building ACL2.

     (in-package 'compiler)
     (let* ((x `-fno-zero-initialized-in-bss')
            (i (search x *cc*)))
             (setq *cc* (concatenate 'string
                                     (subseq *cc* 0 i)
                                     (subseq *cc* (+ i (length x))))))

4. It is possible to profile using ACL2 built on GCL.  See file
save-gprof.lsp in the ACL2 source directory.

GENERALIZED-BOOLEANS    potential soundness issues related to ACL2 predicates

The discussion below outlines a potential source of unsoundness in ACL2.
Although to our knowledge there is no existing Lisp implementation in
which this problem can arise, nevertheless we feel compelled to explain
this situation.

Consider for example the question: What is the value of (equal 3 3)?
According to the ACL2 axioms, it's t.  And as far as we know, based on
considerable testing, the value is t in every Common Lisp
implementation.  However, according the Common Lisp draft proposed ANSI
standard, any non-nil value could result.  Thus for example, (equal 3 3)
is allowed by the standard to be 17.

The Common Lisp standard specifies (or soon will) that a number of
Common Lisp functions that one might expect to return Boolean values
may, in fact, return arbitrary values.  Examples of such functions are
equal, rationalp, and <; a much more complete list is given below.
Indeed, we dare to say that every Common Lisp function that one may
believe returns only Booleans is, nevertheless, not specified by the
standard to have that property, with the exceptions of the functions not
and null.  The standard refers to such arbitrary values as "generalized
Booleans," but in fact this terminology makes no restriction on those
values.  Rather, it merely specifies that they are to be viewed, in an
informal sense, as being either nil or not nil.

This situation is problematic for ACL2, which axiomatizes these
functions to return Booleans.  The problem is that because (for
efficiency and simplicity) ACL2 makes very direct use of compiled Common
Lisp functions to support the execution of its functions, there is in
principle a potential for unsoundness due to these "generalized
Booleans."  For example, ACL2's equal function is defined to be Common
Lisp's equal.  Hence if in Common Lisp the form (equal 3 3) were to
evaluate to 17, then in ACL2 we could prove (using the
:executable-counterpart of equal) (equal (equal 3 3) 17).  However, ACL2
can also prove (equal (equal x x) t), and these two terms together are
contradictory, since they imply (instantiating x in the second term by
3) that (equal 3 3) is both equal to 17 and to t.

To make matters worse, the standard allows (equal 3 3) to evaluate to
*different* non-nil values every time.  That is: equal need not even be
a function!

Fortunately, no existing Lisp implementation takes advantage of the
flexibility to have (most of) its predicates return generalized
Booleans, as far as we know.  We may implement appropriate safeguards in
future releases of ACL2, in analogy to (indeed, probably extending) the
existing safeguards by way of guards (see GUARD).  For now,
we'll sleep a bit better knowing that we have been up-front about this
potential problem.

The following list of functions contains all those that are defined in
Common Lisp to return generalized Booleans but are assumed by ACL2 to
return Booleans.  In addition, the functions acl2-numberp and
complex-rationalp are directly defined in terms of respective Common
Lisp functions numberp and complexp.

     /=
     <
     =
     alpha-char-p
     atom
     char-equal
     char<
     char<=
     char>
     char>=
     characterp
     consp
     digit-char-p
     endp
     eq
     eql
     equal
     evenp
     integerp
     keywordp
     listp
     logbitp
     logtest
     lower-case-p
     minusp
     oddp
     plusp
     rationalp
     standard-char-p
     string-equal
     string<
     string<=
     string>
     string>=
     stringp
     subsetp
     symbolp
     upper-case-p
     zerop

GOAL-SPEC    to indicate where a hint is to be used

     Examples:
     "Goal"
     "goal"
     "Subgoal *1/3""
     "subgoal *1/3""
     "[2]Subgoal *1/3""

When hints are given to the theorem prover, a goal-spec is provided to
specify the goal to which the hints are to be applied.  The hints
provided are carried along innocuously until the named goal arises.
When it arises, the hints are "activated" for that goal and its
descendents.

A legal goal specification may be extracted from the theorem prover's
output.  Certain lines clearly label formulas, as in

     Subgoal *1/3.2'
     (IMPLIES ... ...)

and these lines all give rise to goal specifications.  In general, these
lines all start either with "Goal" or "Subgoal" or else with those words
preceded by a number in square brackets, as in

     [1]Subgoal *1/3.2'
     (IMPLIES ... ...).

A goal specification may be obtained by deleting any surrounding
whitespace from such a line and embedding the text in string quotation
marks.  Thus

     "[1]Subgoal *1/3.2'"

is the goal specifier for the goal above.

As noted, a hint is applied to a goal when the hint's goal specification
matches the name ACL2 assigns to the goal.  The matching algorithm is
case-insensitive.  Thus, alternative goal specifications for the goal
above are "[1]subgoal *1/3.2'" and "[1]SUBGOAL *1/3.2'".  The matching
algorithm does not tolerate non-case discrepancies.  Thus,
"[1]Subgoal*1/3.2'" and " [1]Subgoal *1/3.2'" are unacceptable.

Sometimes a formula is given two names, e.g.,

     Subgoal *1/14.2'
     (IMPLIES ...
              ...)
     Name the formula above *1.1.

It is the first name (the one that starts with "Goal" or "Subgoal") and
not the second which constitutes a legal goal-spec.  Roughly speaking,
when the system prints the line containing the goal specification, it
activates any hints that are attached to that goal-spec.  Consider the
example above.  Suppose Subgoal *1/14.2' could be proved by using a
certain lemma instance.  Then the appropriate entry in the hints would
be:

     ("Subgoal *1/14.2'" :use ...)

This might surprise you because the system appears to do nothing to
*1/14.2' besides push it for a subsequent induction.  But actually
between the time the system printed the goal-spec line and the time it
decides to push the goal, you can think of the system as trying
everything it has.  So a use hint activated when Subgoal *1/14.2' arises
is just what you want.

But what if you want to give an :induct hint?  By the time induction is
tried, the formula has been given the name *1.1.  Well, this is one you
just have to remember:

     ("Subgoal *1/14.2'" :induct ...).

When the above hint is activated the :induct directive short-circuits
the rest of the processing and sends immediately the formula into the
pool of goals to prove by induction.  The induct hint is attached to the
formula in the pool and when the time comes to turn our attention to
that goal, the induct advice is followed.

GUARD    restricting the domain of a function

The ACL2 system provides a mechanism for restricting a function
definition to a particular domain.  Although such restrictions, which
are called "guards," are actually ignored by the ACL2 *logic*, they can
be useful as a specification device or as a means of causing the
execution of definitions directly in Common Lisp.  To make such a
restriction, use the :guard xarg to defun.  See XARGS for a
discussion of how to use :guard.  The general issue of guards and guard
verification is discussed in the topics listed below.

Related topics other than immediate subtopics:

To begin further discussion of guards, see GUARD-INTRODUCTION.
That section directs the reader to further sections for more details.
To see just a summary of some commands related to guards, see
GUARD-QUICK-REFERENCE.

GUARD-EVALUATION-EXAMPLES-LOG    log showing combinations of defun-modes and guard-checking

See GUARD-EVALUATION-EXAMPLES-SCRIPT for a script that shows the
interaction of defun-modes with the value set by set-guard-checking.
Here, we present a log resulting from running this script (using ACL2
Version 3.0, built on Allegro Common Lisp).

See SET-GUARD-CHECKING for discussion of the interaction between
defun-modes and guard-checking that is illustrated by this script.  Also
see GUARD-EVALUATION-TABLE for a succinct table, with associated
discussion, that covers in detail the interactions illustrated here.

     ACL2 !>(defun fact (x)
              (declare (xargs :guard (integerp x)
                              :mode :program))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     Summary
     Form:  ( DEFUN FACT ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT
     ACL2 !>(trace$ fact)
     NIL
     ACL2 !>:set-guard-checking t

     Guard-checking-on already has value T.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the :program function symbol
     FACT, which is (INTEGERP X), is violated by the arguments in the call
     (FACT T).  See :DOC wet for how you might be able to get an error backtrace.
     See :DOC set-guard-checking for information about suppressing this
     check with (set-guard-checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the :program function symbol
     FACT, which is (INTEGERP X), is violated by the arguments in the call
     (FACT T).  See :DOC wet for how you might be able to get an error backtrace.
     See :DOC set-guard-checking for information about suppressing this
     check with (set-guard-checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards.  To avoid guard
     checking entirely, :SET-GUARD-CHECKING :NONE.  See :DOC set-guard-
     checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:u

               0:x(EXIT-BOOT-STRAP-MODE)
     ACL2 >(defun fact (x)
              (declare (xargs :guard t
                              :mode :program))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     Summary
     Form:  ( DEFUN FACT ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT
     ACL2 >(trace$ fact)
     NIL
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards.  To avoid guard
     checking entirely, :SET-GUARD-CHECKING :NONE.  See :DOC set-guard-
     checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:u

               0:x(EXIT-BOOT-STRAP-MODE)
     ACL2 >(defun fact (x)
              (declare (xargs :guard (integerp x)
                              :verify-guards nil
                              :mode :logic))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     For the admission of FACT we will use the relation O< (which is known
     to be well-founded on the domain recognized by O-P) and the measure
     (ACL2-COUNT X).  The non-trivial part of the measure conjecture is

     Goal
     (IMPLIES (POSP X)
              (O< (ACL2-COUNT (+ -1 X))
                  (ACL2-COUNT X))).

     By the simple :definition POSP we reduce the conjecture to

     Goal'
     (IMPLIES (AND (INTEGERP X) (< 0 X))
              (O< (ACL2-COUNT (+ -1 X))
                  (ACL2-COUNT X))).

     But we reduce the conjecture to T, by case analysis.

     Q.E.D.

     That completes the proof of the measure theorem for FACT.  Thus, we
     admit this function under the principle of definition. We observe that
     the type of FACT is described by the theorem
     (AND (INTEGERP (FACT X)) (< 0 (FACT X))).  We used the :compound-recognizer
     rule POSP-COMPOUND-RECOGNIZER and primitive type reasoning.

     Summary
     Form:  ( DEFUN FACT ...)
     Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
             (:DEFINITION NOT)
             (:DEFINITION POSP)
             (:FAKE-RUNE-FOR-TYPE-SET NIL))
     Warnings:  None
     Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
      FACT
     ACL2 >(trace$ fact)
     NIL
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)

     ACL2 Warning [Guards] in TOP-LEVEL:  Guard-checking will be inhibited
     on recursive calls of the executable counterpart (i.e., in the ACL2
     logic) of FACT.  To check guards on all recursive calls:
       (set-guard-checking :all)
     To leave behavior unchanged except for inhibiting this message:
       (set-guard-checking :nowarn)

     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
     is (INTEGERP X), is violated by the arguments in the call (FACT T).
     See :DOC wet for how you might be able to get an error backtrace.
     See :DOC set-guard-checking for information about suppressing this
     check with (set-guard-checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
     is (INTEGERP X), is violated by the arguments in the call (FACT T).
     See :DOC wet for how you might be able to get an error backtrace.
     See :DOC set-guard-checking for information about suppressing this
     check with (set-guard-checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards.  To avoid guard
     checking entirely, :SET-GUARD-CHECKING :NONE.  See :DOC set-guard-
     checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >(verify-guards fact)

     Computing the guard conjecture for FACT....

     The guard conjecture for FACT is trivial to prove, given the :compound-
     recognizer rule POSP-COMPOUND-RECOGNIZER, primitive type reasoning
     and the :type-prescription rule FACT.  FACT is compliant with Common
     Lisp.

     Summary
     Form:  ( VERIFY-GUARDS FACT)
     Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
             (:FAKE-RUNE-FOR-TYPE-SET NIL)
             (:TYPE-PRESCRIPTION FACT))
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT
     ACL2 >(trace$ fact)
     NIL
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
     is (INTEGERP X), is violated by the arguments in the call (FACT T).
     See :DOC wet for how you might be able to get an error backtrace.
     See :DOC set-guard-checking for information about suppressing this
     check with (set-guard-checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
     is (INTEGERP X), is violated by the arguments in the call (FACT T).
     See :DOC wet for how you might be able to get an error backtrace.
     See :DOC set-guard-checking for information about suppressing this
     check with (set-guard-checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards.  To avoid guard
     checking entirely, :SET-GUARD-CHECKING :NONE.  See :DOC set-guard-
     checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:u
      L        1:x(DEFUN FACT (X) ...)
     ACL2 >:u
               0:x(EXIT-BOOT-STRAP-MODE)
     ACL2 >(defun fact (x)
              (declare (xargs :guard (integerp x)
                              :mode :logic))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     For the admission of FACT we will use the relation O< (which is known
     to be well-founded on the domain recognized by O-P) and the measure
     (ACL2-COUNT X).  The non-trivial part of the measure conjecture is

     Goal
     (IMPLIES (POSP X)
              (O< (ACL2-COUNT (+ -1 X))
                  (ACL2-COUNT X))).

     By the simple :definition POSP we reduce the conjecture to

     Goal'
     (IMPLIES (AND (INTEGERP X) (< 0 X))
              (O< (ACL2-COUNT (+ -1 X))
                  (ACL2-COUNT X))).

     But we reduce the conjecture to T, by case analysis.

     Q.E.D.

     That completes the proof of the measure theorem for FACT.  Thus, we
     admit this function under the principle of definition. We observe that
     the type of FACT is described by the theorem
     (AND (INTEGERP (FACT X)) (< 0 (FACT X))).  We used the :compound-recognizer
     rule POSP-COMPOUND-RECOGNIZER and primitive type reasoning.

     Computing the guard conjecture for FACT....

     The guard conjecture for FACT is trivial to prove, given the :compound-
     recognizer rule POSP-COMPOUND-RECOGNIZER, primitive type reasoning
     and the :type-prescription rule FACT.  FACT is compliant with Common
     Lisp.

     Summary
     Form:  ( DEFUN FACT ...)
     Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
             (:DEFINITION NOT)
             (:DEFINITION POSP)
             (:FAKE-RUNE-FOR-TYPE-SET NIL)
             (:TYPE-PRESCRIPTION FACT))
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT
     ACL2 >(trace$ fact)
     NIL
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
     is (INTEGERP X), is violated by the arguments in the call (FACT T).
     See :DOC wet for how you might be able to get an error backtrace.
     See :DOC set-guard-checking for information about suppressing this
     check with (set-guard-checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
     is (INTEGERP X), is violated by the arguments in the call (FACT T).
     See :DOC wet for how you might be able to get an error backtrace.
     See :DOC set-guard-checking for information about suppressing this
     check with (set-guard-checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards.  To avoid guard
     checking entirely, :SET-GUARD-CHECKING :NONE.  See :DOC set-guard-
     checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:u
               0:x(EXIT-BOOT-STRAP-MODE)
     ACL2 >(defun fact (x)
              (declare (xargs :guard t
                              :verify-guards nil
                              :mode :logic))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     For the admission of FACT we will use the relation O< (which is known
     to be well-founded on the domain recognized by O-P) and the measure
     (ACL2-COUNT X).  The non-trivial part of the measure conjecture is

     Goal
     (IMPLIES (POSP X)
              (O< (ACL2-COUNT (+ -1 X))
                  (ACL2-COUNT X))).

     By the simple :definition POSP we reduce the conjecture to

     Goal'
     (IMPLIES (AND (INTEGERP X) (< 0 X))
              (O< (ACL2-COUNT (+ -1 X))
                  (ACL2-COUNT X))).

     But we reduce the conjecture to T, by case analysis.

     Q.E.D.

     That completes the proof of the measure theorem for FACT.  Thus, we
     admit this function under the principle of definition. We observe that
     the type of FACT is described by the theorem
     (AND (INTEGERP (FACT X)) (< 0 (FACT X))).  We used the :compound-recognizer
     rule POSP-COMPOUND-RECOGNIZER and primitive type reasoning.

     Summary
     Form:  ( DEFUN FACT ...)
     Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
             (:DEFINITION NOT)
             (:DEFINITION POSP)
             (:FAKE-RUNE-FOR-TYPE-SET NIL))
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT
     ACL2 >(trace$ fact)
     NIL
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards.  To avoid guard
     checking entirely, :SET-GUARD-CHECKING :NONE.  See :DOC set-guard-
     checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >(verify-guards fact)

     Computing the guard conjecture for FACT....

     The guard conjecture for FACT is trivial to prove, given the :compound-
     recognizer rule POSP-COMPOUND-RECOGNIZER and the :type-prescription
     rule FACT.  FACT is compliant with Common Lisp.

     Summary
     Form:  ( VERIFY-GUARDS FACT)
     Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
             (:TYPE-PRESCRIPTION FACT))
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT
     ACL2 >(trace$ fact)
     NIL
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards.  To avoid guard
     checking entirely, :SET-GUARD-CHECKING :NONE.  See :DOC set-guard-
     checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >