Confluence of an Extension of Combinatory Logic by Boolean Constants
Łukasz Czajka · arXiv (Cornell University) · 2017
We show confluence of a conditional term rewriting system CL-pc^1, which is an extension of Combinatory Logic by Boolean constants. This solves problem 15 from the RTA list of open problems. The proof has been fully formalized in the Coq proof assistant.