OAI/Computability/QuantumFactoring/NativeAIGMulWrapper.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactQuantumFactoring.NativeAIG.BinaryState line 14
  2. def OAI.ExactQuantumFactoring.NativeAIG.binaryStateCode line 15
  3. lemma OAI.ExactQuantumFactoring.NativeAIG.RefsBound.zeros line 16
  4. def OAI.ExactQuantumFactoring.NativeAIG.mulFirstInput line 22
  5. def OAI.ExactQuantumFactoring.NativeAIG.mulFirst line 27
  6. lemma OAI.ExactQuantumFactoring.NativeAIG.mulFirst_budget line 28
  7. lemma OAI.ExactQuantumFactoring.NativeAIG.mulFirst_length line 30
  8. lemma OAI.ExactQuantumFactoring.NativeAIG.mulFirst_value line 32
  9. def OAI.ExactQuantumFactoring.NativeAIG.initializeMul line 35
  10. def OAI.ExactQuantumFactoring.NativeAIG.mulBlastState line 42
  11. lemma OAI.ExactQuantumFactoring.NativeAIG.mulBlastState_value line 43
  12. def OAI.ExactQuantumFactoring.NativeAIG.swapBinary line 60
  13. def OAI.ExactQuantumFactoring.NativeAIG.mulState line 61
  14. lemma OAI.ExactQuantumFactoring.NativeAIG.mulState_value line 64
  15. lemma OAI.ExactQuantumFactoring.NativeAIG.mulBlastState_budget line 68
  16. lemma OAI.ExactQuantumFactoring.NativeAIG.mulState_budget line 73
  17. lemma OAI.ExactQuantumFactoring.NativeAIG.mulState_length line 81
  18. def OAI.ExactQuantumFactoring.NativeAIG.Emission.binaryGraphP line 90
  19. def OAI.ExactQuantumFactoring.NativeAIG.Emission.binaryLhsP line 92
  20. def OAI.ExactQuantumFactoring.NativeAIG.Emission.binaryRhsP line 94
  21. def OAI.ExactQuantumFactoring.NativeAIG.Emission.zerosP line 96
  22. def OAI.ExactQuantumFactoring.NativeAIG.Emission.mulFirstInputP line 100
  23. def OAI.ExactQuantumFactoring.NativeAIG.Emission.mulFirstP line 106
  24. def OAI.ExactQuantumFactoring.NativeAIG.Emission.initializeMulP line 107
  25. def OAI.ExactQuantumFactoring.NativeAIG.Emission.mulBlastStateP line 116
  26. def OAI.ExactQuantumFactoring.NativeAIG.Emission.swapBinaryP line 118
  27. def OAI.ExactQuantumFactoring.NativeAIG.Emission.mulStateP line 120
  28. def OAI.ExactQuantumFactoring.NativeAIG.Emission.mulP line 125