EditLCSLower.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TreeEdit.BinaryLower.EditStep.common_subsequence line 11
Source documentation
Every elementary edit preserves a common subsequence after at most two unmatched symbols in total. This includes substitutions by the same letter.
```
theorem EditStep.common_subsequence {α : Type*} {x y : List α}
    (h : EditStep x y) :
    ∃ z : List α, z.Sublist x ∧ z.Sublist y ∧
      x.length + y.length ≤ 2 + 2 * z.length := by
…
```
Mentions: OAI.TreeEdit.EditStep
theorem OAI.TreeEdit.BinaryLower.EditScript.common_subsequence line 35
Source documentation
A script of cost n has a common subsequence with at most 2*n unmatched symbols in its two endpoints. Intermediate words are unrestricted.
```
theorem EditScript.common_subsequence {α : Type*} {x y : List α} {n : ℕ}
    (h : EditScript x y n) :
    ∃ z : List α, z.Sublist x ∧ z.Sublist y ∧
      x.length + y.length ≤ 2 * n + 2 * z.length := by
…
```
Mentions: OAI.TreeEdit.EditScript
theorem OAI.TreeEdit.BinaryLower.EditScript.lcs_loss_le line 49
Source documentation
The insertion/deletion deficit of a script's endpoints is at most twice its ordinary unit-edit cost.
```
theorem EditScript.lcs_loss_le {α : Type*} {x y : List α} {n : ℕ}
    (h : EditScript x y n) :
    x.length + y.length - 2 * lcs x y ≤ 2 * n := by
…
```
Mentions: OAI.TreeEdit.EditScript, OAI.TreeEdit.lcs