OAI/Combinatorics/EditDistance/BlockAlignment.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Contraction of arbitrary bit alignments to letter blocks

  1. def OAI.EditCode.BlockPair line 16
  2. lemma OAI.EditCode.BlockPair.symm line 19
  3. lemma OAI.EditCode.BlockPair.span line 25
  4. lemma OAI.EditCode.pair_strict line 28
  5. lemma OAI.EditCode.pair_unique line 37
  6. lemma OAI.EditCode.span_pair line 46
  7. lemma OAI.EditCode.pair_letters line 72
  8. theorem OAI.EditCode.letter_loss_le line 96
  9. theorem OAI.EditCode.indel_code_lower line 151