OAI/Combinatorics/ParityLifts/FlowerSearch.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ParityWL.Complexity.FlowerRecord line 7
2. def OAI.ParityWL.Complexity.GoodFlower line 9
3. def OAI.ParityWL.Complexity.GoodFlower.toFlower line 17
4. lemma OAI.ParityWL.Complexity.GoodFlower.ofFlower line 42
5. def OAI.ParityWL.Complexity.flowerCandidates line 57
6. lemma OAI.ParityWL.Complexity.mem_flowerCandidates line 62
7. lemma OAI.ParityWL.Complexity.flowerCandidates_complete line 73
8. def OAI.ParityWL.Complexity.flowerList line 114
9. lemma OAI.ParityWL.Complexity.mem_flowerList line 119
10. lemma OAI.ParityWL.Complexity.flowerList_ne_nil line 124
11. def OAI.ParityWL.Complexity.selectedFlower line 135
12. lemma OAI.ParityWL.Complexity.selectedFlower_good line 138