OAI/Combinatorics/KMedianRecovery/Branching/BlueNextTable.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueTable.row line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueTable.row_computes line 11
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueTable.next line 12
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueTable.next_computes line 13
  5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueTable.next_pack line 17
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueTable.initRow line 29
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueTable.initRow_computes line 31
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueTable.initial line 35
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueTable.initial_computes line 36
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueTable.initial_pack line 41
  11. def OAI.MetricKMedianRecovery.BlueDP.labels line 54
  12. def OAI.MetricKMedianRecovery.BlueDP.destinations line 55
  13. def OAI.MetricKMedianRecovery.BlueDP.cost line 56
  14. def OAI.MetricKMedianRecovery.BlueDP.Valid line 57
  15. def OAI.MetricKMedianRecovery.BlueDP.Route line 59
  16. def OAI.MetricKMedianRecovery.BlueDP.Spec line 60
  17. lemma OAI.MetricKMedianRecovery.BlueDP.select_spec line 64
  18. lemma OAI.MetricKMedianRecovery.BlueDP.route_append line 67
  19. lemma OAI.MetricKMedianRecovery.BlueDP.valid_append line 80
  20. lemma OAI.MetricKMedianRecovery.BlueDP.merge_spec line 87
  21. lemma OAI.MetricKMedianRecovery.BlueDP.empty_spec line 106
  22. lemma OAI.MetricKMedianRecovery.BlueDP.item_witness line 110
  23. lemma OAI.MetricKMedianRecovery.BlueDP.item_spec line 122
  24. lemma OAI.MetricKMedianRecovery.BlueDP.collect_items_spec line 130
  25. lemma OAI.MetricKMedianRecovery.BlueDP.collect_dest line 142
  26. lemma OAI.MetricKMedianRecovery.BlueDP.blockAt_spec line 166
  27. lemma OAI.MetricKMedianRecovery.BlueDP.block_spec line 182