OAI/Combinatorics/EditApproximation/Binary/BinaryLocalGrid.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Local endpoint lists executed with binary division, multiplication, subtraction and validity comparisons. Only the bounded grid-index range is visited.

  1. theorem OAI.EditApproximation.saturatingSubtractWithWork_value line 15
  2. theorem OAI.EditApproximation.saturatingSubtractWithWork_cost line 25
  3. theorem OAI.EditApproximation.naturalCeiling_div_eq_ceilDiv line 33
  4. theorem OAI.EditApproximation.gridPointsWithWork_value line 47
  5. theorem OAI.EditApproximation.makeStateWithWork_value line 58
  6. theorem OAI.EditApproximation.filterMapWithWork_value line 71
  7. theorem OAI.EditApproximation.filterMapWithWork_cost line 79
  8. theorem OAI.EditApproximation.gridStateBoxWithWork_value line 93