OAI/Computability/QuantumFactoring/NativeAIGIfProcedure.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExactQuantumFactoring.NativeAIG.RefsBound.push_inc line 13
  2. def OAI.ExactQuantumFactoring.NativeAIG.ifStepData line 23
  3. lemma OAI.ExactQuantumFactoring.NativeAIG.ifStep_ok line 26
  4. def OAI.ExactQuantumFactoring.NativeAIG.ifStep line 33
  5. lemma OAI.ExactQuantumFactoring.NativeAIG.ifStep_budget line 34
  6. lemma OAI.ExactQuantumFactoring.NativeAIG.ifStep_iterate_budget line 35
  7. lemma OAI.ExactQuantumFactoring.NativeAIG.ifStep_iterate_loop line 40
  8. def OAI.ExactQuantumFactoring.NativeAIG.initializeIfData line 47
  9. lemma OAI.ExactQuantumFactoring.NativeAIG.initializeIf_ok line 48
  10. def OAI.ExactQuantumFactoring.NativeAIG.initializeIf line 51
  11. def OAI.ExactQuantumFactoring.NativeAIG.ifVecState line 52
  12. lemma OAI.ExactQuantumFactoring.NativeAIG.ifVecState_value line 53
  13. lemma OAI.ExactQuantumFactoring.NativeAIG.ifVecState_budget line 56
  14. def OAI.ExactQuantumFactoring.NativeAIG.Emission.ifStepDataP line 60
  15. def OAI.ExactQuantumFactoring.NativeAIG.Emission.ifStepP line 71
  16. def OAI.ExactQuantumFactoring.NativeAIG.Emission.ifIterationP line 73
  17. def OAI.ExactQuantumFactoring.NativeAIG.Emission.initializeIfDataP line 85
  18. def OAI.ExactQuantumFactoring.NativeAIG.Emission.initializeIfP line 90
  19. def OAI.ExactQuantumFactoring.NativeAIG.Emission.ifVecStateP line 92
  20. def OAI.ExactQuantumFactoring.NativeAIG.Emission.ifVecP line 95