OAI/Combinatorics/KMedian/CookLevin/InitialTable.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.Compiler.CSPTable.pullLabels line 15
2. lemma OAI.MetricKMedian.PCP.Compiler.CSPTable.poly_pullLabels line 18
3. def OAI.MetricKMedian.PCP.Compiler.CSPTable.pullRep line 26
4. lemma OAI.MetricKMedian.PCP.Compiler.CSPTable.pull_wellFormed line 35
5. def OAI.MetricKMedian.PCP.Compiler.InitialProgram.bits line 41
6. def OAI.MetricKMedian.PCP.Compiler.InitialProgram.table line 42
7. lemma OAI.MetricKMedian.PCP.Compiler.InitialProgram.poly_table line 43
8. lemma OAI.MetricKMedian.PCP.Compiler.InitialProgram.bits_valid line 46
9. def OAI.MetricKMedian.PCP.Compiler.InitialProgram.bitsRep line 47
10. def OAI.MetricKMedian.PCP.Compiler.InitialProgram.represents line 49
11. lemma OAI.MetricKMedian.PCP.Compiler.InitialProgram.valid line 52
12. lemma OAI.MetricKMedian.PCP.Compiler.InitialProgram.correct line 55