PrefixMachineRun.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Termination of the explicit prefix stack

The rank charges all possible task starts, including the sibling skipped after an early YES. The stack machine terminates in at most three times this task count plus two control actions. A collector action is a macro, whose internal primitive operations still need their own watchdog.

def OAI.LowSpaceSubsetSum.PrefixMachine.pendingWeight line 19
def OAI.LowSpaceSubsetSum.PrefixMachine.rank line 22
theorem OAI.LowSpaceSubsetSum.PrefixMachine.rank_pos line 27
theorem OAI.LowSpaceSubsetSum.PrefixMachine.rank_next line 30
theorem OAI.LowSpaceSubsetSum.PrefixMachine.output_eq_searchRight line 70
Source documentation
The explicit stack performs exactly the original prefix search.
```
theorem output_eq_searchRight (D : RepresentationParentData n) (B : ℕ)
    (check : Array (Entry (Fin n)) → Bool) (job : Job n) :
    (Watchdog.run (step D B check) Control.cells
      (3 * D.taskStarts B job.order job.restriction + 2) (.eval job [])).output =
        some (D.searchRight B check job.order job.restriction) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.RepresentationParentData, OAI.LowSpaceSubsetSum.Entry, OAI.LowSpaceSubsetSum.PrefixMachine.Job, OAI.LowSpaceSubsetSum.Watchdog.run, OAI.LowSpaceSubsetSum.PrefixMachine.step, OAI.LowSpaceSubsetSum.PrefixMachine.Control.cells