pre: are two agents related by the (weak) bisimulation preorder?

pre(A,B);

Notes

Returns true iff A and B are related by some weak bisimulation preorder. R is a weak 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 is locally divergent at a)

We set divergence by maximal fixpoint: a thing gets to be marked not globally divergent by not having @ as a summand or component (even under restriction/relabelling), and not having any tau-successors, or having every tau-successor satisfy that. Then P diverges at a iff P=a=>P' globally divergent. (So, e.g., @ does not diverge at tau.)

See also