OAI/Combinatorics/KMedianRecovery/Encoding/CoupledEncode.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryCorrection.encode line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryCorrection.applyWord line 14
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryCorrection.applyWord_computes line 16
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCorrection.applyWord_pack line 21
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryCorrection.mapRow line 30
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryCorrection.mapRow_computes line 31
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCorrection.mapRow_pack line 32
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryCorrection.mapHistory line 35
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryCorrection.mapHistory_computes line 36
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCorrection.mapHistory_pack line 37
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryCorrection.mapSet line 40
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryCorrection.mapSet_computes line 41
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCorrection.mapSet_pack line 42
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.stateBits line 59
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.outputBits line 62
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.outcomeBits line 63
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.mapFree line 66
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.mapFree_computes line 67
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.mapFree_pack line 68
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.mapPrefix line 71
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.mapPrefix_computes line 73
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.mapPrefix_pack line 76
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.historyBits_append line 79
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.historyBits_cons line 81
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.finish line 83
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.finish_computes line 84
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.finish_pack line 86
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.same line 91
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.same_computes line 92
  30. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.same_pack line 97