implemented new mechanism for tie breaking; proving termination: the skeleton is there, but some (hopefully trivial) sorries left