OAI/Computability/QuantumFactoring/NativeAIGAddWrapper.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.NativeAIG.initializeAddData line 14
  2. lemma OAI.ExactQuantumFactoring.NativeAIG.initializeAdd_ok line 15
  3. def OAI.ExactQuantumFactoring.NativeAIG.initializeAdd line 18
  4. def OAI.ExactQuantumFactoring.NativeAIG.swapAddData line 19
  5. def OAI.ExactQuantumFactoring.NativeAIG.swapAdd line 20
  6. def OAI.ExactQuantumFactoring.NativeAIG.addBlastState line 22
  7. def OAI.ExactQuantumFactoring.NativeAIG.addState line 23
  8. lemma OAI.ExactQuantumFactoring.NativeAIG.addBlastState_value line 26
  9. lemma OAI.ExactQuantumFactoring.NativeAIG.addState_value line 29
  10. lemma OAI.ExactQuantumFactoring.NativeAIG.addBlastState_budget line 33
  11. lemma OAI.ExactQuantumFactoring.NativeAIG.addState_budget line 36
  12. def OAI.ExactQuantumFactoring.NativeAIG.Emission.listUnaryLength line 44
  13. def OAI.ExactQuantumFactoring.NativeAIG.Emission.initializeAddDataP line 57
  14. def OAI.ExactQuantumFactoring.NativeAIG.Emission.initializeAddP line 62
  15. def OAI.ExactQuantumFactoring.NativeAIG.Emission.swapAddDataP line 64
  16. def OAI.ExactQuantumFactoring.NativeAIG.Emission.swapAddP line 68
  17. def OAI.ExactQuantumFactoring.NativeAIG.Emission.addBlastStateP line 70
  18. def OAI.ExactQuantumFactoring.NativeAIG.Emission.addStateP line 73
  19. def OAI.ExactQuantumFactoring.NativeAIG.Emission.addP line 83