OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorExecutionMap.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Record-map refinement of the complete separator execution

Mapping stored records to their mathematical views preserves not only acceptance but the original scan and workspace ledgers.

  1. def OAI.LowSpaceSubsetSum.SeparatorExecutionMap.mapOut line 15
  2. theorem OAI.LowSpaceSubsetSum.SeparatorExecutionMap.merge_map line 17
  3. theorem OAI.LowSpaceSubsetSum.SeparatorExecutionMap.sortRun_split line 39
  4. theorem OAI.LowSpaceSubsetSum.SeparatorExecutionMap.sortRun_map line 53
  5. theorem OAI.LowSpaceSubsetSum.SeparatorExecutionMap.sort_map line 70
  6. theorem OAI.LowSpaceSubsetSum.SeparatorExecutionMap.find_map line 75
  7. theorem OAI.LowSpaceSubsetSum.SeparatorExecutionMap.terminal_map line 97
  8. theorem OAI.LowSpaceSubsetSum.SeparatorExecutionMap.bounded_map line 106
  9. theorem OAI.LowSpaceSubsetSum.SeparatorExecutionMap.keep_map line 115
  10. theorem OAI.LowSpaceSubsetSum.SeparatorExecutionMap.traversal_map line 121
  11. def OAI.LowSpaceSubsetSum.SeparatorExecutionMap.block line 135
  12. theorem OAI.LowSpaceSubsetSum.SeparatorExecutionMap.blocks_map line 143