OAI/Combinatorics/LowSpaceSubsetSum/Storage/StoredParentExecution.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Refinement of the stored-record parent collector

The state casts below change only the proof of the key evaluator. Semantic erasure preserves the complete stopped result, including occurrence order, query/report/copy counters and early overflow.

  1. def OAI.LowSpaceSubsetSum.MergedReader.rekey line 18
  2. theorem OAI.LowSpaceSubsetSum.MergedReader.rekey_inverse line 21
  3. theorem OAI.LowSpaceSubsetSum.MergedReader.rekey_next line 26
  4. abbrev OAI.LowSpaceSubsetSum.StoredParentExecution.State line 41
  5. theorem OAI.LowSpaceSubsetSum.StoredParentExecution.key_eq line 45
  6. def OAI.LowSpaceSubsetSum.StoredParentExecution.toStored line 52
  7. def OAI.LowSpaceSubsetSum.StoredParentExecution.start line 56
  8. def OAI.LowSpaceSubsetSum.StoredParentExecution.semanticState line 60
  9. theorem OAI.LowSpaceSubsetSum.StoredParentExecution.semantic_start line 64
  10. def OAI.LowSpaceSubsetSum.StoredParentExecution.read line 70
  11. theorem OAI.LowSpaceSubsetSum.StoredParentExecution.semantic_read line 74
  12. def OAI.LowSpaceSubsetSum.StoredParentExecution.collect line 95
  13. def OAI.LowSpaceSubsetSum.StoredParentExecution.erase line 103
  14. theorem OAI.LowSpaceSubsetSum.StoredParentExecution.collect_value line 108
  15. theorem OAI.LowSpaceSubsetSum.StoredParentExecution.erase_charge line 161
  16. theorem OAI.LowSpaceSubsetSum.StoredParentExecution.collect_work line 169