OAI/Combinatorics/KMedian/CookLevin/TableauDirectoryProgram.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.poly_append_comp line 11
2. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.poly_and_comp line 14
3. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.poly_range_succ line 18
4. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.poly_range_comp line 21
5. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.poly_range_succ_comp line 23
6. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.poly_vars line 26
7. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.poly_clauses line 34
8. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.poly_boundaries line 43
9. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.poly_tests line 49
10. lemma OAI.MetricKMedian.PCP.Compiler.TableauDirectory.poly_code_eq line 52