OAI/Computability/QuantumFactoring/NativeAIGBounds.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.NativeAIG.DeclBound line 13
2. structure OAI.ExactQuantumFactoring.NativeAIG.Bounded line 17
3. lemma OAI.ExactQuantumFactoring.NativeAIG.DeclBound.mono line 22
4. lemma OAI.ExactQuantumFactoring.NativeAIG.Bounded.mono line 24
5. lemma OAI.ExactQuantumFactoring.NativeAIG.lookup_bound line 27
6. lemma OAI.ExactQuantumFactoring.NativeAIG.addGate_bound line 36
7. lemma OAI.ExactQuantumFactoring.NativeAIG.go_bound line 53
8. lemma OAI.ExactQuantumFactoring.NativeAIG.gate_bound line 79
9. lemma OAI.ExactQuantumFactoring.NativeAIG.orGate_bound line 83
10. lemma OAI.ExactQuantumFactoring.NativeAIG.xorGate_bound line 87
11. lemma OAI.ExactQuantumFactoring.NativeAIG.fullOut_bound line 95
12. lemma OAI.ExactQuantumFactoring.NativeAIG.fullCarry_bound line 100
13. lemma OAI.ExactQuantumFactoring.NativeAIG.full_bound line 107
14. lemma OAI.ExactQuantumFactoring.NativeAIG.nat_bits_length_bound line 114
15. lemma OAI.ExactQuantumFactoring.NativeAIG.refCode_length_bound line 117
16. lemma OAI.ExactQuantumFactoring.NativeAIG.keyCode_length_bound line 121
17. lemma OAI.ExactQuantumFactoring.NativeAIG.declCode_length_bound line 128
18. lemma OAI.ExactQuantumFactoring.NativeAIG.entryCode_length_bound line 139
19. lemma OAI.ExactQuantumFactoring.NativeAIG.listCode_length_bound line 146
20. lemma OAI.ExactQuantumFactoring.NativeAIG.graphCode_length_bound line 149