OAI/Combinatorics/UniformKServer/RawPartition.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformKServer.RawPartition.pack line 10
  2. def OAI.UniformKServer.RawPartition.GoodBlock line 15
  3. theorem OAI.UniformKServer.RawPartition.flatten_pack line 18
  4. theorem OAI.UniformKServer.RawPartition.pack_good line 29
  5. theorem OAI.UniformKServer.RawPartition.pack_complete line 53
  6. theorem OAI.UniformKServer.RawPartition.no_endpoint_prefix line 72
  7. theorem OAI.UniformKServer.RawPartition.good_count line 91
  8. theorem OAI.UniformKServer.RawPartition.complete_append line 100
  9. theorem OAI.UniformKServer.RawPartition.block_count_bound line 108
  10. theorem OAI.UniformKServer.RawPartition.completed_charge line 125