OAI/Combinatorics/FiniteCircle/Edit.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteCircle.EditStep.symm line 12
2. theorem OAI.FiniteCircle.EditStep.append_left line 18
3. theorem OAI.FiniteCircle.EditStep.append_right line 25
4. theorem OAI.FiniteCircle.EditStep.map line 32
5. theorem OAI.FiniteCircle.EditScript.one line 42
6. theorem OAI.FiniteCircle.EditScript.trans line 44
7. theorem OAI.FiniteCircle.EditScript.symm line 49
8. theorem OAI.FiniteCircle.EditScript.append_left line 54
9. theorem OAI.FiniteCircle.EditScript.append_right line 59
10. theorem OAI.FiniteCircle.EditScript.map line 64
11. theorem OAI.FiniteCircle.EditScript.deleteAll line 69
12. theorem OAI.FiniteCircle.EditScript.insertAll line 74
13. theorem OAI.FiniteCircle.EditScript.exists_script line 76
14. theorem OAI.FiniteCircle.EditScript.of_sublist line 79
15. theorem OAI.FiniteCircle.EditScript.of_length_eq line 89
16. theorem OAI.FiniteCircle.editDistance_spec line 103
17. theorem OAI.FiniteCircle.editDistance_le_of_script line 106
18. theorem OAI.FiniteCircle.editDistance_self line 109
19. theorem OAI.FiniteCircle.editDistance_eq_zero line 112
20. theorem OAI.FiniteCircle.editDistance_symm line 122
21. theorem OAI.FiniteCircle.editDistance_triangle line 127
22. theorem OAI.FiniteCircle.editDistance_map_le line 131
23. theorem OAI.FiniteCircle.editDistance_map_eq line 135
24. theorem OAI.FiniteCircle.encode_nil line 142
25. theorem OAI.FiniteCircle.encode_cons line 143
26. theorem OAI.FiniteCircle.encode_append line 145
27. theorem OAI.FiniteCircle.length_encode line 147
28. theorem OAI.FiniteCircle.EditStep.encode_script line 153
29. theorem OAI.FiniteCircle.EditScript.encode_script line 167
30. theorem OAI.FiniteCircle.editDistance_encode_le line 174
31. theorem OAI.FiniteCircle.lcs_exists line 178
32. theorem OAI.FiniteCircle.le_lcs line 187
33. theorem OAI.FiniteCircle.lcs_le_length_left line 195
34. theorem OAI.FiniteCircle.lcs_le_length_right line 200
35. theorem OAI.FiniteCircle.lcs_symm line 205
36. theorem OAI.FiniteCircle.lcs_self line 214
37. theorem OAI.FiniteCircle.lcs_nil_left line 217
38. theorem OAI.FiniteCircle.lcs_nil_right line 220
39. theorem OAI.FiniteCircle.lcs_mono line 223
40. theorem OAI.FiniteCircle.lcs_encode_ge line 229
41. theorem OAI.FiniteCircle.deficit_encode_le line 238
42. theorem OAI.FiniteCircle.sublist_common_large line 246
43. theorem OAI.FiniteCircle.lcs_triangle line 273
44. theorem OAI.FiniteCircle.unequalDeficit_triangle line 280
45. theorem OAI.FiniteCircle.unequalDeficit_self line 292
46. theorem OAI.FiniteCircle.EditStep.unequalDeficit_le line 295
47. theorem OAI.FiniteCircle.EditScript.unequalDeficit_le line 318
48. theorem OAI.FiniteCircle.unequalDeficit_le_editDistance line 325
49. theorem OAI.FiniteCircle.editDistance_le_two_unequalDeficit line 328
50. theorem OAI.FiniteCircle.deficit_eq_unequalDeficit line 336
51. theorem OAI.FiniteCircle.deficit_le_editDistance line 339
52. theorem OAI.FiniteCircle.editDistance_le_two_deficit line 344
53. theorem OAI.FiniteCircle.lcs_cons_right_le line 349
54. theorem OAI.FiniteCircle.lcs_cons_cons line 359
55. theorem OAI.FiniteCircle.lcs_reverse line 382
56. theorem OAI.FiniteCircle.lcs_append_common_left line 391
57. theorem OAI.FiniteCircle.lcs_append_common_right line 397
58. theorem OAI.FiniteCircle.deficit_append_common_right line 403
59. theorem OAI.FiniteCircle.lcs_map_ge line 408
60. theorem OAI.FiniteCircle.lcs_map_eq line 414
61. theorem OAI.FiniteCircle.lcs_append_replicate line 426
62. def OAI.FiniteCircle.freshPad line 464
63. theorem OAI.FiniteCircle.length_freshPad line 467
64. theorem OAI.FiniteCircle.lcs_freshPad line 470
65. theorem OAI.FiniteCircle.deficit_freshPad line 479
66. theorem OAI.FiniteCircle.sublist_take_with_loss line 487
67. theorem OAI.FiniteCircle.unequalDeficit_take_sublist_le line 513