OAI/Combinatorics/KMedian/CookLevin/SeedInput.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.Compiler.SeedProgram.leftOrder line 12
2. def OAI.MetricKMedian.PCP.Compiler.SeedProgram.rightOrder line 13
3. abbrev OAI.MetricKMedian.PCP.Compiler.SeedProgram.Width line 14
4. abbrev OAI.MetricKMedian.PCP.Compiler.SeedProgram.LeftSize line 15
5. abbrev OAI.MetricKMedian.PCP.Compiler.SeedProgram.RightSize line 16
6. def OAI.MetricKMedian.PCP.Compiler.SeedProgram.output line 18
7. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.output_raw line 26
8. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.output_perfect line 32
9. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.output_sound line 36
10. lemma OAI.MetricKMedian.PCP.Compiler.SeedProgram.poly_output_raw line 48