OAI/Combinatorics/KMedian/CookLevin/TableauRun.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.Tableau.Padded.next line 13
2. lemma OAI.MetricKMedian.PCP.Tableau.Padded.reaches line 14
3. lemma OAI.MetricKMedian.PCP.Tableau.Padded.none_iterate line 24
4. lemma OAI.MetricKMedian.PCP.Tableau.Padded.option_to_next line 28
5. lemma OAI.MetricKMedian.PCP.Tableau.Padded.fixed line 40
6. lemma OAI.MetricKMedian.PCP.Tableau.Padded.bounded line 42
7. lemma OAI.MetricKMedian.PCP.Tableau.Padded.terminal_unique line 47
8. lemma OAI.MetricKMedian.PCP.Tableau.Padded.agrees line 50
9. lemma OAI.MetricKMedian.PCP.Tableau.advance_eq_padded line 65
10. lemma OAI.MetricKMedian.PCP.Tableau.run_length line 70
11. lemma OAI.MetricKMedian.PCP.Tableau.run_of_outputs line 80