# [isabelle] Problem with simplifier trace

Hallo!
I have a loop in my simplifier rules and I try to get to the cause of
it. I set Isabelle to give me a simplifier trace and set the
simplifier depth to 5. Then I get a trace that leaves me confused
because I don't get what's going on. I give a reduced version of my
trace to keep it simple. C1 and C2 are constructors, f is a function.
[1] Applying instance of rewrite rule R1
(C1 ?s ?v) : X ==> f ?s ?v == f (C1 ?s ?v) ?v
[1] Trying to rewrite
(C1 (C2 s) v) : X ==> f (C2 s) v == f (C1 (C2 s) v) v
[2] SIMPLIFIER INVOKED ON THE FOLLOWING TERM
(C1 (C2 s) v) : X
[2] Applying instance of rewrite rule R2
(C1 ?s ?v) : X == False
[2] Rewriting
(C1 (C2 s) v) : X == False
[1] Succeeded
f (C2 s) v == f (C1 (C2 s) v) v
What I don't get is: Why does the rule R1 succeed even if it's premise
was simplified to False. Or is there something else going on? Did I
read it wrong?
Thanks in advance,
Christoph Feller

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*