OAI/Combinatorics/LowSpaceSubsetSum/Streams/ResidueSort.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Concrete lexicographic residue sorting of the shared right array

  1. def OAI.LowSpaceSubsetSum.ResidueSort.relation line 13
  2. instance OAI.LowSpaceSubsetSum.ResidueSort.(instance at line 16) line 16
  3. theorem OAI.LowSpaceSubsetSum.ResidueSort.transitive line 19
  4. theorem OAI.LowSpaceSubsetSum.ResidueSort.total line 25
  5. def OAI.LowSpaceSubsetSum.ResidueSort.sort line 30
  6. theorem OAI.LowSpaceSubsetSum.ResidueSort.permutation line 33
  7. theorem OAI.LowSpaceSubsetSum.ResidueSort.size line 38
  8. theorem OAI.LowSpaceSubsetSum.ResidueSort.sorted line 43
  9. theorem OAI.LowSpaceSubsetSum.ResidueSort.index_order line 52
  10. theorem OAI.LowSpaceSubsetSum.ResidueSort.primary line 63
  11. theorem OAI.LowSpaceSubsetSum.ResidueSort.secondary line 71