OAI/Computability/PerfectCompleteness/Machines/BinaryGapReduction.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PerfectCompleteness.BinaryGapReduction.nonemptyline 19 - theorem
OAI.PerfectCompleteness.BinaryGapReduction.exactly_twoline 22 - theorem
OAI.PerfectCompleteness.BinaryGapReduction.malformed_soundnessline 28