OAI/Combinatorics/LowSpaceSubsetSum/Storage/ScalarTieOuterCells.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The outer scalar tie replay with a shared buffer and saved reader

  1. def OAI.LowSpaceSubsetSum.ScalarTieOuterCells.payload line 14
  2. def OAI.LowSpaceSubsetSum.ScalarTieOuterCells.step line 17
  3. theorem OAI.LowSpaceSubsetSum.ScalarTieOuterCells.step_value line 30
  4. theorem OAI.LowSpaceSubsetSum.ScalarTieOuterCells.payload_le line 43
  5. theorem OAI.LowSpaceSubsetSum.ScalarTieOuterCells.step_cells line 51
  6. def OAI.LowSpaceSubsetSum.ScalarTieOuterCells.run line 68
  7. theorem OAI.LowSpaceSubsetSum.ScalarTieOuterCells.run_value line 81
  8. theorem OAI.LowSpaceSubsetSum.ScalarTieOuterCells.run_cells line 106