OAI/Combinatorics/MatchingCount/Machines/TreePostRealization.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MatchingFPRAS.TreePost.Alphabet line 9
2. def OAI.MatchingFPRAS.TreePost.accesses line 10
3. lemma OAI.MatchingFPRAS.TreePost.accesses_bound line 12
4. def OAI.MatchingFPRAS.TreePost.machine line 14
5. def OAI.MatchingFPRAS.TreePost.overhead line 17
6. def OAI.MatchingFPRAS.TreePost.inputStacks line 20
7. lemma OAI.MatchingFPRAS.TreePost.inputStacks_bound line 22
8. def OAI.MatchingFPRAS.TreePost.packed line 33
9. def OAI.MatchingFPRAS.TreePost.steps line 35
10. theorem OAI.MatchingFPRAS.TreePost.computes line 38
11. lemma OAI.MatchingFPRAS.TreePost.packed_length line 66
12. lemma OAI.MatchingFPRAS.TreePost.weight_le_packed_length line 75
13. theorem OAI.MatchingFPRAS.TreePost.polynomial_compiles line 79