OAI/Computability/QuantumFactoring/NativeAIGDivOperations.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.NativeAIG.divSubInput line 13
  2. def OAI.ExactQuantumFactoring.NativeAIG.divSubState line 20
  3. lemma OAI.ExactQuantumFactoring.NativeAIG.divSub_budget line 21
  4. lemma OAI.ExactQuantumFactoring.NativeAIG.divSub_length line 26
  5. lemma OAI.ExactQuantumFactoring.NativeAIG.divSub_value line 28
  6. def OAI.ExactQuantumFactoring.NativeAIG.divUltInput line 32
  7. def OAI.ExactQuantumFactoring.NativeAIG.divUltState line 39
  8. lemma OAI.ExactQuantumFactoring.NativeAIG.ultState_budget line 40
  9. lemma OAI.ExactQuantumFactoring.NativeAIG.divUlt_budget line 42
  10. lemma OAI.ExactQuantumFactoring.NativeAIG.divUlt_value line 48
  11. def OAI.ExactQuantumFactoring.NativeAIG.divQInput line 57
  12. def OAI.ExactQuantumFactoring.NativeAIG.divQState line 65
  13. lemma OAI.ExactQuantumFactoring.NativeAIG.divQ_budget line 66
  14. lemma OAI.ExactQuantumFactoring.NativeAIG.divQ_length line 70
  15. def OAI.ExactQuantumFactoring.NativeAIG.divRInput line 72
  16. def OAI.ExactQuantumFactoring.NativeAIG.divRState line 81
  17. lemma OAI.ExactQuantumFactoring.NativeAIG.divR_budget line 82
  18. lemma OAI.ExactQuantumFactoring.NativeAIG.divR_length line 86
  19. lemma OAI.ExactQuantumFactoring.NativeAIG.divQR_value line 88