OAI/Combinatorics/LowSpaceSubsetSum/Search/WatchdogRanking.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Termination and value preservation under an interrupting loop

  1. theorem OAI.LowSpaceSubsetSum.Watchdog.terminates_of_ranking line 11
  2. theorem OAI.LowSpaceSubsetSum.Watchdog.terminates_value line 25
  3. theorem OAI.LowSpaceSubsetSum.Watchdog.ranked_complete line 40