OAI/Combinatorics/SharpRamsey/Trees/PivotDecoder.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SharpLogRamsey.ActualPivot.FirstCode line 17
2. abbrev OAI.SharpLogRamsey.ActualPivot.SecondCode line 19
3. abbrev OAI.SharpLogRamsey.ActualPivot.Code line 22
4. def OAI.SharpLogRamsey.ActualPivot.read line 24
5. def OAI.SharpLogRamsey.ActualPivot.Input.choose line 32
6. lemma OAI.SharpLogRamsey.ActualPivot.Input.firstRow_eq line 43
7. lemma OAI.SharpLogRamsey.ActualPivot.Input.next_of_index line 48
8. lemma OAI.SharpLogRamsey.ActualPivot.Input.choose_of_index line 66
9. lemma OAI.SharpLogRamsey.ActualPivot.Input.choose_first_fail line 83
10. lemma OAI.SharpLogRamsey.ActualPivot.Input.choose_failure line 93
11. theorem OAI.SharpLogRamsey.ActualPivot.Input.choose_failure_bound line 115
12. theorem OAI.SharpLogRamsey.ActualPivot.Input.choose_valid line 122