OAI/Computability/MinUncut/Machines/AlphabetReduction.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.MinUncutGames.Foundations.PCP.AlphabetReduction.LegalPairline 16 - abbrev
OAI.MinUncutGames.Foundations.PCP.AlphabetReduction.InputCoordinateline 19 - def
OAI.MinUncutGames.Foundations.PCP.AlphabetReduction.pairEncodingline 21 - def
OAI.MinUncutGames.Foundations.PCP.AlphabetReduction.edgeTesterRejectline 25 - theorem
OAI.MinUncutGames.Foundations.PCP.AlphabetReduction.rejected_edge_tester_boundline 29 - theorem
OAI.MinUncutGames.Foundations.PCP.AlphabetReduction.honest_edge_testerline 45