OAI/Combinatorics/EditApproximation/Binary/BinaryPreparedKernelReads.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Complete reader-aware local refinement. Initial, mass, historical, and current values are obtained through costed finite-buffer readers; the complete Boolean continuation has exactly the original return word.

  1. def OAI.EditApproximation.BinaryFraction.preparedLocalKernelReadWithWork line 29
  2. theorem OAI.EditApproximation.BinaryFraction.preparedLocalKernelReadWithWork_eq line 40
  3. def OAI.EditApproximation.BinaryFraction.cachedPreparedLocalKernelReadWithWork line 61
  4. theorem OAI.EditApproximation.BinaryFraction.cachedPreparedLocalKernelReadWithWork_eq line 68