OAI/Computability/QuantumFactoring/NativeAIGAddBounded.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.NativeAIG.RefsBound line 14
  2. lemma OAI.ExactQuantumFactoring.NativeAIG.RefsBound.mono line 15
  3. lemma OAI.ExactQuantumFactoring.NativeAIG.RefsBound.get line 17
  4. lemma OAI.ExactQuantumFactoring.NativeAIG.RefsBound.push line 24
  5. lemma OAI.ExactQuantumFactoring.NativeAIG.refsCode_bound line 33
  6. structure OAI.ExactQuantumFactoring.NativeAIG.AddData line 38
  7. def OAI.ExactQuantumFactoring.NativeAIG.AddOK line 47
  8. abbrev OAI.ExactQuantumFactoring.NativeAIG.AddState line 50
  9. def OAI.ExactQuantumFactoring.NativeAIG.addStepData line 51
  10. lemma OAI.ExactQuantumFactoring.NativeAIG.addStep_ok line 54
  11. def OAI.ExactQuantumFactoring.NativeAIG.addStep line 62
  12. def OAI.ExactQuantumFactoring.NativeAIG.addDataView line 63
  13. def OAI.ExactQuantumFactoring.NativeAIG.addDataCode line 64
  14. def OAI.ExactQuantumFactoring.NativeAIG.addStateCode line 67
  15. lemma OAI.ExactQuantumFactoring.NativeAIG.addStateCode_bound line 68
  16. lemma OAI.ExactQuantumFactoring.NativeAIG.budget_le_code line 79
  17. lemma OAI.ExactQuantumFactoring.NativeAIG.addStep_budget line 82
  18. lemma OAI.ExactQuantumFactoring.NativeAIG.addStep_iterate_budget line 83
  19. lemma OAI.ExactQuantumFactoring.NativeAIG.addStep_iterate_loop line 88