OAI/Computability/QuantumFactoring/NativeAIGDivBounded.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExactQuantumFactoring.NativeAIG.divStep_bound line 14
  2. structure OAI.ExactQuantumFactoring.NativeAIG.DivData line 43
  3. def OAI.ExactQuantumFactoring.NativeAIG.DivOK line 47
  4. abbrev OAI.ExactQuantumFactoring.NativeAIG.DivState line 51
  5. def OAI.ExactQuantumFactoring.NativeAIG.divDataCode line 52
  6. def OAI.ExactQuantumFactoring.NativeAIG.divStateCode line 53
  7. def OAI.ExactQuantumFactoring.NativeAIG.divStepData line 55
  8. lemma OAI.ExactQuantumFactoring.NativeAIG.divStep_ok line 58
  9. def OAI.ExactQuantumFactoring.NativeAIG.divStepState line 64
  10. lemma OAI.ExactQuantumFactoring.NativeAIG.divStepState_budget line 65
  11. lemma OAI.ExactQuantumFactoring.NativeAIG.divStepState_lhs line 67
  12. lemma OAI.ExactQuantumFactoring.NativeAIG.divStepState_iterate_lhs line 68
  13. lemma OAI.ExactQuantumFactoring.NativeAIG.divStepState_iterate_budget line 73
  14. lemma OAI.ExactQuantumFactoring.NativeAIG.divStepState_iterate_loop line 78
  15. lemma OAI.ExactQuantumFactoring.NativeAIG.divStateCode_bound line 85
  16. lemma OAI.ExactQuantumFactoring.NativeAIG.divBudget_le_code line 92