OAI/Computability/QuantumFactoring/NodeStateBounds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.pending_count line 18
2. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.output_count line 19
3. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.bad_count line 20
4. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.old_count line 21
5. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.supplied_count line 22
6. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.nodeInput_count line 23
7. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.top_count line 25
8. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.nextPending_count line 27
9. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.emission_count line 29
10. def OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.outputBound line 32
11. def OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.stepBound line 34
12. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.nextOutput_count line 37
13. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.nextBad_count line 47
14. theorem OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.step_count line 56