OAI/Combinatorics/KMedianRecovery/Recovery/Mul.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.add_length line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.mulFrom line 24
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.value_mulFrom line 28
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.normalize_mulFrom line 38
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.mStacks line 44
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.mStacks_0 line 45
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.mStacks_1 line 46
  8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.mStacks_2 line 47
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.mStacks_3 line 48
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.mStacks_4 line 49
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.upd0 line 51
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.upd1 line 54
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.upd2 line 57
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.upd3 line 60
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.upd4 line 63
  16. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.program line 67
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.cfg line 126
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.done line 128
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.initial line 131
  20. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.final line 134
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.parse_nil line 138
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.parse_one line 141
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.parse_false line 144
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.parse_true line 147
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.process_nil line 151
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.process_false line 154
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.process_true line 157
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.sum_nil line 161
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.sum_left line 166
  30. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.sum_right line 170
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.sum_both line 174
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.resty_nil line 179
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.resty_cons line 182
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.resta_nil line 185
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.resta_cons line 188
  36. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.clear_nil line 191
  37. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.clear_cons line 194
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.sum_outputs line 198
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.resta_outputs line 225
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.resty_outputs line 234
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.add_cycle line 245
  42. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.Multiplication.clear_outputs line 256