OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationObservationCells.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Lookahead, conditional snapshots and the exact fill capacity

Lookahead may construct a next reader state, which is discarded afterward. Both that state and the original reader are included in the live trace.

  1. theorem OAI.LowSpaceSubsetSum.RepresentationObservationCells.fillAcc_size line 16
  2. theorem OAI.LowSpaceSubsetSum.RepresentationObservationCells.fill_capacity line 34
  3. def OAI.LowSpaceSubsetSum.RepresentationObservationCells.hasKey line 50
  4. theorem OAI.LowSpaceSubsetSum.RepresentationObservationCells.hasKey_value line 62
  5. theorem OAI.LowSpaceSubsetSum.RepresentationObservationCells.hasKey_cells line 70
  6. def OAI.LowSpaceSubsetSum.RepresentationObservationCells.snapshot line 108
  7. theorem OAI.LowSpaceSubsetSum.RepresentationObservationCells.snapshot_value line 119
  8. theorem OAI.LowSpaceSubsetSum.RepresentationObservationCells.snapshot_cells line 129