OAI/Combinatorics/KMedian/CookLevin/TableauBoundary.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.Tableau.prefixCell line 12
2. lemma OAI.MetricKMedian.PCP.Tableau.prefixCell_complete line 14
3. lemma OAI.MetricKMedian.PCP.Tableau.prefixCell_sound line 19
4. structure OAI.MetricKMedian.PCP.Tableau.Boundary line 31
5. abbrev OAI.MetricKMedian.PCP.Tableau.BoundaryClause line 36
6. def OAI.MetricKMedian.PCP.Tableau.timeLast line 37
7. def OAI.MetricKMedian.PCP.Tableau.boundaryTime line 38
8. def OAI.MetricKMedian.PCP.Tableau.boundaryQuery line 39
9. def OAI.MetricKMedian.PCP.Tableau.boundaryRelation line 42
10. def OAI.MetricKMedian.PCP.Tableau.boundedSystem line 48
11. lemma OAI.MetricKMedian.PCP.Tableau.bounded_satisfies_iff line 52
12. lemma OAI.MetricKMedian.PCP.Tableau.decoded_boundary line 58