OAI/Combinatorics/EditApproximation/Coarse/CoarseRangeCopy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.coarseRangeCopyWithWork_value line 13

   Source documentation

   Copy a range from an indexed immutable input. Each step charges the source read, copied symbol bits, and literal binary address increment.

   theorem coarseRangeCopyWithWork_value (read : ℕ → ℕ) (start length : ℕ) :
       (coarseRangeCopyWithWork read start length).1 =
         List.ofFn (fun i : Fin length => read (start + i.val)) := by
   …

   Mentions: OAI.EditApproximation.coarseRangeCopyWithWork

2. theorem OAI.EditApproximation.coarseRangeCopyWithWork_cost line 22