OAI/Computability/QuantumFactoring/BitStackGCD.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitStackProgram.gcdStep line 12
2. def OAI.ExactQuantumFactoring.BitStackProgram.gcdRound line 13
3. lemma OAI.ExactQuantumFactoring.BitStackProgram.gcdStep_value line 15
4. lemma OAI.ExactQuantumFactoring.BitStackProgram.mod_half line 23
5. lemma OAI.ExactQuantumFactoring.BitStackProgram.gcdRound_half line 30
6. lemma OAI.ExactQuantumFactoring.BitStackProgram.gcdRound_value line 40
7. lemma OAI.ExactQuantumFactoring.BitStackProgram.gcdRound_iterate_bound line 43
8. lemma OAI.ExactQuantumFactoring.BitStackProgram.gcdRound_iterate_value line 54
9. lemma OAI.ExactQuantumFactoring.BitStackProgram.gcdRound_result line 60
10. lemma OAI.ExactQuantumFactoring.BitStackProgram.gcdStep_sizeSum line 69
11. lemma OAI.ExactQuantumFactoring.BitStackProgram.gcdRound_iterate_sizeSum line 78