OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationRecordSort.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Actual costed residue sorting of stored leaf records

  1. def OAI.LowSpaceSubsetSum.RepresentationKeys.compare line 12
  2. theorem OAI.LowSpaceSubsetSum.RepresentationKeys.compare_value line 19
  3. theorem OAI.LowSpaceSubsetSum.RepresentationKeys.compare_work line 27
  4. theorem OAI.LowSpaceSubsetSum.RepresentationKeys.comparator_polynomial line 35
  5. theorem OAI.LowSpaceSubsetSum.RepresentationKeys.compare_scale line 41
  6. def OAI.LowSpaceSubsetSum.RepresentationKeys.sort line 47
  7. theorem OAI.LowSpaceSubsetSum.RepresentationKeys.sort_value line 52
  8. theorem OAI.LowSpaceSubsetSum.RepresentationKeys.sort_work line 59
  9. theorem OAI.LowSpaceSubsetSum.RepresentationKeys.sort_polynomial line 67
  10. theorem OAI.LowSpaceSubsetSum.RepresentationKeys.sort_scale line 88
  11. theorem OAI.LowSpaceSubsetSum.RepresentationKeys.sort_parent_value line 96