OAI/Combinatorics/LowSpaceSubsetSum/Counting/MatchFold.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact callback semantics for matching Cartesian occurrences.

  1. def OAI.LowSpaceSubsetSum.MatchFold.run line 13
  2. theorem OAI.LowSpaceSubsetSum.MatchFold.nil_right line 19
  3. theorem OAI.LowSpaceSubsetSum.MatchFold.append_left line 25
  4. theorem OAI.LowSpaceSubsetSum.MatchFold.filter_congr line 33
  5. theorem OAI.LowSpaceSubsetSum.MatchFold.group_eq line 44
  6. theorem OAI.LowSpaceSubsetSum.MatchFold.split_groups line 59
  7. theorem OAI.LowSpaceSubsetSum.MatchFold.skip_left line 87
  8. theorem OAI.LowSpaceSubsetSum.MatchFold.skip_right line 97