precong(A,B);This is like pre (q.v.) except that we fiddle the =^a=> graph such that the roots P and Q don't have tau arrows to themselves but Q does have an eps arrow to itself, which is deemed to match a tau-arrow from P to a divergent state P' which is related to Q. (We copy the roots, in fact, so if P or Q occur as derivatives of themselves then in that context they will have tau loops like all other nodes. The effect is simply to treat the first transition specially, just as in equality vs w. bisim.)