OAI/Combinatorics/KMedian/CookLevin/TableauRelationProgram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.PCP.Compiler.TableauDirectory.RelationSet line 15
2. def OAI.MetricKMedian.PCP.Compiler.TableauDirectory.firstControlSet line 16
3. def OAI.MetricKMedian.PCP.Compiler.TableauDirectory.lastControlSet line 18
4. def OAI.MetricKMedian.PCP.Compiler.TableauDirectory.firstCellSet line 20
5. def OAI.MetricKMedian.PCP.Compiler.TableauDirectory.lastCellSet line 22
6. def OAI.MetricKMedian.PCP.Compiler.TableauDirectory.rawAccept line 24
7. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.rawAccept_clause line 36
8. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.rawAccept_boundary line 40
9. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.rawAccept_correct line 46
10. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.poly_category line 53
11. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.poly_rawAccept line 62