OAI/Combinatorics/EditApproximation/Binary/BinaryWarmupReads.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The warmup continuation evaluates finite input-table lookups and charges their scan costs at the point where each returned word is used.

  1. theorem OAI.EditApproximation.BinaryFraction.localWarmupReadKernelWithWork_eq line 18
  2. theorem OAI.EditApproximation.BinaryFraction.localWarmupReadKernelWithWork_cost line 28
  3. def OAI.EditApproximation.BinaryFraction.cachedLocalWarmupReadWithWork line 74
  4. theorem OAI.EditApproximation.BinaryFraction.cachedLocalWarmupReadWithWork_eq_cost line 81