OAI/Combinatorics/LowSpaceSubsetSum/Word/WordInputDescriptor.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Executed input descriptor and main-branch guard

An indexed tail scan computes the maximum original input word. Two doubling cursors then compute the input bit length and the guard's ceiling logarithm. The original input is read-only throughout.

  1. def OAI.LowSpaceSubsetSum.WordInputDescriptor.maximumLoop line 17
  2. theorem OAI.LowSpaceSubsetSum.WordInputDescriptor.maximumLoop_upper line 25
  3. theorem OAI.LowSpaceSubsetSum.WordInputDescriptor.maximumLoop_lower line 36
  4. theorem OAI.LowSpaceSubsetSum.WordInputDescriptor.maximumLoop_work line 56
  5. theorem OAI.LowSpaceSubsetSum.WordInputDescriptor.maximumLoop_cells line 67
  6. def OAI.LowSpaceSubsetSum.WordInputDescriptor.maximum line 77
  7. theorem OAI.LowSpaceSubsetSum.WordInputDescriptor.maximum_value line 79
  8. theorem OAI.LowSpaceSubsetSum.WordInputDescriptor.maximum_work line 87
  9. theorem OAI.LowSpaceSubsetSum.WordInputDescriptor.maximum_cells line 90
  10. structure OAI.LowSpaceSubsetSum.WordInputDescriptor.Result line 93
  11. def OAI.LowSpaceSubsetSum.WordInputDescriptor.run line 102
  12. theorem OAI.LowSpaceSubsetSum.WordInputDescriptor.run_maximum line 112
  13. theorem OAI.LowSpaceSubsetSum.WordInputDescriptor.run_bits line 115
  14. theorem OAI.LowSpaceSubsetSum.WordInputDescriptor.run_scale line 118
  15. theorem OAI.LowSpaceSubsetSum.WordInputDescriptor.run_guardWidth line 122
  16. theorem OAI.LowSpaceSubsetSum.WordInputDescriptor.run_guard line 127
  17. theorem OAI.LowSpaceSubsetSum.WordInputDescriptor.run_work_exact line 133
  18. theorem OAI.LowSpaceSubsetSum.WordInputDescriptor.run_work line 142
  19. theorem OAI.LowSpaceSubsetSum.WordInputDescriptor.run_cells_small line 151
  20. theorem OAI.LowSpaceSubsetSum.WordInputDescriptor.run_cells line 154