OAI/Combinatorics/EditApproximation/Geometry/PartitionIntervals.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Valid target states from an actual alignment partition

Prefix lengths convert an ordered list partition of a target substring to valid global endpoint states. Every returned substring is exactly the corresponding partition piece, even when pieces are empty.

  1. theorem OAI.EditApproximation.flatten_take_length_le line 16
  2. theorem OAI.EditApproximation.flatten_take_succ_length line 23
  3. theorem OAI.EditApproximation.substring_middle line 30
  4. theorem OAI.EditApproximation.substring_flatten_piece line 35
  5. def OAI.EditApproximation.partitionInterval line 48
  6. theorem OAI.EditApproximation.substring_inside_shift line 62
  7. theorem OAI.EditApproximation.partitionInterval_substring line 72
  8. theorem OAI.EditApproximation.partitionInterval_shared line 86