OAI/Combinatorics/EditApproximation/Queries/QueryBufferSpace.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.EditApproximation.bitCompareWithWork_input_cells line 11

    Source documentation

    Materializing the two natural-word encodings fits the comparison loop.

    theorem bitCompareWithWork_input_cells (left right : List Bool) :
    left.length + right.length ≤ (bitCompareWithWork left right).2 := by
…

    Mentions: OAI.EditApproximation.bitCompareWithWork

  2. theorem OAI.EditApproximation.naturalEqualAllocation_le_work line 34
  3. theorem OAI.EditApproximation.coordinateEqualAllocation_le_work line 40
  4. theorem OAI.EditApproximation.queryHistoryEqualAllocation_le_work line 51
  5. theorem OAI.EditApproximation.queryIntervalEqualAllocation_le_work line 61
  6. theorem OAI.EditApproximation.queryOnlineKeyEqualAllocation_le_work line 71
  7. theorem OAI.EditApproximation.queryGroupKeyEqualAllocation_le_work line 81
  8. def OAI.EditApproximation.naturalEqualInvocations line 92
  9. theorem OAI.EditApproximation.naturalEqualInvocations_le_work line 94
  10. def OAI.EditApproximation.coordinateEqualInvocations line 98
  11. theorem OAI.EditApproximation.coordinateEqualInvocations_le_work line 102
  12. def OAI.EditApproximation.queryHistoryEqualInvocations line 111
  13. theorem OAI.EditApproximation.queryHistoryEqualInvocations_le_work line 114
  14. theorem OAI.EditApproximation.BinaryFraction.queryChildReadAllocation_le_work line 126
  15. theorem OAI.EditApproximation.BinaryFraction.queryHistoryReadAllocation_le_work line 133
  16. theorem OAI.EditApproximation.BinaryFraction.naturalFloorAllocation_le_work line 140
  17. theorem OAI.EditApproximation.BinaryFraction.queryOnlineIntegerReadAllocation_le_work line 148
  18. theorem OAI.EditApproximation.BinaryFraction.queryGroupDrawReadAllocation_le_work line 160
  19. def OAI.EditApproximation.BinaryFraction.queryChildReadInvocations line 176
  20. theorem OAI.EditApproximation.BinaryFraction.queryChildReadInvocations_le_work line 180
  21. def OAI.EditApproximation.BinaryFraction.queryHistoryReadInvocations line 185
  22. theorem OAI.EditApproximation.BinaryFraction.queryHistoryReadInvocations_le_work line 189