This is documentation for ACL2 Version 3.4
Copyright (C) 2008  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.

SUBVERSIVE-RECURSIONS    why we restrict encapsulated recursive functions

Subtleties arise when one of the "constrained" functions, f, introduced
in the signature of an encapsulate event, is involved in the
termination argument for a non-local recursively defined function, g,
in that encapsulate.  During the processing of the encapsulated events,
f is locally defined to be some witness function, f'.  Properties of f'
are explicitly proved and exported from the encapsulate as the
constraints on the undefined function f.  But if f is used in a
recursive g defined within the encapsulate, then the termination proof
for g may use properties of f' - the witness - that are not explicitly
set forth in the constraints stated for f.

Such recursive g are said be "subversive" because if naively treated
they give rise to unsound induction schemes or (via functional
instantiation) recurrence equations that are impossible to satisfy.  We
illustrate what could go wrong below.

Subversive recursions are not banned outright.  Instead, they are
treated as part of the constraint.  That is, in the case above, the
definitional equation for g becomes one of the constraints on f.  This
is generally a severe restriction on future functional instantiations
of f.  In addition, ACL2 removes from its knowledge of g any
suggestions about legal inductions to "unwind" its recursion.

What should you do?  Often, the simplest response is to move the
offending recursive definition, e.g., g, out of the encapsulate.  That
is, introduce f by constraint and then define g as an "independent"
event.  You may need to constrain "additional" properties of f in order
to admit g, e.g., constrain it to reduce some ordinal measure.
However, by separating the introduction of f from the admission of g
you will clearly identify the necessary constraints on f, functional
instantiations of f will be simpler, and g will be a useful function
which suggests inductions to the theorem prover.

Note that the functions introduced in the signature should not even
occur ancestrally in the termination proofs for non-local recursive
functions in the encapsulate.  That is, the constrained functions of an
encapsulate should not be reachable in the dependency graph of the
functions used in the termination arguments of recursive functions in
encapsulate.  If they are reachable, their definitions become part of
the constraints.

The following event illustrates the problem posed by subversive
recursions.

     (encapsulate (((f *) => *))
       (local (defun f (x) (cdr x)))
       (defun g (x)
         (if (consp x) (not (g (f x))) t)))

Suppose, contrary to how ACL2 works, that the encapsulate above were to
introduce no constraints on f on the bogus grounds that the only use of
f in the encapsulate is in an admissible function.  We discuss the
plausibility of this bogus argument in a moment.

Then it would be possible to prove the theorem:

     (defthm f-not-identity
       (not (equal (f '(a . b)) '(a . b)))
       :rule-classes nil
       :hints (("Goal" :use (:instance g (x '(a . b))))))

simply by observing that if (f '(a . b)) were '(a . b), then (g '(a .
b)) would be (not (g '(a . b))), which is impossible.

But then we could functionally instantiate f-not-identity, replacing f
by the identity function, to prove nil!  This is bad.

     (defthm bad
       nil
       :rule-classes nil
       :hints
       (("Goal" :use (:functional-instance f-not-identity (f identity)))))

This sequence of events was legal in versions of ACL2 prior to Version
1.5.  When we realized the problem we took steps to make it illegal.
However, our steps were insufficient and it was possible to sneak in a
subversive function (via mutual recursion) as late as Version  2.3.

We now turn to the plausibility of the bogus argument above.  Why might
one even be tempted to think that the definition of g above poses no
constraint on f?  Here is a very similar encapsulate.

     (encapsulate (((f *) => *))
       (local (defun f (x) (cdr x)))
       (defun map (x)
         (if (consp x)
             (cons (f x) (map (cdr x)))
           nil)))

Here map plays the role of g above.  Like g, map calls the constrained
function f.  But map truly does not constrain f.  In particular, the
definition of map could be moved "out" of the encapsulate so that map
is introduced afterwards.  The difference between map and g is that the
constrained function plays no role in the termination argument for the
one but does for the other.

As a "user-friendly" gesture, ACL2 implicitly moves map-like functions
out of encapsulations; logically speaking, they are introduced after
the encapsulation.  This simplifies the constraint.  This is done only
for "top-level" encapsulations.  When an encapsulate containing a
non-empty signature list is embedded in another encapsulate with a
non-empty signature list, no attempt is made to move map-like functions
out.  The user is advised, via the "infected" warning, to phrase the
encapsulation in the simplest way possible.

The lingering bug between Versions 1.5 and 2.3 mentioned above was due
to our failure to detect the g-like nature of some functions when they
were defined in mutually recursively cliques with other functions.  The
singly recursive case was recognized.  The bug arose because our
detection "algorithm" was based on the "suggested inductions" left
behind by successful definitions.  We failed to recall that
mutually-recursive definitions do not, as of this writing, make any
suggestions about inductions and so did not leave any traces of their
subversive natures.

SYNTAX    the syntax of ACL2 is that of Common Lisp

For the details of ACL2 syntax, see CLTL.  For examples of ACL2 syntax,
use :pe to print some of the ACL2 system code.  For example:

     :pe assoc-equal
     :pe dumb-occur
     :pe var-fn-count
     :pe add-linear-variable-to-alist

There is no comprehensive description of the ACL2 syntax yet, except
that found in CLTL.  Also see TERM.

SYNTAXP    attach a heuristic filter on a :rewrite, :meta, or :linear rule

     Example:
     Consider the :REWRITE rule created from

     (IMPLIES (SYNTAXP (NOT (AND (CONSP X)
                                 (EQ (CAR X) 'NORM))))
              (EQUAL (LXD X)
                     (LXD (NORM X)))).

The syntaxp hypothesis in this rule will allow the rule to be applied
to (lxd (trn a b)) but will not allow it to be applied to (lxd (norm
a)).

     General Form:
     (SYNTAXP test)

Syntaxp always returns t and so may be added as a vacuous hypothesis.
However, when relieving the hypothesis, the test "inside" the syntaxp
form is actually treated as a meta-level proposition about the proposed
instantiation of the rule's variables and that proposition must
evaluate to true (non-nil) to "establish" the syntaxp hypothesis.

Note that the test of a syntaxp hypothesis does not, in general, deal
with the meaning or semantics or values of the terms, but rather with
their syntactic forms.  In the example above, the syntaxp hypothesis
allows the rule to be applied to every target of the form (lxd u),
provided u is not of the form (norm v).  Observe that without this
syntactic restriction the rule above could loop producing a sequence of
increasingly complex targets (lxd a), (lxd (norm a)), (lxd (norm (norm
a))), etc.  An intuitive reading of the rule might be "norm the
argument of lxd unless it has already been normed."

Note also that a syntaxp hypothesis deals with the syntactic form used
internally by ACL2, rather than that seen by the user.  In some cases
these are the same, but there can be subtle differences with which the
writer of a syntaxp hypothesis must be aware.  You can use :trans to
display this internal representation.

There are two types of syntaxp hypotheses.  The simpler type of syntaxp
hypothesis may be used as the nth hypothesis in a :rewrite or :linear
rule whose :corollary is (implies (and hyp1 ... hypn ... hypk) (equiv
lhs rhs)) provided test is a term, test contains at least one variable,
and every variable occuring freely in test occurs freely in lhs or in
some hypi, i<n.  In addition, test must not use any stobjs.  The case
of :meta rules is similar to the above, except that it applies to the
result of applying the hypothesis metafunction.  (Later below we will
describe the second type, an _extended_ syntaxp hypothesis, which may
use state.)

We illustrate the use of simple syntaxp hypotheses by slightly
elaborating the example given above.  Consider a :rewrite rule whose
:corollary is:

     (IMPLIES (AND (RATIONALP X)
                   (SYNTAXP (NOT (AND (CONSP X)
                                      (EQ (CAR X) 'NORM)))))
              (EQUAL (LXD X)
                     (LXD (NORM X))))

How is this rule applied to (lxd (trn a b))?  First, we form a
substitution that instantiates the left-hand side of the conclusion of
the rule so that it is identical to the target term.  In the present
case, the substitution replaces x with (trn a b).

     (LXD X) ==> (LXD (trn a b)).

Then we backchain to establish the hypotheses, in order.  Ordinarily
this means that we instantiate each hypothesis with our substitution and
then attempt to rewrite the resulting instance to true.  Thus, in order
to relieve the first hypothesis above, we rewrite

     (RATIONALP (trn a b)).

If this rewrites to true, we continue.

Of course, most users are aware of some exceptions to this general
description of the way we relieve hypotheses.  For example, if a
hypothesis contains a "free-variable" -- one not bound by the current
substitution -- we attempt to extend the substitution by searching for
an instance of the hypothesis among known truths.  See
FREE-VARIABLES.  Forced hypotheses are another exception to the
general rule of how hypotheses are relieved.

Hypotheses marked with syntaxp, as in (syntaxp test), are also
exceptions.  We instantiate such a hypothesis; but instead of rewriting
the instantiated instance, we evaluate the instantiated test.  More
precisely, we evaluate test in an environment in which its variable
symbols are bound to the quotations of the terms to which those
variables are bound in the instantiating substitution.  So in the case
in point, we (in essence) evaluate

     (NOT (AND (CONSP '(trn a b)) (EQ (CAR '(trn a b)) 'NORM))).

This clearly evaluates to t.  When a syntaxp test evaluates to true, we
consider the syntaxp hypothesis to have been established; this is sound
because logically (syntaxp test) is t regardless of test.  If the test
evaluates to nil (or fails to evaluate because of guard violations) we
act as though we cannot establish the hypothesis and abandon the
attempt to apply the rule; it is always sound to give up.

The acute reader will have noticed something odd about the form

     (NOT (AND (CONSP '(trn a b)) (EQ (CAR '(trn a b)) 'NORM))).

When relieving the first hypothesis, (RATIONALP X), we substituted (trn
a b) for X; but when relieving the second hypothesis, (SYNTAXP (NOT
(AND (CONSP X) (EQ (CAR X) 'NORM)))), we substituted the quotation of
(trn a b) for X.  Why the difference?  Remember that in the first
hypothesis we are talking about the value of (trn a b) -- is it
rational -- while in the second one we are talking about its syntactic
form.  Remember also that Lisp, and hence ACL2, evaluates the arguments
to a function before applying the function to the resulting values.
Thus, we are asking "Is the list (trn a b) a consp and if so, is its
car the symbol NORM?"  The quotes on both (trn a b) and NORM are
therefore necessary.  One can verify this by defining trn to be, say
cons, and then evaluating forms such as

     (AND (CONSP '(trn a b)) (EQ (CAR '(trn a b)) 'NORM))
     (AND (CONSP (trn a b)) (EQ (CAR (trn a b)) NORM))
     (AND (CONSP (trn 'a 'b)) (EQ (CAR (trn 'a 'b)) NORM))
     (AND (CONSP '(trn a b)) (EQ '(CAR (trn a b)) ''NORM))

at the top-level ACL2 prompt.

See SYNTAXP-EXAMPLES for more examples of the use of syntaxp.

An extended syntaxp hypothesis is similar to the simple type described
above, but it uses two additional variables, mfc and state, which must
not be bound by the left hand side or an earlier hypothesis of the
rule.  They must be the last two variables mentioned by form; first
mfc, then state.  These two variables give access to the functions
mfc-xxx; see EXTENDED-METAFUNCTIONS.  As described there, mfc
is bound to the so-called metafunction-context and state to ACL2's
state.  See SYNTAXP-EXAMPLES for an example of the use of these
extended syntaxp hypotheses.

SYNTAXP-EXAMPLES    examples pertaining to syntaxp hypotheses

See SYNTAXP for a basic discussion of the use of syntaxp to
control rewriting.

A common syntactic restriction is

     (SYNTAXP (AND (CONSP X) (EQ (CAR X) 'QUOTE)))

or, equivalently,

     (SYNTAXP (QUOTEP X)).

A rule with such a hypothesis can be applied only if x is bound to a
specific constant.  Thus, if x is 23 (which is actually represented
internally as (quote 23)), the test evaluates to t; but if x prints as
(+ 11 12) then the test evaluates to nil (because (car x) is the symbol
binary-+).  We see the use of this restriction in the rule

     (implies (and (syntaxp (quotep c))
                   (syntaxp (quotep d)))
              (equal (+ c d x)
                     (+ (+ c d) x))).

If c and d are constants, then the executable-counterpart of binary-+
will evaluate the sum of c and d.  For instance, under the influence of
this rule

     (+ 11 12 foo)

rewrites to

     (+ (+ 11 12) foo)

which in turn rewrites to (+ 23 foo).  Without the syntactic
restriction, this rule would loop with the built-in rules
ASSOCIATIVITY-OF-+ or COMMUTATIVITY-OF-+.

We here recommend that the reader try the affects of entering
expressions such as the following at the top level ACL2 prompt.

     (+ 11 23)
     (+ '11 23)
     (+ '11 '23)
     (+ ''11 ''23)
     :trans (+ 11 23)
     :trans (+ '11 23)
     :trans (+ ''11 23)
     :trans (+ c d x)
     :trans (+ (+ c d) x)

We also recommend that the reader verify our claim above about looping
by trying the affect of each of the following rules individually.

     (defthm good
        (implies (and (syntaxp (quotep c))
                      (syntaxp (quotep d)))
                 (equal (+ c d x)
                        (+ (+ c d) x))))

     (defthm bad
        (implies (and (acl2-numberp c)
                      (acl2-numberp d))
                 (equal (+ c d x)
                        (+ (+ c d) x))))

on (the false) theorems:

     (thm
       (equal (+ 11 12 x) y))

     (thm
       (implies (and (acl2-numberp c)
                     (acl2-numberp d)
                     (acl2-numberp x))
                (equal (+ c d x) y))).

One can use :brr, perhaps in conjunction with cw-gstack, to investigate
any looping.

Here is a simple example showing the value of rule good above.  Without
good, the thm form below fails.

     (defstub foo (x) t)

     (thm (equal (foo (+ 3 4 x)) (foo (+ 7 x))))

The next three examples further explore the use of quote in syntaxp
hypotheses.

We continue the examples of syntaxp hypotheses with a rule from
books/finite-set-theory/set-theory.lisp.  We will not discuss here the
meaning of this rule, but it is necessary to point out that
(ur-elementp nil) is true in this book.

     (defthm scons-nil
       (implies (and (syntaxp (not (equal a ''nil)))
                     (ur-elementp a))
                (= (scons e a)
                   (scons e nil)))).

Here also, syntaxp is used to prevent looping.  Without the
restriction, (scons e nil) would be rewritten to itself since
(ur-elementp nil) is true.
Question: Why the use of two quotes in "nil?
Hints: Nil is a constant just as 23 is.  Try :trans (cons a nil),
:trans (cons 'a 'nil), and :trans (cons "a "nil).  Also, don't forget
that the arguments to a function are evaluated before the function is
applied.

The next two rules move negative constants to the other side of an
inequality.

     (defthm |(< (+ (- c) x) y)|
       (implies (and (syntaxp (quotep c))
                     (syntaxp (< (cadr c) 0))
                     (acl2-numberp y))
                (equal (< (+ c x) y)
                       (< (fix x) (+ (- c) y)))))

     (defthm |(< y (+ (- c) x))|
       (implies (and (syntaxp (quotep c))
                     (syntaxp (< (cadr c) 0))
                     (acl2-numberp y))
                (equal (< y (+ c x))
                       (< (+ (- c) y) (fix x)))))

Questions: What would happen if (< (cadr c) '0) were used?  What about
(< (cadr c) "0)?

One can also use syntaxp to restrict the application of a rule to a
particular set of variable bindings as in the following taken from
books/ihs/quotient-remainder-lemmas.lisp.

     (encapsulate ()

       (local
        (defthm floor-+-crock
          (implies
           (and (real/rationalp x)
                (real/rationalp y)
                (real/rationalp z)
                (syntaxp (and (eq x 'x) (eq y 'y) (eq z 'z))))
           (equal (floor (+ x y) z)
                  (floor (+ (+ (mod x z) (mod y z))
                            (* (+ (floor x z) (floor y z)) z)) z)))))

       (defthm floor-+
         (implies
          (and (force (real/rationalp x))
               (force (real/rationalp y))
               (force (real/rationalp z))
               (force (not (equal z 0))))
          (equal (floor (+ x y) z)
                 (+ (floor (+ (mod x z) (mod y z)) z)
                    (+ (floor x z) (floor y z))))))

       )

We recommend the use of :brr to investigate the use of floor-+-crock.

Another useful restriction is defined by

     (defun rewriting-goal-literal (x mfc state)

       ;; Are we rewriting a top-level goal literal, rather than rewriting
       ;; to establish a hypothesis from a rewrite (or other) rule?

       (declare (ignore x state))
       (null (access metafunction-context mfc :ancestors))).

We use this restriction in the rule

     (defthm |(< (* x y) 0)|
         (implies (and (syntaxp (rewriting-goal-literal x mfc state))
                       (rationalp x)
                       (rationalp y))
                  (equal (< (* x y) 0)
                         (cond ((equal x 0)
                                nil)
                               ((equal y 0)
                                nil)
                               ((< x 0)
                                (< 0 y))
                               ((< 0 x)
                                (< y 0))))))

which has been found to be useful, but which also leads to excessive
thrashing in the linear arithmetic package if used indiscriminately.

See EXTENDED-METAFUNCTIONS for information on the use of mfc
and metafunction-context.

TERM    the three senses of well-formed ACL2 expressions or formulas

     Examples of Terms:
     (cond ((caar x) (cons t x)) (t 0))   ; an untranslated term

     (if (car (car x)) (cons 't x) '0)    ; a translated term

     (car (cons x y) 'nil v)              ; a pseudo-term

In traditional first-order predicate calculus a "term" is a syntactic
entity denoting some object in the universe of individuals.  Often, for
example, the syntactic characterization of a term is that it is either
a variable symbol or the application of a function symbol to the
appropriate number of argument terms.  Traditionally, "atomic formulas"
are built from terms with predicate symbols such as "equal" and
"member;" "formulas" are then built from atomic formulas with
propositional "operators" like "not," "and," and "implies." Theorems
are formulas.  Theorems are "valid" in the sense that the value of a
theorem is true, in any model of the axioms and under all possible
assignments of individuals to variables.

However, in ACL2, terms are used in place of both atomic formulas and
formulas.  ACL2 does not have predicate symbols or propositional
operators as distinguished syntactic entities.  The ACL2 universe of
individuals includes a "true" object (denoted by t) and a "false"
object (denoted by nil), predicates and propositional operators are
functions that return these objects.  Theorems in ACL2 are terms and
the "validity" of a term means that, under no assignment to the
variables does the term evaluate to nil.

We use the word "term" in ACL2 in three distinct senses.  We will speak
of "translated" terms, "untranslated" terms, and "pseudo-" terms.

_Translated Terms:  The Strict Sense and Internal Form_

In its most strict sense, a "term" is either a legal variable symbol, a
quoted constant, or the application of an n-ary function symbol or
closed lambda expression to a true list of n terms.

The legal variable symbols are symbols other than t or nil which are
not in the keyword package, do not start with ampersand, do not start
and end with asterisks, and if in the main Lisp package, do not violate
an appropriate restriction (see NAME).

Quoted constants are expressions of the form (quote x), where x is any
ACL2 object.  Such expressions may also be written 'x.

Closed lambda expressions are expressions of the form (lambda (v1 ...
vn) body) where the vi are distinct legal variable symbols, body is a
term, and the only free variables in body are among the vi.

The function termp, which takes two arguments, an alleged term x and a
logical world w (see WORLD), recognizes terms of a given
extension of the logic.  Termp is defined in :program mode.  Its
definition may be inspected with :pe termp for a complete specification
of what we mean by "term" in the most strict sense.  Most ACL2
term-processing functions deal with terms in this strict sense and use
termp as a guard.  That is, the "internal form" of a term satisfies
termp, the strict sense of the word "term."

_Untranslated Terms:  What the User Types_

While terms in the strict sense are easy to explore (because their
structure is so regular and simple) they can be cumbersome to type.
Thus, ACL2 supports a more sugary syntax that includes uses of macros
and constant symbols.  Very roughly speaking, macros are functions that
produce terms as their results.  Constants are symbols that are
associated with quoted objects.  Terms in this sugary syntax are
"translated" to terms in the strict sense; the sugary syntax is more
often called "untranslated."  Roughly speaking, translation just
implements macroexpansion, the replacement of constant symbols by their
quoted values, and the checking of all the rules governing the strict
sense of "term."

More precisely, macro symbols are as described in the documentation for
defmacro.  A macro, mac, can be thought of as a function, mac-fn, from
ACL2 objects to an ACL2 object to be treated as an untranslated term.
For example, caar is defined as a macro symbol; the associated macro
function maps the object x into the object (car (car x)).  A macro form
is a "call" of a macro symbol, i.e., a list whose car is the macro
symbol and whose cdr is an arbitrary true list of objects, used as a
term.  Macroexpansion is the process of replacing in an untranslated
term every occurrence of a macro form by the result of applying the
macro function to the appropriate arguments.  The "appropriate"
arguments are determined by the exact form of the definition of the
macro; macros support positional, keyword, optional and other kinds of
arguments.  See DEFMACRO.

In addition to macroexpansion and constant symbol dereferencing,
translation implements the mapping of let and let* forms into
applications of lambda expressions and closes lambda expressions
containing free variables.  Thus, the translation of

     (let ((x (1+ i))) (cons x k))

can be seen as a two-step process that first produces

     ((lambda (x) (cons x k)) (1+ i))

and then

     ((lambda (x k) (cons x k)) (1+ i) k) .

Observe that the body of the let and of the first lambda expression
contains a free k which is finally bound and passed into the second
lambda expression.

Translation also maps flet forms into applications of lambda
expressions.  See FLET.

When we say, of an event-level function such as defun or defthm, that
some argument "must be a term" we mean an untranslated term.  The event
functions translate their term-like arguments.

To better understand the mapping between untranslated terms and
translated terms it is convenient to use the keyword command :trans to
see examples of translations.  See TRANS and also see
TRANS1.

Finally, we note that the theorem prover prints terms in untranslated
form.  But there can be more than one correct untranslated term
corresponding to a given translated term.  For example, the translated
term (if x y 'nil) can be untranslated as (if x y nil) and can also be
untranslated as (and x y).  The theorem prover attempts to print an
untranslated term that is as helpful to the user as possible.  In
particular, consider a term of the form (nth k st) where st is a
single-threaded object (see STOBJ) and the kth accessor of st
is, say, kn.  The theorem prover typically would expand (kn st) to (nth
k st).  If k is large then it could be difficult for the user to make
sense out of a proof transcript that mentions the expanded term.
Fortunately, the untranslation of (nth k st) would be (nth *kn* st);
here *kn* would be a constant (see DEFCONST) added by the
defstobj event introducing st, defined to have value k.  The user can
extend this user-friendly style of printing applications of nth to
stobjs; see ADD-NTH-ALIAS.  These remarks about printing
applications of function nth extend naturally to function update-nth.
Moreover, the prover will attempt to treat terms as stobjs for the
above purpose when appropriate.  For example, if function foo has
signature ((foo * st) => (mv * * * st)), where st is introduced with
(defstobj st f0 f1), then the term (nth '1 (mv-nth '3 (foo x st0)))
will be printed as (nth *f1* (mv-nth 3 (foo x st0))).

_Pseudo-Terms:  A Common Guard for Metafunctions_

Because termp is defined in :program mode, it cannot be used
effectively in conjectures to be proved.  Furthermore, from the
perspective of merely guarding a term processing function, termp often
checks more than is required.  Finally, because termp requires the
logical world as one of its arguments it is impossible to use termp as
a guard in places where the logical world is not itself one of the
arguments.

For these reasons we support the idea of "pseudo-terms."  A pseudo-term
is either a symbol (but not necessarily one having the syntax of a
legal variable symbol), a true list beginning with quote (but not
necessarily well-formed), or the "application of" a symbol or pseudo
lambda expression to a true list of pseudo-terms.  A pseudo lambda
expression is an expression of the form (lambda (v1 ... vn) body) where
the vi are all symbols and body is a pseudo-term.

Pseudo-terms are recognized by the unary function pseudo-termp.  If
(termp x w) is true, then (pseudo-termp x) is true.  However, if x
fails to be a (strict) term it may nevertheless still be a pseudo-term.
For example, (car a b) is not a term, because car is applied to the
wrong number of arguments, but it is a pseudo-term.

The structures recognized by pseudo-termp can be recursively explored
with the same simplicity that terms can be.  In particular, if x is not
a variablep or an fquotep, then (ffn-symb x) is the function (symbol or
lambda expression) and (fargs x) is the list of argument pseudo-terms.
A metafunction (see META) or clause-processor (see
CLAUSE-PROCESSOR) may use pseudo-termp as the guard.

TERM-ORDER    the ordering relation on terms used by ACL2

ACL2 must occasionally choose which of two terms is syntactically
smaller.  The need for such a choice arises, for example, when using
equality hypotheses in conjectures (the smaller term is substituted for
the larger elsewhere in the formula), in stopping loops in permutative
rewrite rules (see LOOP-STOPPER), and in choosing the order in
which to try to cancel the addends in linear arithmetic inequalities.
When this notion of syntactic size is needed, ACL2 uses "term order."
Popularly speaking, term order is just a lexicographic ordering on
terms.  But the situation is actually more complicated.

We define term order only with respect to terms in translated form.
See TRANS.  Constants are viewed as built up by
_pseudo-function_ applications, as described at the end of this
documentation.

Term1 comes before term2 in the term order iff

     (a) the number of variable occurrences in term1 is less than that
     in term2, or

     (b) the numbers of variable occurrences in the two terms are equal
     but the number of function applications in term1 is less than that
     in term2, or

     (c) the numbers of variable occurrences in the two terms are equal,
     the numbers of functions applications in the two terms are equal,
     but the number of pseudo-function applications in term1 is less
     than that in term2, or

     (d) the numbers of variable occurrences in the two terms are equal,
     the numbers of functions applications in the two terms are equal,
     the numbers of pseudo-function applications in the two terms are
     equal, and term1 comes before term2 in a lexicographic ordering,
     lexorder, based their structure as Lisp objects:  see
     LEXORDER.

The function term-order, when applied to the translations of two ACL2
terms, returns t iff the first is "less than or equal" to the second in
the term order.

By "number of variable occurrences" we do not mean "number of distinct
variables" but "number of times a variable symbol is mentioned."  (cons
x x) has two variable occurrences, not one.  Thus, perhaps
counterintuitively, a large term that contains only one variable
occurrence, e.g., (standard-char-p (car (reverse x))) comes before
(cons x x) in the term order.

Since constants contain no variable occurrences and non-constant
expressions must contain at least one variable occurrence, constants
come before non-constants in the term order, no matter how large the
constants.  For example, the list constant

     '(monday tuesday wednesday thursday friday)

comes before x in the term order.  Because term order is involved in
the control of permutative rewrite rules and used to shift smaller
terms to the left, a set of permutative rules designed to allow the
permutation of any two tips in a tree representing the nested
application of some function will always move the constants into the
left-most tips.  Thus,

     (+ x 3 (car (reverse klst)) (dx i j)) ,

which in translated form is

     (binary-+ x
               (binary-+ '3
                         (binary-+ (dx i j)
                                   (car (reverse klst))))),

will be permuted under the built-in commutativity rules to

     (binary-+ '3
               (binary-+ x
                         (binary-+ (car (reverse klst))
                                   (dx i j))))

or

     (+ 3 x (car (reverse klst)) (dx i j)).

Two terms with the same numbers of variable occurrences, function
applications, and pseudo-function applications are ordered by
lexicographic means, based on their structures.  See LEXORDER.
Thus, if two terms (member ...) and (reverse ...) contain the same
numbers of variable occurrences and function applications, then the
member term is first in the term order because member comes before
reverse in the term order (which is here reduced to alphabetic
ordering).

It remains to discuss the notion of _pseudo-function_ applications.

Clearly, two constants are ordered using cases (c) and (d) of term
order, since they each contain 0 variable occurrences and no function
calls.  This raises the question "How many function applications are in
a constant?"  Because we regard the number of function applications as
a more fundamental measure of the size of a constant than lexicographic
considerations, we decided that for the purposes of term order,
constants would be seen as being built by primitive constructor
functions.  These constructor functions are not actually defined in
ACL2 but merely imagined for the purposes of term order.  We here use
suggestive names for these imagined functions, ignoring entirely the
prior use of these names within ACL2.  The imagined applications of
these functions are what we refer to as _pseudo-function_ applications.

The constant function z constructs 0.  Positive integers are
constructed from (z) by the successor function, s.  Thus 2 is (s (s
(z))) and contains three function applications.  100 contains one
hundred and one applications.  Negative integers are constructed from
their positive counterparts by -.  Thus, -2 is (- (s (s (z)))) and has
four applications.  Ratios are constructed by the dyadic function /.
Thus, -1/2 is

     (/ (- (s (z))) (s (s (z))))

and contains seven applications.  Complex rationals are similarly
constructed from rationals.  All character objects are considered
primitive and are constructed by constant functions of the same name.
Thus #\a and #\b both contain one application.  Strings are built from
the empty string, (o) by the "string-cons" function written cs.  Thus
"AB" is (cs (#\a) (cs (#\b) (o))) and contains five applications.
Symbols are obtained from strings by "packing" the symbol-name with the
unary function p.  Thus 'ab is

     (p (cs (#\a) (cs (#\b) (o))))

and has six applications.  Note that packages are here ignored and thus
'acl2::ab and 'my-package::ab each contain just six applications.
Finally, conses are built with cons, as usual.  So '(1 . 2) is (cons '1
'2) and contains six applications, since '1 contains two and '2
contains three.  This, for better or worse, answers the question "How
many function applications are in a constant?"

THE-METHOD    how to find proofs

Many users develop proof scripts in an Emacs buffer and submit one
event at a time to the theorem prover running in a *shell* buffer.  The
script buffer is logically divided into two regions: the events that
have been accepted by the theorem prover and those that have not yet
been accepted.  An imaginary "barrier" divides these two regions.  The
region above the barrier describes the state of the *shell* buffer (and
ACL2's logical world).  The region below the barrier is the "to do"
list.

We usually start a proof project by typing the key lemmas, and main
goal into the to do list.  Definitions are here just regarded as
theorems to prove (i.e., the measure conjectures).  Then we follow "The
Method."

(1) Think about the proof of the first theorem in the to do list.
Structure the proof either as an induction followed by simplification
or just simplification.  Have the necessary lemmas been proved? That
is, are the necessary lemmas in the done list already?  If so, proceed
to Step 2.  Otherwise, add the necessary lemmas at the front of the to
do list and repeat Step 1.

(2) Call the theorem prover on the first theorem in the to do list and
let the output stream into the *shell* buffer.  Abort the proof if it
runs more than a few seconds.

(3) If the theorem prover succeeded, advance the barrier past the
successful command and go to Step 1.

(4) Otherwise, inspect the failed proof attempt, starting from the
beginning, not the end.  Basically you should look for the first place
the proof attempt deviates from your imagined proof.  If your imagined
proof was inductive, inspect the induction scheme used by ACL2.  If
that is ok, then find the first subsequent subgoal that is stable under
simplification and think about why it was not proved by the simplifier.
If your imagined proof was not inductive, then think about the first
subgoal stable under simplification, as above.  Modify the script
appropriately.  It usually means adding lemmas to the to do list, just
in front of the theorem just tried.  It could mean adding hints to the
current theorem.  In any case, after the modifications go to Step 1.

We do not seriously suggest that this or any rotely applied algorithm
will let you drive ACL2 to difficult proofs.  Indeed, to remind you of
this we call this "The Method" rather than "the method."  That is, we
are aware of the somewhat pretentious nature of any such advice.  But
these remarks have helped many users approach ACL2 in a constructive
and disciplined way.

We say much more about The Method in the ACL2 book.  See the home page.
Also see SET-GAG-MODE for a discussion of a way for ACL2 to
help you to use The Method.

Learning to read failed proofs is a useful skill.  There are several
kinds of "checkpoints" in a proof: (1) a formula to which induction is
being (or would be) applied, (2) the first formula stable under
simplification, (3) a formula that is possibly generalized, either by
cross-fertilizing with and throwing away an equivalence hypothesis or
by explicit generalization of a term with a new variable.

At the induction checkpoint, confirm that you believe the formula being
proved is a theorem and that it is appropriately strong for an
inductive proof.  Read the selected induction scheme and make sure it
agrees with your idea of how the proof should go.

At the post-simplification checkpoint, which is probably the most
commonly seen, consider whether there are additional rewrite rules you
could prove to make the formula simplify still further.  Look for
compositions of function symbols you could rewrite.  Look for
contradictions among hypotheses and prove the appropriate implications:
for example, the checkpoint might contain the two hypotheses (P (F A))
and (NOT (Q (G (F A)))) and you might realize that (implies (p x) (q (g
x))) is a theorem.  Look for signs that your existing rules did not
apply, e.g., for terms that should have been rewritten, and figure out
why they were not.  Possible causes include that they do not exactly
match your old rules, that your old rules have hypotheses that cannot
be relieved here - perhaps because some other rules are missing, or
perhaps your old rules are disabled.  If you cannot find any further
simplifications to make in the formula, ask yourself whether it is
valid.  If so, sketch a proof.  Perhaps the proof is by appeal to a
combination of lemmas you should now prove?

At the two generalization checkpoints -- where hypotheses are discarded
or terms are replaced by variables -- ask yourself whether the result
is a theorem.  It often is not.  Think about rewrite rules that would
prove the formula.  These are often restricted versions of the
overly-general formulas created by the system's heuristics.

See PROOF-TREE for a discussion of a tool to help you navigate
through ACL2 proofs.

TTAGS-SEEN    list some declared trust tags (ttags)

     General Forms:
     :ttags-seen
     (ttags-seen)

Suppose the output is as follows.

     (T NIL)
     (FOO "/home/bob/bar.lisp"
          "/home/cindy/bar.lisp")
     Warning: This output is minimally trustworthy (see :DOC TTAGS-SEEN).

This output indicates that the current logical world has seen the
declaration of trust tag T at the top-level (see DEFTTAG) and
the declaration of trust tag FOO in the two books included from the
listed locations.  The warning emphasizes that this command cannot be
used to validate the "purity" of an ACL2 session, because using a ttag
renders enough power to hide from this or any other command the fact
that the ttag was ever declared.

As discussed elsewhere (see DEFTTAG), the only reliable way to
validate the "purity" of a session is to watch for "TTAG NOTE" output.

Another shortcoming of this command is that it only checks the current
logical world for ttag declarations.  For example, one could execute a
defttag event; then use progn! and set-raw-mode to replace system
functions with corrupt definitions or to introduce inconsistent axioms
in the ground-zero world; and finally, execute :ubt! 1 to remove all
evidence of the ttag in the world while leaving in place the corrupt
definitions or axioms.  The base world is now tainted, meaning we could
prove nil or certify a book that proves nil, but the resulting session
or book would contain no trace of the ttag that tainted it!

Despite shortcomings, this command might be useful to system hackers.
It also serves to illustrate the inherent flaw in asking a session
whether or how it is "tainted", justifying the "TTAG NOTE" approach
(see DEFTTAG).

TTREE    tag trees

Many low-level ACL2 functions take and return "tag trees" or "ttrees"
(pronounced "tee-trees") which contain various useful bits of
information such as the lemmas used, the linearize assumptions made,
etc.

Let a "tagged pair" be a list whose car is a symbol, called the "tag,"
and whose cdr is an arbitrary object, called the "tagged object."  A
"tag tree" is either nil, a tagged pair consed onto a tag tree, or a
non-nil tag tree consed onto a tag tree.

Abstractly a tag tree represents a list of sets, each member set having
a name given by one of the tags occurring in the ttree.  The elements
of the set named tag are all of the objects tagged tag in the tree.  To
cons a tagged pair (tag . obj) onto a tree is to add-to-set-equal obj
to the set corresponding to tag.  To cons two tag trees together is to
union-equal the corresponding sets.  The concrete representation of the
union so produced has duplicates in it, but we feel free to ignore or
delete duplicates.

The beauty of this definition is that to combine two non-nil tag trees
you need do only one cons.

The following function accumulates onto ans the set associated with a
given tag in a ttree:

     (defun tagged-objects (tag ttree ans)
      (cond
       ((null ttree) ans)
       ((symbolp (caar ttree))             ; ttree = ((tag . obj) . ttree)
        (tagged-objects tag (cdr ttree)
                        (cond ((eq (caar ttree) tag)
                               (add-to-set-equal (cdar ttree) ans))
                              (t ans))))
       (t                                  ; ttree = (ttree . ttree)
          (tagged-objects tag (cdr ttree)
                              (tagged-objects tag (car ttree) ans)))))

This function is defined as a :PROGRAM mode function in ACL2.

The rewriter, for example, takes a term and a ttree (among other
things), and returns a new term, term', and new ttree, ttree'.  Term'
is equivalent to term (under the current assumptions) and the ttree' is
an extension of ttree.  If we focus just on the set associated with the
tag LEMMA in the ttrees, then the set for ttree' is the extension of
that for ttree obtained by unioning into it all the runes used by the
rewrite.  The set associated with LEMMA can be obtained by
(tagged-objects 'LEMMA ttree nil).