OAI/Combinatorics/BinaryEdit/SubsequenceIntersection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TreeEdit.BinaryLower.common_subsequence_compose line 8

   Source documentation

   Composing two common-subsequence loss bounds adds their costs.

   theorem common_subsequence_compose {α : Type*} {x y z : List α} {m n : ℕ}
       (hxy : ∃ u : List α, u.Sublist x ∧ u.Sublist y ∧
         x.length + y.length ≤ m + 2 * u.length)
       (hyz : ∃ v : List α, v.Sublist y ∧ v.Sublist z ∧
         y.length + z.length ≤ n + 2 * v.length) :
       ∃ w : List α, w.Sublist x ∧ w.Sublist z ∧
         x.length + z.length ≤ m + n + 2 * w.length := by
   …