OAI/Combinatorics/MatchingCount/Machines/RegisterStructured.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MatchingFPRAS.RegisterStructured.Select line 11
2. instance OAI.MatchingFPRAS.RegisterStructured.(instance at line 12) line 12
3. def OAI.MatchingFPRAS.RegisterStructured.selectCode line 13
4. def OAI.MatchingFPRAS.RegisterStructured.select line 18
5. lemma OAI.MatchingFPRAS.RegisterStructured.select_nil line 19
6. lemma OAI.MatchingFPRAS.RegisterStructured.select_cons line 29
7. inductive OAI.MatchingFPRAS.RegisterStructured.Loop line 40
8. instance OAI.MatchingFPRAS.RegisterStructured.(instance at line 41) line 41
9. def OAI.MatchingFPRAS.RegisterStructured.loopCode line 42
10. def OAI.MatchingFPRAS.RegisterStructured.loop line 46
11. lemma OAI.MatchingFPRAS.RegisterStructured.loop_exec line 48