OAI/Computability/QuantumFactoring/NativeAIGSubProcedure.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExactQuantumFactoring.NativeAIG.neg_bound line 14
  2. lemma OAI.ExactQuantumFactoring.NativeAIG.sub_bound line 19
  3. def OAI.ExactQuantumFactoring.NativeAIG.negInput line 28
  4. def OAI.ExactQuantumFactoring.NativeAIG.negState line 32
  5. lemma OAI.ExactQuantumFactoring.NativeAIG.negState_value line 33
  6. lemma OAI.ExactQuantumFactoring.NativeAIG.negState_budget line 35
  7. lemma OAI.ExactQuantumFactoring.NativeAIG.negState_length line 38
  8. def OAI.ExactQuantumFactoring.NativeAIG.subNext line 42
  9. def OAI.ExactQuantumFactoring.NativeAIG.subState line 46
  10. lemma OAI.ExactQuantumFactoring.NativeAIG.subState_value line 47
  11. lemma OAI.ExactQuantumFactoring.NativeAIG.subState_budget line 55
  12. lemma OAI.ExactQuantumFactoring.NativeAIG.subState_length line 61