OAI/Combinatorics/TreeEdit/Alignments.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.TreeEdit.Alignment line 11
  2. theorem OAI.TreeEdit.Alignment.le_lcs line 20
  3. def OAI.TreeEdit.Alignment.restrict line 35
  4. theorem OAI.TreeEdit.exists_lcs_alignment line 42
  5. theorem OAI.TreeEdit.strictMono_fin_gap line 51
  6. theorem OAI.TreeEdit.div_strict_of_equal_residue line 66
  7. def OAI.TreeEdit.blockIndex line 86
  8. theorem OAI.TreeEdit.equal_label_alignment_bound line 89
  9. def OAI.TreeEdit.indexSpan line 128
  10. theorem OAI.TreeEdit.indexSpan_empty line 132
  11. theorem OAI.TreeEdit.mem_indexSpan line 135
  12. theorem OAI.TreeEdit.card_le_indexSpan line 141
  13. theorem OAI.TreeEdit.indexSpan_disjoint line 145
  14. theorem OAI.TreeEdit.sum_span_card_le line 182
  15. theorem OAI.TreeEdit.sum_span_gaps_le line 193
  16. def OAI.TreeEdit.blockPairKey line 204
  17. theorem OAI.TreeEdit.blockPairKey_monotone line 211
  18. theorem OAI.TreeEdit.blockPairKey_eq_iff line 218
  19. theorem OAI.TreeEdit.block_span_gap_budget line 239