OAI/Combinatorics/KMedianRecovery/Recovery/Pack3.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.UnaryTake.pack line 10
  2. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryTake.head_pack line 11
  3. def OAI.MetricKMedianRecovery.BitMachine.UnaryTake.counter line 12
  4. def OAI.MetricKMedianRecovery.BitMachine.UnaryTake.data line 13
  5. def OAI.MetricKMedianRecovery.BitMachine.UnaryTake.output line 14
  6. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryTake.counter_pack line 15
  7. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryTake.data_pack line 17
  8. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryTake.output_pack line 19
  9. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryTake.length_pack line 21
  10. def OAI.MetricKMedianRecovery.BitMachine.UnaryTake.counter_computes line 24
  11. def OAI.MetricKMedianRecovery.BitMachine.UnaryTake.data_computes line 25
  12. def OAI.MetricKMedianRecovery.BitMachine.UnaryTake.output_computes line 27
  13. def OAI.MetricKMedianRecovery.BitMachine.UnaryTake.pack_computes line 29
  14. def OAI.MetricKMedianRecovery.BitMachine.UnaryTake.step line 34
  15. def OAI.MetricKMedianRecovery.BitMachine.UnaryTake.step_computes line 38
  16. def OAI.MetricKMedianRecovery.BitMachine.UnaryTake.next line 48
  17. def OAI.MetricKMedianRecovery.BitMachine.UnaryTake.mass line 49
  18. def OAI.MetricKMedianRecovery.BitMachine.UnaryTake.rank line 50
  19. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryTake.projection_bounds line 51
  20. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryTake.mass_next line 57
  21. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryTake.length_next line 69
  22. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryTake.rank_next line 76
  23. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryTake.iterate_bounds line 88
  24. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryTake.stop line 101
  25. def OAI.MetricKMedianRecovery.BitMachine.UnaryTake.loop_computes line 108
  26. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryTake.next_nil line 123
  27. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryTake.next_cons line 126
  28. lemma OAI.MetricKMedianRecovery.BitMachine.UnaryTake.loop_spec line 130
  29. def OAI.MetricKMedianRecovery.BitMachine.UnaryTake.takeWords line 143
  30. def OAI.MetricKMedianRecovery.BitMachine.UnaryTake.takeWords_computes line 144