OAI/Combinatorics/LowSpaceSubsetSum/Streams/PrefixMachine.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Explicit pending-sibling stack for prefix recomputation

A collector result is inspected and discarded in one task action. A frame contains only the next restriction and remaining index order. In particular, no overflowing dictionary or reader state is retained in a frame. Task execution inside this action is accounted for separately by the join ledger.

  1. structure OAI.LowSpaceSubsetSum.PrefixMachine.Job line 18
  2. inductive OAI.LowSpaceSubsetSum.PrefixMachine.Control line 22
  3. def OAI.LowSpaceSubsetSum.PrefixMachine.Control.stack line 28
  4. def OAI.LowSpaceSubsetSum.PrefixMachine.Control.cells line 34

    Source documentation

    Masks and an order pointer can use fewer cells. Counting every mask bit and every remaining order element still gives this conservative bound.

    def cells (s : Control n) : ℕ := (4 * n + 16) * (s.stack.length + 1)
…

    Mentions: OAI.LowSpaceSubsetSum.PrefixMachine.Control

  5. def OAI.LowSpaceSubsetSum.PrefixMachine.step line 38
  6. def OAI.LowSpaceSubsetSum.PrefixMachine.GoodStack line 52
  7. def OAI.LowSpaceSubsetSum.PrefixMachine.Invariant line 56
  8. theorem OAI.LowSpaceSubsetSum.PrefixMachine.goodStack_length line 61
  9. theorem OAI.LowSpaceSubsetSum.PrefixMachine.invariant_next line 74
  10. theorem OAI.LowSpaceSubsetSum.PrefixMachine.cells_le line 120
  11. def OAI.LowSpaceSubsetSum.PrefixMachine.jobValue line 129
  12. def OAI.LowSpaceSubsetSum.PrefixMachine.meaning line 133
  13. theorem OAI.LowSpaceSubsetSum.PrefixMachine.step_meaning line 138
  14. theorem OAI.LowSpaceSubsetSum.PrefixMachine.watchdog_sound line 167
  15. theorem OAI.LowSpaceSubsetSum.PrefixMachine.watchdog_stack_peak line 187