OAI/Combinatorics/EditApproximation/Coarse/CoarseInputGuard.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.coarseInputGuardWithWork_value line 12

   Source documentation

   This guard uses interval endpoints before either input slice is copied.

   theorem coarseInputGuardWithWork_value (sourceLo sourceHi targetLo targetHi : ℕ) :
       (coarseInputGuardWithWork sourceLo sourceHi targetLo targetHi).1 =
         decide (2 * (sourceHi - sourceLo) < targetHi - targetLo) := by
   …

   Mentions: OAI.EditApproximation.coarseInputGuardWithWork

2. theorem OAI.EditApproximation.coarseInputGuardWithWork_cost line 19
3. theorem OAI.EditApproximation.coarsePreparedSlicesWithWork_value line 39

   Source documentation

   The optional copied pair is absent on the long-target branch.

   theorem coarsePreparedSlicesWithWork_value (source target : List ℕ)
       (sourceLo sourceHi targetLo targetHi : ℕ)
       (hslo : sourceLo ≤ sourceHi) (hshi : sourceHi ≤ source.length)
       (htlo : targetLo ≤ targetHi) (hthi : targetHi ≤ target.length) :
       (coarsePreparedSlicesWithWork source target sourceLo sourceHi targetLo targetHi).1 =
         if 2 * (sourceHi - sourceLo) < targetHi - targetLo then none else
         some (substring source sourceLo sourceHi, substring target targetLo targetHi) := by
   …

   Mentions: OAI.EditApproximation.coarsePreparedSlicesWithWork, OAI.EditApproximation.substring