OAI/Combinatorics/KMedianRecovery/Branching/BlueTable.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedianRecovery.BlueDP.Table line 10
  2. def OAI.MetricKMedianRecovery.BlueDP.lookup line 11
  3. lemma OAI.MetricKMedianRecovery.BlueDP.lookup_map line 14
  4. def OAI.MetricKMedianRecovery.BlueDP.states line 24
  5. lemma OAI.MetricKMedianRecovery.BlueDP.mem_states line 25
  6. lemma OAI.MetricKMedianRecovery.BlueDP.states_length line 36
  7. def OAI.MetricKMedianRecovery.BlueDP.initialTable line 38
  8. def OAI.MetricKMedianRecovery.BlueDP.nextTable line 39
  9. def OAI.MetricKMedianRecovery.BlueDP.tables line 41
  10. lemma OAI.MetricKMedianRecovery.BlueDP.tables_eq line 44
  11. lemma OAI.MetricKMedianRecovery.BlueDP.lookup_tables line 59
  12. lemma OAI.MetricKMedianRecovery.BlueDP.tables_length line 62
  13. def OAI.MetricKMedianRecovery.BlueDP.tableStep line 65
  14. def OAI.MetricKMedianRecovery.BlueDP.tableRun line 69
  15. lemma OAI.MetricKMedianRecovery.BlueDP.tableRun_spec line 71
  16. def OAI.MetricKMedianRecovery.BlueDP.tableBest line 82
  17. lemma OAI.MetricKMedianRecovery.BlueDP.tableBest_eq line 84
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueStates.key_sublist line 91
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueStates.states_encode line 95
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueStates.run line 103
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueStates.run_computes line 104
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueStates.run_pack line 105
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueStates.nonemptyKey line 111
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueStates.nonemptyKey_computes line 112
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueStates.blocks line 114
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueStates.blocks_computes line 115
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueStates.key_empty line 117
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueStates.nonemptyKey_pair line 126
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueStates.blocks_pack line 129