OAI/Computability/QuantumFactoring/NativeAIGCarryProcedure.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.NativeAIG.carryStepData line 14
  2. lemma OAI.ExactQuantumFactoring.NativeAIG.carryStep_ok line 18
  3. def OAI.ExactQuantumFactoring.NativeAIG.carryStep line 23
  4. lemma OAI.ExactQuantumFactoring.NativeAIG.carryStep_budget line 24
  5. lemma OAI.ExactQuantumFactoring.NativeAIG.carryStep_iterate_budget line 25
  6. lemma OAI.ExactQuantumFactoring.NativeAIG.carryStep_iterate_loop line 30
  7. def OAI.ExactQuantumFactoring.NativeAIG.overflowState line 37
  8. lemma OAI.ExactQuantumFactoring.NativeAIG.overflowState_value line 38
  9. lemma OAI.ExactQuantumFactoring.NativeAIG.overflowState_budget line 40
  10. def OAI.ExactQuantumFactoring.NativeAIG.ultInput line 42
  11. def OAI.ExactQuantumFactoring.NativeAIG.ultState line 45
  12. lemma OAI.ExactQuantumFactoring.NativeAIG.ultState_value line 46
  13. lemma OAI.ExactQuantumFactoring.NativeAIG.ult_bound line 50
  14. def OAI.ExactQuantumFactoring.NativeAIG.Emission.carryStepDataP line 63
  15. def OAI.ExactQuantumFactoring.NativeAIG.Emission.carryStepP line 72
  16. def OAI.ExactQuantumFactoring.NativeAIG.Emission.carryIterationP line 74
  17. def OAI.ExactQuantumFactoring.NativeAIG.Emission.overflowStateP line 86
  18. def OAI.ExactQuantumFactoring.NativeAIG.Emission.ultInputP line 89
  19. def OAI.ExactQuantumFactoring.NativeAIG.Emission.ultStateP line 97
  20. def OAI.ExactQuantumFactoring.NativeAIG.Emission.ultP line 98