OAI/Combinatorics/EditApproximation/Binary/BinaryBufferSpace.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Stored key/value words and the actual linear lookup call tree. Reads return pointers to retained words; only comparison scratch is fresh.

  1. def OAI.EditApproximation.BinaryFraction.storedCells line 13
  2. def OAI.EditApproximation.BinaryFraction.bufferCells line 16
  3. theorem OAI.EditApproximation.BinaryFraction.storedCells_le_width line 20
  4. theorem OAI.EditApproximation.BinaryFraction.bufferCells_le line 26
  5. theorem OAI.EditApproximation.BinaryFraction.bufferCells_le_fourthPower line 37
  6. def OAI.EditApproximation.BinaryFraction.gatheredLookupInvocations line 56
  7. theorem OAI.EditApproximation.BinaryFraction.gatheredLookupAllocation_le_work line 63
  8. theorem OAI.EditApproximation.BinaryFraction.gatheredLookupInvocations_le_work line 82