BRR@

Major Section:  BREAK-REWRITE

Example:
(brr@ :target)      ; the term being rewritten
(brr@ :unify-subst) ; the unifying substitution

General Form:
(brr@ :symbol)

:symbol             (brr@ :symbol)
-------             ---------------------


:target             the term to be rewritten.  This term is an
                    instantiation of the left-hand side of the
                    conclusion of the rewrite-rule being broken.
                    This term is in translated form!  Thus, if
                    you are expecting (equal x nil) -- and your
                    expectation is almost right -- you will see
                    (equal x 'nil); similarly, instead of (cadr a)
                    you will see (car (cdr a)).  In translated
                    forms, all constants are quoted (even nil, t,
                    strings and numbers) and all macros are
                    expanded.


:unify-subst        the substitution that, when applied to :target,
                    produces the left-hand side of the rule being
                    broken.  This substitution is an alist pairing
                    variable symbols to translated (!) terms.


:wonp               t or nil indicating whether the rune was
                    successfully applied.  (brr@ :wonp) returns
                    nil if evaluated before :EVALing the rule.


:rewritten-rhs      the result of successfully applying the rule
                    or else nil if (brr@ :wonp) is nil.  The result
                    of successfully applying the rule is always a
                    translated (!) term and is never nil.


:failure-reason     some non-nil lisp object indicating why the rule 
                    was not applied or else nil.  Before the rule is
                    :EVALed, (brr@ :failure-reason) is nil.  After
                    :EVALing the rule, (brr@ :failure-reason) is nil
                    if (brr@ :wonp) is t.  Rather than document the
                    various non-nil objects returned as the failure
                    reason, we encourage you simply to evaluate
                    (brr@ :failure-reason) in the contexts of interest.
                    Alternatively, study the ACL2 function tilde-@-
                    failure-reason-phrase.


:lemma           *  the rewrite rule being broken.  For example,
                    (access rewrite-rule (brr@ :lemma) :lhs) will
                    return the left-hand side of the conclusion
                    of the rule.


:type-alist      *  a display of the type-alist governing :target.
                    Elements on the displayed list are of the form
                    (term type), where term is a term and type
                    describes information about term assumed to hold
                    in the current context.  The type-alist may be
                    used to determine the current assumptions, e.g.,
                    whether A is a CONSP.


:ancestors       *  a stack of frames indicating the backchain history
                    of the current context.  The theorem prover is in
                    the process of trying to establish each hypothesis
                    in this stack.  Thus, the negation of each hypothesis
                    can be assumed false.  Each frame also records the
                    rules on behalf of which this backchaining is being
                    done and the weight (function symbol count) of the
                    hypothesis.  All three items are involved in the
                    heuristic for preventing infinite backchaining.


:gstack          *  the current goal stack.  The gstack is maintained
                    by rewrite and is the data structure printed as the
                    current ``path.''  Thus, any information derivable
                    from the :path brr command is derivable from gstack.
                    For example, from gstack one might determine that
                    the current term is the second hypothesis of a
                    certain rewrite rule.