OAI/Computability/QuantumFactoring/NativeAIGMulProcedure.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.NativeAIG.mulAddInput line 13
  2. def OAI.ExactQuantumFactoring.NativeAIG.mulAdded line 17
  3. lemma OAI.ExactQuantumFactoring.NativeAIG.mulAdded_value line 18
  4. lemma OAI.ExactQuantumFactoring.NativeAIG.mulAdded_budget line 20
  5. lemma OAI.ExactQuantumFactoring.NativeAIG.mulAdded_length line 25
  6. def OAI.ExactQuantumFactoring.NativeAIG.mulIfInput line 31
  7. lemma OAI.ExactQuantumFactoring.NativeAIG.mulIfInput_value line 37
  8. def OAI.ExactQuantumFactoring.NativeAIG.Emission.mulBudgetP line 51
  9. def OAI.ExactQuantumFactoring.NativeAIG.Emission.mulGraphP line 53
  10. def OAI.ExactQuantumFactoring.NativeAIG.Emission.mulLhsP line 55
  11. def OAI.ExactQuantumFactoring.NativeAIG.Emission.mulRhsP line 57
  12. def OAI.ExactQuantumFactoring.NativeAIG.Emission.mulOutputP line 59
  13. def OAI.ExactQuantumFactoring.NativeAIG.Emission.mulCurrP line 61
  14. def OAI.ExactQuantumFactoring.NativeAIG.Emission.mulCinP line 63
  15. def OAI.ExactQuantumFactoring.NativeAIG.Emission.mulAddInputP line 65
  16. def OAI.ExactQuantumFactoring.NativeAIG.Emission.mulAddedP line 70
  17. def OAI.ExactQuantumFactoring.NativeAIG.Emission.mulIfInputP line 71
  18. def OAI.ExactQuantumFactoring.NativeAIG.Emission.isZeroP line 80
  19. def OAI.ExactQuantumFactoring.NativeAIG.Emission.mulNextP line 87
  20. def OAI.ExactQuantumFactoring.NativeAIG.Emission.mulStepP line 95
  21. def OAI.ExactQuantumFactoring.NativeAIG.Emission.mulIterationP line 103