OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorTerminal.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The separator's terminal sort and first exact-weight match

  1. def OAI.LowSpaceSubsetSum.SeparatorTerminal.read line 13
  2. theorem OAI.LowSpaceSubsetSum.SeparatorTerminal.reader line 17
  3. def OAI.LowSpaceSubsetSum.SeparatorTerminal.sort line 21
  4. theorem OAI.LowSpaceSubsetSum.SeparatorTerminal.sort_perm line 24
  5. theorem OAI.LowSpaceSubsetSum.SeparatorTerminal.sort_sorted line 29
  6. def OAI.LowSpaceSubsetSum.SeparatorTerminal.run line 37
  7. theorem OAI.LowSpaceSubsetSum.SeparatorTerminal.correct line 47
  8. theorem OAI.LowSpaceSubsetSum.SeparatorTerminal.scans_le line 62
  9. def OAI.LowSpaceSubsetSum.SeparatorTerminal.bounded line 82

    Source documentation

    The caller's capacity guard also bounds the terminal cost on every input.

    def bounded (n : ℕ) (wx : α → ℤ) (wy : β → ℤ) (target : ℤ) (xs : List α) (ys : List β) :
    SeparatorTraversal.Result :=
…

    Mentions: OAI.LowSpaceSubsetSum.SeparatorTraversal.Result

  10. theorem OAI.LowSpaceSubsetSum.SeparatorTerminal.bounded_correct line 86
  11. theorem OAI.LowSpaceSubsetSum.SeparatorTerminal.bounded_scans line 91
  12. theorem OAI.LowSpaceSubsetSum.SeparatorTerminal.bounded_peak line 100
  13. theorem OAI.LowSpaceSubsetSum.SeparatorTerminal.bounded_peak_capacity line 115