OAI/Computability/QuantumFactoring/NativeAIGMulBounded.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.NativeAIG.MulOK line 14
  2. abbrev OAI.ExactQuantumFactoring.NativeAIG.MulState line 15
  3. def OAI.ExactQuantumFactoring.NativeAIG.mulStateCode line 16
  4. def OAI.ExactQuantumFactoring.NativeAIG.mulStepData line 18
  5. lemma OAI.ExactQuantumFactoring.NativeAIG.mulStep_ok line 23
  6. def OAI.ExactQuantumFactoring.NativeAIG.mulStep line 35
  7. lemma OAI.ExactQuantumFactoring.NativeAIG.mulStep_budget line 36
  8. lemma OAI.ExactQuantumFactoring.NativeAIG.mulStep_lhs line 37
  9. lemma OAI.ExactQuantumFactoring.NativeAIG.mulStep_iterate_lhs line 38
  10. lemma OAI.ExactQuantumFactoring.NativeAIG.mulStep_iterate_budget line 42
  11. lemma OAI.ExactQuantumFactoring.NativeAIG.mulStep_iterate_loop line 47
  12. lemma OAI.ExactQuantumFactoring.NativeAIG.mulStateCode_bound line 56
  13. lemma OAI.ExactQuantumFactoring.NativeAIG.mulBudget_le_code line 58