OAI/Combinatorics/LowSpaceSubsetSum/Search/Watchdog.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Interrupting the finite transition loop

The wrapper executes at most its supplied number of transitions. A timeout rejects. The completeness lemma requires the underlying run to terminate within that same budget; no after-the-fact cost computation is performed.

  1. inductive OAI.LowSpaceSubsetSum.Watchdog.Transition line 17
  2. structure OAI.LowSpaceSubsetSum.Watchdog.Result line 21
  3. def OAI.LowSpaceSubsetSum.Watchdog.run line 27
  4. def OAI.LowSpaceSubsetSum.Watchdog.accepted line 36
  5. theorem OAI.LowSpaceSubsetSum.Watchdog.steps_le line 38
  6. theorem OAI.LowSpaceSubsetSum.Watchdog.peak_le line 48
  7. theorem OAI.LowSpaceSubsetSum.Watchdog.sound line 62
  8. inductive OAI.LowSpaceSubsetSum.Watchdog.TerminatesIn line 80
  9. theorem OAI.LowSpaceSubsetSum.Watchdog.complete line 85