Christina Kirk, Aart Middeldorp: Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems. CPP 2025: 156-170