OAI/Combinatorics/KMedianRecovery/Machines/StepMachine.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.pack line 13
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.sf line 15
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.sf_computes line 16
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.bf line 17
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.bf_computes line 18
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.mappedFree line 19
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.mappedFree_computes line 20
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.mappedPrefix line 22
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.mappedPrefix_computes line 23
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.Q line 27
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.Q_computes line 28
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.power line 30
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.power_computes line 31
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.base line 35
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.base_computes line 36
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.H line 50
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.H_computes line 51
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.T line 53
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.T_computes line 54
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.G line 56
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.G_computes line 57
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.U line 59
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.U_computes line 60
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.QG line 62
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.QG_computes line 63
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.contBase line 65
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.contBase_computes line 66
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.W line 80
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.W_computes line 81
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.ctx line 85
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.ctx_computes line 86
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.c line 95
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.c_computes line 96
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.a line 98
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.a_computes line 99
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.qbits line 101
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.qbits_computes line 102
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.key line 106
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.key_computes line 107
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.spare line 111
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.spare_computes line 112
  42. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.leafKey line 116
  43. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.leafKey_computes line 117
  44. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.crossInput line 121
  45. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.crossInput_computes line 122
  46. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.bankInput line 138
  47. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.bankInput_computes line 139
  48. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.banks line 148
  49. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.banks_computes line 149
  50. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.resolveInput line 151
  51. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.resolveInput_computes line 152
  52. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.prefixG line 168
  53. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.prefixG_computes line 169
  54. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.finishInput line 171
  55. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.finishInput_computes line 172
  56. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.advanceInput line 182
  57. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.advanceInput_computes line 183
  58. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.fallbackInput line 193
  59. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.fallbackInput_computes line 194
  60. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.sandwiched line 204
  61. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.sandwiched_computes line 206
  62. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.active line 209
  63. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.active_computes line 211
  64. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.nonempty line 218
  65. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.nonempty_computes line 219
  66. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.run line 221
  67. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.run_computes line 222