OAI/Combinatorics/MatchingCount/Machines/RegisterControl.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MatchingFPRAS.RegisterControl.Instr line 10
2. def OAI.MatchingFPRAS.RegisterControl.procedure line 16
3. def OAI.MatchingFPRAS.RegisterControl.successor line 19
4. abbrev OAI.MatchingFPRAS.RegisterControl.Label line 22
5. instance OAI.MatchingFPRAS.RegisterControl.(instance at line 23) line 23
6. def OAI.MatchingFPRAS.RegisterControl.code line 25
7. def OAI.MatchingFPRAS.RegisterControl.compile line 35
8. def OAI.MatchingFPRAS.RegisterControl.cfg line 39
9. inductive OAI.MatchingFPRAS.RegisterControl.Effect line 42
10. lemma OAI.MatchingFPRAS.RegisterControl.effect_compiles line 49
11. inductive OAI.MatchingFPRAS.RegisterControl.Runs line 84
12. lemma OAI.MatchingFPRAS.RegisterControl.runs_compiles line 89
13. lemma OAI.MatchingFPRAS.RegisterControl.compile_exec line 99