Dohan Kim, Teppei Saito, René Thiemann, Akihisa Yamada: An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting. CPP 2025: 272-282