### DETAILS to question:

Why isn't this rewrite rule being applied?

Continuing the discussion from the answer to that question (main text):

In rare cases, something subtle may be going on that prevents the rewriter from being able to establish a hypothesis -- especially, when a hypothesis is a subterm of the left-hand side of the conclusion occurring in a context in which a term may only be replaced by an equal value, not one that is merely Boolean equivalent. Here is a reasonably small example.

```;;; Start ACL2 input

(defun f (x) (not (not x)))

; Note: The example should work with (defun f (x) x) instead, but that would
; give the system too much help since its "type-reasoning" system would know
; that (f x) = x.

; The following thorem says in Boolean (iff) contexts that we should always
; rewrite (f x) to (if x t nil).  (We could actually use x on the right-hand
; side in place of (if x t nil), but this way we the rule is not an
; abbreviation rule and hence we can use :monitor on it.)

(defthm f-x-iff-x (iff (f x) (if x t nil)))

(in-theory (disable f))

(defun g (x) x)

; If x is not nil, then (g x) is not nil:
(defthm g-x-if-x (implies x (g x)))

; NOTE!  The rule g-x-if-x immediately above is a good example of one that
; would be better cast as an unconditional rewrite rule.  In this case, the
; rule (iff (g x) x) would allow the THM below to get proved.

(in-theory (disable g))

; The following fails because (f x) is not rewritten, even though it is an
; iff-context, i.e. the HYP. of g-x-if-x

; Now comes the subtle problem.  As we will see below, when the rewriter
; attempts to apply the rule g-x-if-x to (g (f x)), it will try to verify that
; (f x) is not nil.  But by then it has already attempted to rewrite (f x) to a
; term equal to (f x), not just Boolean equivalent (because (f x) is an
; argument of g), and the best it could do was return (f x) from that attempt.
; It does not try to rewrite (f x) again when relieving the hypothesis of
; g-x-if-x, which is too bad since otherwise it could have applied f-x-iff-x.

(thm (implies x (g (f x))))

; The rest of this FAQ entry is in two parts.  First we show the use of the
; break-rewrite utility.  Second, we trace parts of the rewriter, an activity
; that is quite obscure and is really intended for those interested in the ACL2
; implementation.

; First, we use break-rewrite as shown below to try to see why the proof fails.
; Unfortunately, it appears below that f-x-iff-x is not even being tried!

#|

ACL2 !>:brr t
The monitored runes are:
NIL
T
ACL2 !>:monitor (:rewrite f-x-iff-x) t
(((:REWRITE F-X-IFF-X) 'T))
ACL2 !>:monitor (:rewrite g-x-if-x) t
(((:REWRITE F-X-IFF-X) 'T)
((:REWRITE G-X-IF-X) 'T))
ACL2 !>(thm (implies x (g (f x))))

(1 Breaking (:REWRITE G-X-IF-X) on (G (F X)):
1 ACL2 >:go

1x (:REWRITE G-X-IF-X) failed because :HYP 1 rewrote to (F X).
1)

Name the formula above *1.

No induction schemes are suggested by *1.  Consequently, the proof
attempt has failed.

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION IMPLIES))
Warnings:  None
Time:  0.10 seconds (prove: 0.08, print: 0.00, other: 0.02)

******** FAILED ********  See :DOC failure  ******** FAILED ********
ACL2 !>

|#

```
Finally, here is our trace, carried out in a GCL version of ACL2. NOTE: This version of trace will probably not work in Allegro versions 5.0.1 and earlier.
```#|

ACL2 !>:q

Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).

ACL2>(trace (rewrite
:entry (list (nth 0 si::arglist) ; term
(nth 1 si::arglist) ; alist
(nth 5 si::arglist) ; geneqv
))
(rewrite-with-lemma
:entry (list (nth 0 si::arglist) ; term
(cadr (access rewrite-rule (nth 1 si::arglist) :rune)) ; lemma name
(nth 4 si::arglist) ; geneqv
)))
(REWRITE REWRITE-WITH-LEMMA ACL2_*1*_ACL2::REWRITE-WITH-LEMMA
ACL2_*1*_ACL2::REWRITE)

ACL2>(LP)

ACL2 Version 2.5.  Level 1.  Cbd
"/u/kaufmann/test/".
Type :help for help.

ACL2 !>(thm (implies x (g (f x))))
1> (REWRITE X NIL
((NIL IFF
:FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE
NIL)))>
<1 (REWRITE X NIL)>
1> (REWRITE (G (F X))
NIL
((NIL IFF
:FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE
NIL)))>
; Notice (second NIL on next line) that we are preserving
; equality, not Boolean equivalence.  Hence we are also
; preserving equality in the REWRITE-WITH-LEMMA call that
; follows:
2> (REWRITE (F X) NIL NIL)>
3> (REWRITE X NIL NIL)>
<3 (REWRITE X NIL)>
3> (REWRITE-WITH-LEMMA (F X) F-X-IFF-X NIL)>
; The lemma F-X-IFF-X does not apply because the context
; requires preservation of equality, not mere Boolean equivalence.
; At this point that is not a problem; in fact it is entirely
; appropriate.
<3 (REWRITE-WITH-LEMMA NIL (F X) NIL)>
; So, (F X) rewrote to itself:
<2 (REWRITE (F X) NIL)>
2> (REWRITE-WITH-LEMMA (G (F X))
G-X-IF-X
((NIL IFF
:FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE
NIL)))>
; Notice that in the next call, we are not rewriting the term (F X), but
; rather, are rewriting X where X is bound to (F X).  This is unfortunate
; since unlike the earlier rewrite of this term, we now have a Boolean
; context (indicated by the IFF below), so this time the lemma F-X-IFF-X
; would have applied.  This call of REWRITE is thus doomed simply to
; return (F X).
3> (REWRITE X ((X F X))
((NIL IFF
:FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE
NIL)))>
<3 (REWRITE (F X) NIL)>
<2 (REWRITE-WITH-LEMMA NIL (G (F X)) NIL)>
<1 (REWRITE (G (F X)) NIL)>

Name the formula above *1.

No induction schemes are suggested by *1.  Consequently, the proof
attempt has failed.

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION IMPLIES))
Warnings:  None
Time:  0.03 seconds (prove: 0.02, print: 0.00, other: 0.01)

******** FAILED ********  See :DOC failure  ******** FAILED ********
ACL2 !>

|#
```