OAI/Combinatorics/EditApproximation/Coarse/CoarseReadAccess.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.coarsePaddedReadWithWork_value line 13

   Source documentation

   A padded-source lookup tests its virtual endpoint and then reads the original symbol array. Padding is represented by none.

   theorem coarsePaddedReadWithWork_value {α : Type*} (n : ℕ) (source : List α) (offset : ℕ) :
       (coarsePaddedReadWithWork n source offset).1 = coarsePaddedRead n source offset := by
   …

   Mentions: OAI.EditApproximation.coarsePaddedReadWithWork, OAI.EditApproximation.coarsePaddedRead

2. theorem OAI.EditApproximation.coarsePaddedReadWithWork_cost line 19
3. theorem OAI.EditApproximation.coarsePaddedRead_symbol_mem line 26
4. theorem OAI.EditApproximation.coarseChildOffsetWithWork_value line 35

   Source documentation

   Child offsets are formed by literal multiplication and addition.

   theorem coarseChildOffsetWithWork_value (offset capacity index : ℕ) :
       bitWordValue (coarseChildOffsetWithWork offset capacity index).1 = offset + index * capacity := by
   …

   Mentions: OAI.EditApproximation.bitWordValue, OAI.EditApproximation.coarseChildOffsetWithWork

5. theorem OAI.EditApproximation.coarseChildOffsetWithWork_cost line 39