Returns true iff A and B are related by some strong bisimulation preorder. R is a strong bisimulation preorder iff PRQ implies
Q is no more divergent than P and
P-a->P' implies Q-a->Q' and P' R Q' and
either P diverges globally or Q-a->Q' implies P-a->P' and P' R Q' (except that we allow Q-a->Q' to go unmatched if P -a-> some globally divergent state.)
Here "P diverges globally" means P has @ as a summand or component, (possibly after variable lookup, possible under restriction/relabelling) "P diverges locally at a" means P -a-> P' which diverges globally. "Q is no more divergent than P" means if Q diverges (globally, at a) so does P.
So if there are no @s in sight, this is the same as strongeq.