OAI/Combinatorics/TreeEdit/EditMetric.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TreeEdit.EditStep.symm line 13
2. theorem OAI.TreeEdit.EditStep.append_left line 19
3. theorem OAI.TreeEdit.EditStep.append_right line 27
4. theorem OAI.TreeEdit.EditScript.trans line 41
5. theorem OAI.TreeEdit.EditScript.one line 47
6. theorem OAI.TreeEdit.EditScript.symm line 50
7. theorem OAI.TreeEdit.EditScript.append_left line 55
8. theorem OAI.TreeEdit.EditScript.append_right line 61
9. theorem OAI.TreeEdit.EditScript.erase line 67
10. theorem OAI.TreeEdit.EditScript.exists_length line 72
11. theorem OAI.TreeEdit.EditScript.zero_iff line 75
12. theorem OAI.TreeEdit.ed_script line 84
13. theorem OAI.TreeEdit.ed_le_of_script line 87
14. theorem OAI.TreeEdit.ed_self line 89
15. theorem OAI.TreeEdit.ed_eq_zero_iff line 92
16. theorem OAI.TreeEdit.ed_comm line 100
17. theorem OAI.TreeEdit.ed_triangle line 105
18. theorem OAI.TreeEdit.ed_append line 108
19. theorem OAI.TreeEdit.common_lengths_nonempty line 113
20. theorem OAI.TreeEdit.common_lengths_bounded line 117
21. theorem OAI.TreeEdit.exists_lcs line 123
22. theorem OAI.TreeEdit.length_le_lcs line 127
23. theorem OAI.TreeEdit.lcs_le_length_left line 130
24. theorem OAI.TreeEdit.lcs_comm line 134
25. theorem OAI.TreeEdit.lcs_le_length_right line 139
26. theorem OAI.TreeEdit.lcs_self line 142
27. theorem OAI.TreeEdit.deficit_self line 146
28. theorem OAI.TreeEdit.deficit_pos_of_ne line 148
29. theorem OAI.TreeEdit.sublist_erase_one line 158
30. theorem OAI.TreeEdit.lcs_step_loss line 168
31. theorem OAI.TreeEdit.lcs_script_loss line 187
32. theorem OAI.TreeEdit.deficit_le_ed line 193
33. theorem OAI.TreeEdit.sublist_script line 199
34. theorem OAI.TreeEdit.ed_le_deficits line 211
35. theorem OAI.TreeEdit.ed_le_twice_deficit line 216
36. theorem OAI.TreeEdit.length_encode line 221
37. theorem OAI.TreeEdit.substitution_script line 230
38. theorem OAI.TreeEdit.encode_append line 242
39. theorem OAI.TreeEdit.encode_cons line 245
40. theorem OAI.TreeEdit.encode_step line 248
41. theorem OAI.TreeEdit.encode_script line 262
42. theorem OAI.TreeEdit.ed_encode_le line 269