OAI/Computability/QuantumFactoring/NativeAIGEqProcedure.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.NativeAIG.eqGate_bound line 12
2. lemma OAI.ExactQuantumFactoring.NativeAIG.andGate_bound line 13
3. lemma OAI.ExactQuantumFactoring.NativeAIG.zipVec_bound line 14
4. lemma OAI.ExactQuantumFactoring.NativeAIG.foldVec_bound line 27
5. lemma OAI.ExactQuantumFactoring.NativeAIG.eqVec_bound line 39
6. def OAI.ExactQuantumFactoring.NativeAIG.eqNext line 48
7. def OAI.ExactQuantumFactoring.NativeAIG.eqState line 53
8. lemma OAI.ExactQuantumFactoring.NativeAIG.eqState_value line 54
9. lemma OAI.ExactQuantumFactoring.NativeAIG.eqState_budget line 63
10. def OAI.ExactQuantumFactoring.NativeAIG.Emission.eqGateP line 68
11. def OAI.ExactQuantumFactoring.NativeAIG.Emission.eqNextP line 73
12. def OAI.ExactQuantumFactoring.NativeAIG.Emission.eqStateP line 81
13. def OAI.ExactQuantumFactoring.NativeAIG.Emission.eqP line 83