Proof Artifact for "A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching" Software

@misc{artifact,
   title = {{Proof Artifact for "A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching"}}, 
   author = {Cohen, Joshua M.},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:31808a21d5034756c3c2d3fc11b22697aaf6eee9;origin=https://doi.org/10.5281/zenodo.15838909;visit=swh:1:snp:eb7de80ce7ad282da1b64dafeea97454bc2f8111;anchor=swh:1:rel:95ec4913f8d066f491fc6864223ddc5539e2eefb;path=/joscoh-why3-semantics-14cabf2/}{\texttt{swh:1:dir:31808a21d5034756c3c2d3fc11b22697aaf6eee9}} (visited on 2025-09-22)},
   url = {https://github.com/joscoh/why3-semantics/tree/itp25},
   doi = {10.4230/artifacts.24696},
}