OAI/Combinatorics/KMedianRecovery/Recovery/Store.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.ProductBits.store line 10
  2. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.store0 line 11
  3. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.store1 line 12
  4. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.store2 line 13
  5. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.upd0 line 14
  6. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.upd1 line 16
  7. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.upd2 line 18
  8. abbrev OAI.MetricKMedianRecovery.BitMachine.ProductBits.program line 21
  9. def OAI.MetricKMedianRecovery.BitMachine.ProductBits.cfg line 62
  10. def OAI.MetricKMedianRecovery.BitMachine.ProductBits.done line 64
  11. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.copy_nil line 66
  12. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.copy_cons line 69
  13. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.parse_nil line 72
  14. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.parse_false line 75
  15. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.parse_one line 78
  16. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.parse_true line 81
  17. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.reverse_nil line 84
  18. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.reverse_cons line 87
  19. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.restore_nil line 90
  20. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.restore_cons line 93
  21. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.encode_nil line 96
  22. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.encode_cons line 99
  23. def OAI.MetricKMedianRecovery.BitMachine.ProductBits.copy_phase line 103
  24. def OAI.MetricKMedianRecovery.BitMachine.ProductBits.parse_phase line 112
  25. def OAI.MetricKMedianRecovery.BitMachine.ProductBits.reverse_phase line 132
  26. def OAI.MetricKMedianRecovery.BitMachine.ProductBits.restore_phase line 141
  27. def OAI.MetricKMedianRecovery.BitMachine.ProductBits.encode_phase line 150
  28. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.initial line 160
  29. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.final line 164
  30. def OAI.MetricKMedianRecovery.BitMachine.ProductBits.duplicate_computes line 169
  31. lemma OAI.MetricKMedianRecovery.BitMachine.ProductBits.projections_length line 182
  32. def OAI.MetricKMedianRecovery.BitMachine.ProductBits.swap_computes line 189
  33. def OAI.MetricKMedianRecovery.BitMachine.PolyComputes.pair line 210