2026-07-21T20:45:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26994 2026-07-16T09:49:34Z ddc:004 open_access

Completing Almost Fair Simulations Correnson, Arthur Kuhn, Iona Finkbeiner, Bernd Fair Simulation Deductive Systems Interactive Proof Assistants Coinduction Language Containment The paper Almost Fair Simulations recently introduced a collection of deductive systems for interactive proofs of language inclusion between Büchi automata. These deductive systems enable intuitive proofs via cyclic reasoning principles, but are unfortunately incomplete for fair similarity, a standard notion of refinement for Büchi automata. In this paper, we address this shortcoming by presenting a new deductive system for language inclusion of Büchi automata that preserves the simplicity of Almost Fair Simulations, with the additional benefit of being complete for fair similarity. We mechanized the soundness and the completeness proofs of our new system in the Rocq proof assistant. The proofs rely on a new technique we call nested parameterized coinduction, an adaptation of Hur’s et al. parameterized coinduction for the difficult case of proofs by coinduction-induction-coinduction. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Arthur Correnson and Iona Kuhn and Bernd Finkbeiner 2026 Is Part Of LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2026.20 urn:nbn:de:0030-drops-269944 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.20 eng https://creativecommons.org/licenses/by/4.0/legalcode