OAI/Combinatorics/EditDistance/RowSeparation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Payload restrictions and fresh-marker row separation

  1. lemma OAI.EditDistortion.sublist_ofFn_comp line 11
  2. lemma OAI.EditDistortion.indel_le_of_matching line 20
  3. lemma OAI.EditRows.payload_mod line 33
  4. def OAI.EditRows.rowValue line 41
  5. def OAI.EditRows.rowWord line 48
  6. lemma OAI.EditRows.rowWord_length line 51
  7. lemma OAI.EditRows.rowValue_ne_none line 54
  8. def OAI.EditRows.payloadOffset line 59
  9. lemma OAI.EditRows.rowValue_payload line 62
  10. lemma OAI.EditRows.local_matching_bound line 80
  11. theorem OAI.EditRows.indel_row_separation line 146