OAI/Combinatorics/KMedianRecovery/Recovery/Value.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.value line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.sumBit line 15
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.carryBit line 16
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.fullAdder line 18
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.add line 22
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.value_add line 29
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.value_bits line 52
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.triStacks line 59
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.stacks_zero line 61
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.stacks_one line 62
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.stacks_two line 63
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.update_zero line 65
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.update_one line 69
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.update_two line 73
  15. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.addProgram line 78
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.cfg line 112
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.done line 114
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.add_initial line 117
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.add_final line 123
  20. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.parse_nil line 129
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.parse_one line 133
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.parse_false line 137
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.parse_true line 141
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.rev_nil line 146
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.rev_cons line 150
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.sum_nil line 155
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.sum_cons_nil line 160
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.sum_nil_cons line 165
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.sum_cons_cons line 170
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.sum_outputs line 176
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.rev_outputs line 201
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.parse_outputs line 215
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.addReverse_computes line 245