OAI/Combinatorics/TreeEdit/SegmentComparison.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TreeEdit.segment line 11
  2. theorem OAI.TreeEdit.length_segment line 14
  3. theorem OAI.TreeEdit.segment_get line 19
  4. theorem OAI.TreeEdit.take_segment line 26
  5. theorem OAI.TreeEdit.lcs_le_take_left line 30
  6. theorem OAI.TreeEdit.lcs_le_take_both line 38
  7. theorem OAI.TreeEdit.get_encode_block line 45
  8. theorem OAI.TreeEdit.segment_encode_block line 66
  9. theorem OAI.TreeEdit.span_bounds line 82
  10. theorem OAI.TreeEdit.span_length_formula line 90
  11. theorem OAI.TreeEdit.span_card_le_lcs line 97
  12. def OAI.TreeEdit.SegmentCode line 153
  13. theorem OAI.TreeEdit.indexSpan_card_cast line 158
  14. theorem OAI.TreeEdit.span_in_block line 165
  15. theorem OAI.TreeEdit.span_encode_eq line 178
  16. theorem OAI.TreeEdit.unequal_pair_bound line 195
  17. theorem OAI.TreeEdit.code_alignment_additive line 240
  18. theorem OAI.TreeEdit.code_deficit_comparison line 312
  19. theorem OAI.TreeEdit.code_edit_comparison line 336