OAI/Combinatorics/TreeEdit/Delimiter.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TreeEdit.Delimiter.eq_of_full_lcs line 9
2. def OAI.TreeEdit.Delimiter.Synchronizing line 16
3. lemma OAI.TreeEdit.Delimiter.full_fiber line 21
4. lemma OAI.TreeEdit.Delimiter.good_fiber_matches line 41
5. lemma OAI.TreeEdit.Delimiter.alignment_bound line 75
6. lemma OAI.TreeEdit.Delimiter.deficit_bound line 140
7. def OAI.TreeEdit.Delimiter.bit line 155
8. def OAI.TreeEdit.Delimiter.code line 159
9. lemma OAI.TreeEdit.Delimiter.bit_true line 162
10. lemma OAI.TreeEdit.Delimiter.bit_label line 169
11. lemma OAI.TreeEdit.Delimiter.code_injective line 178
12. lemma OAI.TreeEdit.Delimiter.get_position line 189
13. lemma OAI.TreeEdit.Delimiter.bit_position line 196
14. lemma OAI.TreeEdit.Delimiter.marker line 203
15. lemma OAI.TreeEdit.Delimiter.code_synchronizing line 222
16. def OAI.TreeEdit.Delimiter.width line 253
17. lemma OAI.TreeEdit.Delimiter.width_eq line 255
18. lemma OAI.TreeEdit.Delimiter.exists_code line 259
19. theorem OAI.TreeEdit.Delimiter.transfer line 266