OAI/Computability/QuantumFactoring/DescendingFilter.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ExactQuantumFactoring.NetworkEmission.FilterState line 11
2. def OAI.ExactQuantumFactoring.NetworkEmission.filterStep line 15
3. def OAI.ExactQuantumFactoring.NetworkEmission.FilterState.code line 19
4. def OAI.ExactQuantumFactoring.NetworkEmission.filterPrefix line 21
5. lemma OAI.ExactQuantumFactoring.NetworkEmission.filterStep_depth line 25
6. lemma OAI.ExactQuantumFactoring.NetworkEmission.filterRun_depth line 28
7. lemma OAI.ExactQuantumFactoring.NetworkEmission.filterStep_value line 34
8. lemma OAI.ExactQuantumFactoring.NetworkEmission.filterRun_value line 40
9. lemma OAI.ExactQuantumFactoring.NetworkEmission.filterRun_result line 48
10. lemma OAI.ExactQuantumFactoring.NetworkEmission.filterRun_bounds line 61