Formalized Confluence of Quasi-Decreasing, Strongly Deterministic Conditional TRSs
arXiv:1609.03341
Abstract
We present an Isabelle/HOL formalization of a characterization of confluence for quasi-reductive strongly deterministic conditional term rewrite systems, due to Avenhaus and Loría-Sáenz.
IWC 2016