OAI/Combinatorics/BinaryEdit/LCSCore.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TreeEdit.BinaryLower.common_sublist_lower_bound line 14

   Source documentation

   Two sublists of one word have a common sublist whose deficit is at most the sum of their deficits in that word.

   theorem common_sublist_lower_bound {α : Type*} {u v w : List α}
       (hu : u.Sublist w) (hv : v.Sublist w) :
       ∃ z : List α, z.Sublist u ∧ z.Sublist v ∧
         u.length + v.length ≤ w.length + z.length := by
   …

2. theorem OAI.TreeEdit.BinaryLower.sublist_survives_deletions line 48

   Source documentation

   Deleting at most k positions from a word destroys at most k positions of any selected subsequence.

   theorem sublist_survives_deletions {α : Type*} {u v w : List α} {k : ℕ}
       (hu : u.Sublist w) (hv : v.Sublist w)
       (hk : w.length ≤ v.length + k) :
       ∃ z : List α, z.Sublist u ∧ z.Sublist v ∧ u.length ≤ z.length + k := by
   …