Oops, I didn't consider that 'best in Arc actually does operate on a data structure that has enough information to tell you whether an infinite substructure can contain a better candidate: If any tail of the list is 'is to one of the tails you've already encountered, its length is infinite but it certainly has no better candidates (since you've already seen them all). All infinite lists in Arc have tails that contain themselves as tails, so it's possible to make an Arc 'best that terminates on any infinite list.