OAI/Combinatorics/KMedianRecovery/Recovery/ProcessOutputs.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.process_outputs line 13
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.parse_phase line 42
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.projections_length line 62
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.raw_computes line 69
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.normalize_computes line 100
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.multiply_computes line 103
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.multiplication line 107
  8. def OAI.MetricKMedianRecovery.BitMachine.NatOps.add line 117
  9. def OAI.MetricKMedianRecovery.BitMachine.NatOps.sub line 122
  10. def OAI.MetricKMedianRecovery.BitMachine.NatOps.mul line 128
  11. def OAI.MetricKMedianRecovery.BitMachine.NatOps.div line 133
  12. def OAI.MetricKMedianRecovery.BitMachine.NatOps.mod line 139
  13. def OAI.MetricKMedianRecovery.BitMachine.NatOps.gcd line 142
  14. def OAI.MetricKMedianRecovery.BitMachine.NatOps.le line 147
  15. def OAI.MetricKMedianRecovery.BitMachine.NatOps.zero line 152
  16. def OAI.MetricKMedianRecovery.BitMachine.Signed.encode line 160
  17. def OAI.MetricKMedianRecovery.BitMachine.Signed.sign line 161
  18. def OAI.MetricKMedianRecovery.BitMachine.Signed.mag line 162
  19. def OAI.MetricKMedianRecovery.BitMachine.Signed.decode line 163
  20. def OAI.MetricKMedianRecovery.BitMachine.Signed.pack line 164
  21. def OAI.MetricKMedianRecovery.BitMachine.Signed.signed line 167
  22. lemma OAI.MetricKMedianRecovery.BitMachine.Signed.pack_bits line 169
  23. lemma OAI.MetricKMedianRecovery.BitMachine.Signed.encode_decode line 173
  24. lemma OAI.MetricKMedianRecovery.BitMachine.Signed.encode_mag line 180
  25. def OAI.MetricKMedianRecovery.BitMachine.Signed.sign_computes line 183
  26. def OAI.MetricKMedianRecovery.BitMachine.Signed.pack_computes line 185
  27. def OAI.MetricKMedianRecovery.BitMachine.Signed.cast_computes line 192
  28. def OAI.MetricKMedianRecovery.BitMachine.Signed.neg_computes line 197
  29. lemma OAI.MetricKMedianRecovery.BitMachine.Signed.signed_add line 209
  30. def OAI.MetricKMedianRecovery.BitMachine.Signed.add_computes line 216
  31. def OAI.MetricKMedianRecovery.BitMachine.Signed.addition line 257