OAI/Combinatorics/KMedianRecovery/Encoding/InstructionBits.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.instructionBits line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.logBits line 13
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.logBits_append line 14
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.finished line 17
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.finished_computes line 18
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.finished_pack line 20
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.chunk line 24
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.chunk_computes line 26
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.chunk_pack line 32
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.step line 39
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.step_computes line 41
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.pack line 44
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.step_pack line 47
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.iterate_pack line 54
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.source_run_next line 63
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.log_length line 67
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.capPoly line 91
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.iterate_length line 93
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.cap line 112
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.run line 113
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.run_computes line 115
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRunTrace.run_pack line 118