OAI/Combinatorics/EditDistance/RecursiveWords.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Recursive payloads, markers, symbol codes, and word separation

  1. lemma OAI.EditFamily.torsionHom_intCast line 15
  2. lemma OAI.EditFamily.Family.far_int line 19
  3. def OAI.EditFamily.payloadList line 36
  4. lemma OAI.EditFamily.payload_length line 40
  5. def OAI.EditFamily.payloadFn line 46
  6. lemma OAI.EditFamily.ofFn_payloadFn line 50
  7. def OAI.EditFamily.rawWord line 53
  8. lemma OAI.EditFamily.rawWord_length line 56
  9. lemma OAI.EditFamily.shift_state line 61
  10. def OAI.EditFamily.componentDistance line 74
  11. lemma OAI.EditFamily.componentDistance_nonneg line 79
  12. lemma OAI.EditFamily.payload_distance_ge_sum line 82
  13. lemma OAI.EditFamily.componentDistance_far line 88
  14. lemma OAI.EditFamily.payload_separation line 96
  15. theorem OAI.EditFamily.rawWord_far line 162
  16. lemma OAI.EditFamily.payload_distance_le_sum line 194
  17. lemma OAI.EditFamily.componentDistance_lift line 212
  18. lemma OAI.EditFamily.payload_cheap_lift line 228
  19. lemma OAI.EditFamily.rawWord_cheap_lift line 241
  20. lemma OAI.EditFamily.payload_allPhase line 267
  21. lemma OAI.EditFamily.rawWord_cheap_phase line 276
  22. def OAI.EditFamily.symbolCode line 294
  23. def OAI.EditFamily.nextWord line 300
  24. lemma OAI.EditFamily.ofFn_nextWord line 305
  25. lemma OAI.EditFamily.nextWord_distance line 309
  26. def OAI.EditFamily.nextSteps line 316
  27. lemma OAI.EditFamily.mem_nextSteps line 320
  28. def OAI.EditFamily.successor line 335