OAI/Combinatorics/EditDistance/DelimiterAlignment.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Increasing matchings through binary delimiter blocks

  1. def OAI.EditCode.BlockSpan line 16
  2. def OAI.EditCode.Missing line 19
  3. def OAI.EditCode.Gap line 22
  4. lemma OAI.EditCode.span_of_no_defect line 26
  5. lemma OAI.EditCode.defect_of_not_span line 45
  6. def OAI.EditCode.Charge line 51
  7. lemma OAI.EditCode.exists_charge line 57
  8. lemma OAI.EditCode.charge_distinct line 73
  9. lemma OAI.EditCode.missing_card line 90
  10. theorem OAI.EditCode.bad_blocks_le_loss line 99