OAI/Combinatorics/KMedian/CookLevin/CookBoundaryProgram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.MetricKMedian.PCP.Compiler.CookProgram.tapeCoding line 19
2. instance OAI.MetricKMedian.PCP.Compiler.CookProgram.tapeHardcoded line 20
3. instance OAI.MetricKMedian.PCP.Compiler.CookProgram.symbolCoding line 21
4. instance OAI.MetricKMedian.PCP.Compiler.CookProgram.symbolHardcoded line 22
5. instance OAI.MetricKMedian.PCP.Compiler.CookProgram.inputSymbolInhabited line 23
6. instance OAI.MetricKMedian.PCP.Compiler.CookProgram.outputSymbolInhabited line 24
7. lemma OAI.MetricKMedian.PCP.Compiler.CookProgram.poly_inputPrefix line 25
8. lemma OAI.MetricKMedian.PCP.Compiler.CookProgram.poly_certificateBound line 27
9. lemma OAI.MetricKMedian.PCP.Compiler.CookProgram.poly_firstCell_fixed line 31
10. lemma OAI.MetricKMedian.PCP.Compiler.CookProgram.poly_firstCell line 45
11. lemma OAI.MetricKMedian.PCP.Compiler.CookProgram.poly_lastCell_fixed line 60
12. lemma OAI.MetricKMedian.PCP.Compiler.CookProgram.poly_lastCell line 74
13. lemma OAI.MetricKMedian.PCP.Compiler.CookProgram.poly_accept line 89