Thanks for the reply.
I think proving two expressions by Analyzer directly is another reasonable solution, but there may be a higher time overhead compared with the “rewrite” method. Currently, the StructuralEqual mechanism has limit ability (only remap-var case) to distinguish these expressions. Overall, this is an idea worth trying and I will try to write a new mechanism similar to the StructuralEqual to solve this problem.
For your second question, actually the RewriteSimplifier is part of the Analyzer. But it is true that adding the new rule directly into tir.Simplify may be a better way and I will try it.
Thanks again for your excellent suggestions!