OAI/Combinatorics/EditApproximation/Binary/BinaryPreparedOnlineReads.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The prepared online candidate executes its band reads, guard reads, and historical reads. The accepted source integer and counted coordinate representation are exactly the original ones.

  1. def OAI.EditApproximation.BinaryFraction.preparedOnlineReadCore line 14
  2. theorem OAI.EditApproximation.BinaryFraction.preparedOnlineReadCore_compare line 28
  3. def OAI.EditApproximation.BinaryFraction.preparedOnlineReadWithWork line 58
  4. def OAI.EditApproximation.BinaryFraction.preparedOnlineReadExtra line 84
  5. theorem OAI.EditApproximation.BinaryFraction.preparedOnlineReadWithWork_eq_cost line 93