I haven't been following this thread in any detail, but the programming
of bra/ket simplification has been,
I think, a fairly common topic. I think I even wrote some programs to do
this with Bruce Char over 30 years ago.
In any case, my thought now is that local transformation rules is NOT
the way to do this, except
as a last resort. Instead, is there a canonical representation that
all these expressions can
be forced into? One which will necessarily be simplified (with respect
to that canonical form)?
Good luck.
RJf