OAI/Combinatorics/LowSpaceSubsetSum/Separators/PreparedSeparatorRefinement.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Four prepared stored blocks refine the original encoded checker

  1. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorRefinement.source_ext line 13
  2. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorRefinement.lookup_congr line 19
  3. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorRefinement.left_lookup line 27
  4. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorRefinement.right_lookup line 37
  5. def OAI.LowSpaceSubsetSum.PreparedSeparatorRefinement.erase line 47
  6. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorRefinement.prepareBlock_source line 50
  7. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorRefinement.prepareFour_source line 75
  8. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorRefinement.source_result line 89
  9. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorRefinement.acceptance line 110