OAI/Combinatorics/KMedianRecovery/Machines/SubProgram.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.subProgram line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.cfg line 50
  3. def OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.done line 52
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.sub_initial line 55
  5. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.sub_final line 61
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.parse_nil line 67
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.parse_one line 71
  8. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.parse_false line 75
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.parse_true line 79
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.rev_nil line 84
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.rev_cons line 88
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.clear_nil line 93
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.clear_cons line 96
  14. def OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.clear_outputs line 101
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.sum_nil_false line 108
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.sum_nil_true line 112
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.sum_cons_nil line 116
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.sum_nil_cons line 121
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.sum_cons_cons line 126
  20. def OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.sum_outputs line 132
  21. def OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.rev_outputs line 162
  22. def OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.parse_outputs line 179
  23. def OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.subtractReverse_computes line 209
  24. def OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.subtract_computes line 218
  25. def OAI.MetricKMedianRecovery.BitMachine.BinarySubtraction.subtraction line 222