Several critical pair criteria are known that guarantee confluence of left-linear term rewrite systems. The correctness of most of these have been formalized in a proof assistant. An important exception has been the development closedness criterion of van Oostrom. The paper proof relies on graphical representations and intuition about overlapping redexes and descendants and has previously eluded all formalization attempts. We present a formalization in the proof assistant Isabelle/HOL. The result has been integrated into the certifier CeTA.
Link for further information.