OAI/Combinatorics/LowSpaceSubsetSum/Storage/ScalarObservationCells.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Lookahead, snapshots and scalar tie-buffer capacity

  1. theorem OAI.LowSpaceSubsetSum.ScalarObservationCells.fillAcc_size line 13
  2. theorem OAI.LowSpaceSubsetSum.ScalarObservationCells.fill_capacity line 31
  3. def OAI.LowSpaceSubsetSum.ScalarObservationCells.hasKey line 44
  4. theorem OAI.LowSpaceSubsetSum.ScalarObservationCells.hasKey_value line 54
  5. theorem OAI.LowSpaceSubsetSum.ScalarObservationCells.hasKey_cells line 62
  6. def OAI.LowSpaceSubsetSum.ScalarObservationCells.snapshot line 80
  7. theorem OAI.LowSpaceSubsetSum.ScalarObservationCells.snapshot_value line 89
  8. theorem OAI.LowSpaceSubsetSum.ScalarObservationCells.snapshot_cells line 97