OAI/Combinatorics/EditDistance/FamilyRecursion.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Length, alphabet, and distortion recurrences for word families

  1. def OAI.EditFamily.familyLength line 12
  2. def OAI.EditFamily.familyAlphabet line 14
  3. def OAI.EditFamily.familyAlpha line 18
  4. def OAI.EditFamily.familyBudget line 20
  5. lemma OAI.EditFamily.familyLength_pos line 24
  6. lemma OAI.EditFamily.familyAlpha_pos line 29
  7. lemma OAI.EditFamily.familyAlpha_le_one line 33
  8. lemma OAI.EditFamily.familyBudget_nonneg line 37
  9. def OAI.EditFamily.recursive line 43
  10. lemma OAI.EditFamily.familyAlphabet_pos line 65
  11. lemma OAI.EditFamily.familyAlphabet_le line 68