OAI/Combinatorics/KMedianRecovery/Recovery/Step2.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.WordList.Lookup.step line 13
  2. def OAI.MetricKMedianRecovery.BitMachine.WordList.Lookup.step_computes line 16
  3. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Lookup.decrement_length line 22
  4. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Lookup.first_step line 26
  5. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Lookup.rest_step line 30
  6. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Lookup.length_step line 34
  7. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Lookup.iterate_bounds line 43
  8. def OAI.MetricKMedianRecovery.BitMachine.WordList.Lookup.run line 56
  9. def OAI.MetricKMedianRecovery.BitMachine.WordList.Lookup.run_computes line 57
  10. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Lookup.step_zero line 72
  11. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Lookup.step_succ line 75
  12. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Lookup.head_iterate line 82
  13. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Lookup.run_encode line 103
  14. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.length_encode_append line 114
  15. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.length_encode_drop line 119
  16. def OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.pack line 126
  17. def OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.items line 127
  18. def OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.context line 128
  19. def OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.accum line 129
  20. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.items_pack line 130
  21. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.context_pack line 132
  22. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.accum_pack line 134
  23. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.length_pack line 136
  24. def OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.items_computes line 138
  25. def OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.context_computes line 139
  26. def OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.accum_computes line 140
  27. def OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.pack_computes line 141
  28. def OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.step line 145
  29. def OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.step_computes line 148
  30. def OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.operation line 155
  31. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.step_nil line 157
  32. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.step_cons line 160
  33. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.iterate_pack line 163
  34. def OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.run line 178
  35. def OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.run_computes line 180
  36. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Fold.run_encode line 184