OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationStoredReader.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Stored bounded-mask readers refine the original representation streams

The maps below are semantic views. Execution uses the bounded records and shared backing array; reading preserves exactly the original cursor state.

  1. def OAI.LowSpaceSubsetSum.RepresentationStoredReader.sourceKey line 16
  2. def OAI.LowSpaceSubsetSum.RepresentationStoredReader.key line 19
  3. theorem OAI.LowSpaceSubsetSum.RepresentationStoredReader.recordKey_eq line 22
  4. abbrev OAI.LowSpaceSubsetSum.RepresentationStoredReader.Cursor line 29
  5. def OAI.LowSpaceSubsetSum.RepresentationStoredReader.cursorMap line 32
  6. abbrev OAI.LowSpaceSubsetSum.RepresentationStoredReader.State line 37
  7. theorem OAI.LowSpaceSubsetSum.RepresentationStoredReader.primary line 41
  8. theorem OAI.LowSpaceSubsetSum.RepresentationStoredReader.secondary line 45
  9. def OAI.LowSpaceSubsetSum.RepresentationStoredReader.rows line 49
  10. theorem OAI.LowSpaceSubsetSum.RepresentationStoredReader.rows_sorted line 55
  11. def OAI.LowSpaceSubsetSum.RepresentationStoredReader.start line 64
  12. def OAI.LowSpaceSubsetSum.RepresentationStoredReader.next line 68
  13. def OAI.LowSpaceSubsetSum.RepresentationStoredReader.output line 73
  14. def OAI.LowSpaceSubsetSum.RepresentationStoredReader.mappedState line 77
  15. def OAI.LowSpaceSubsetSum.RepresentationStoredReader.transportState line 82
  16. theorem OAI.LowSpaceSubsetSum.RepresentationStoredReader.transport_next line 87
  17. theorem OAI.LowSpaceSubsetSum.RepresentationStoredReader.transport_output line 97
  18. theorem OAI.LowSpaceSubsetSum.RepresentationStoredReader.transport_start line 106
  19. def OAI.LowSpaceSubsetSum.RepresentationStoredReader.semanticState line 117
  20. theorem OAI.LowSpaceSubsetSum.RepresentationStoredReader.next_map line 120
  21. theorem OAI.LowSpaceSubsetSum.RepresentationStoredReader.output_map line 132
  22. theorem OAI.LowSpaceSubsetSum.RepresentationStoredReader.mapped_primary line 142
  23. theorem OAI.LowSpaceSubsetSum.RepresentationStoredReader.mapped_start_tree line 147
  24. theorem OAI.LowSpaceSubsetSum.RepresentationStoredReader.state_ext line 160
  25. theorem OAI.LowSpaceSubsetSum.RepresentationStoredReader.mapped_secondary line 167
  26. theorem OAI.LowSpaceSubsetSum.RepresentationStoredReader.mapped_start line 173
  27. theorem OAI.LowSpaceSubsetSum.RepresentationStoredReader.semantic_start line 182
  28. theorem OAI.LowSpaceSubsetSum.RepresentationStoredReader.semantic_next line 189
  29. theorem OAI.LowSpaceSubsetSum.RepresentationStoredReader.semantic_output line 199
  30. theorem OAI.LowSpaceSubsetSum.RepresentationStoredReader.start_output_map line 204