OAI/Combinatorics/MatchingCount/Machines/TreeCompiler.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MatchingFPRAS.TreeMachine.Effect line 11
2. abbrev OAI.MatchingFPRAS.TreeMachine.Label line 21
3. instance OAI.MatchingFPRAS.TreeMachine.(instance at line 22) line 22
4. def OAI.MatchingFPRAS.TreeMachine.code line 24
5. def OAI.MatchingFPRAS.TreeMachine.compile line 35
6. def OAI.MatchingFPRAS.TreeMachine.cfg line 40
7. def OAI.MatchingFPRAS.TreeMachine.SizeBound line 43
8. lemma OAI.MatchingFPRAS.TreeMachine.run_procedure line 45
9. theorem OAI.MatchingFPRAS.TreeMachine.effect_compiles line 64
10. inductive OAI.MatchingFPRAS.TreeMachine.Runs line 115
11. theorem OAI.MatchingFPRAS.TreeMachine.runs_compiles line 120
12. theorem OAI.MatchingFPRAS.TreeMachine.compile_exec line 134