OAI/Combinatorics/KMedian/CookLevin/TableauQueryProgram.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.Compiler.TableauDirectory.rawQuery line 15
2. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.rawQuery_clause line 39
3. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.rawQuery_boundary line 44
4. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.rawQuery_correct line 49
5. instance OAI.MetricKMedian.PCP.Compiler.TableauDirectory.queryCoding line 55
6. instance OAI.MetricKMedian.PCP.Compiler.TableauDirectory.queryHardcoded line 56
7. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.poly_rawQuery line 59