OAI/Computability/QuantumFactoring/NativeAIGDivWrapper.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.NativeAIG.divEqInput line 14
  2. def OAI.ExactQuantumFactoring.NativeAIG.divEqState line 18
  3. lemma OAI.ExactQuantumFactoring.NativeAIG.divEq_budget line 19
  4. lemma OAI.ExactQuantumFactoring.NativeAIG.divEq_value line 23
  5. def OAI.ExactQuantumFactoring.NativeAIG.initializeDiv line 25
  6. def OAI.ExactQuantumFactoring.NativeAIG.divLoopState line 36
  7. lemma OAI.ExactQuantumFactoring.NativeAIG.divStepState_iterate_cin line 37
  8. lemma OAI.ExactQuantumFactoring.NativeAIG.divLoop_budget line 42
  9. lemma OAI.ExactQuantumFactoring.NativeAIG.divLoop_lhs line 47
  10. lemma OAI.ExactQuantumFactoring.NativeAIG.divLoop_cin line 49
  11. lemma OAI.ExactQuantumFactoring.NativeAIG.divLoop_value line 51
  12. def OAI.ExactQuantumFactoring.NativeAIG.divideOutInput line 56
  13. def OAI.ExactQuantumFactoring.NativeAIG.divideState line 64
  14. lemma OAI.ExactQuantumFactoring.NativeAIG.divideState_value line 65
  15. lemma OAI.ExactQuantumFactoring.NativeAIG.divideState_budget line 78
  16. lemma OAI.ExactQuantumFactoring.NativeAIG.divideState_length line 83
  17. def OAI.ExactQuantumFactoring.NativeAIG.Emission.divEqInputP line 87
  18. def OAI.ExactQuantumFactoring.NativeAIG.Emission.divEqStateP line 92
  19. def OAI.ExactQuantumFactoring.NativeAIG.Emission.initializeDivP line 93
  20. def OAI.ExactQuantumFactoring.NativeAIG.Emission.divLoopStateP line 101
  21. def OAI.ExactQuantumFactoring.NativeAIG.Emission.divideOutInputP line 103
  22. def OAI.ExactQuantumFactoring.NativeAIG.Emission.divideStateP line 111
  23. def OAI.ExactQuantumFactoring.NativeAIG.Emission.divideP line 112