OAI/Computability/QuantumFactoring/BitStackSubtractor.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitStackProgram.borrowBit line 12
2. lemma OAI.ExactQuantumFactoring.BitStackProgram.difference_borrow line 14
3. lemma OAI.ExactQuantumFactoring.BitStackProgram.binaryValue_lt line 18
4. abbrev OAI.ExactQuantumFactoring.BitStackProgram.SubState line 25
5. abbrev OAI.ExactQuantumFactoring.BitStackProgram.subStateCode line 26
6. def OAI.ExactQuantumFactoring.BitStackProgram.subStep line 28
7. def OAI.ExactQuantumFactoring.BitStackProgram.subInvariant line 33
8. lemma OAI.ExactQuantumFactoring.BitStackProgram.subInvariant_step line 37
9. lemma OAI.ExactQuantumFactoring.BitStackProgram.subInvariant_iterate line 51
10. lemma OAI.ExactQuantumFactoring.BitStackProgram.subStep_tapes line 57
11. def OAI.ExactQuantumFactoring.BitStackProgram.wordSubtract line 66
12. lemma OAI.ExactQuantumFactoring.BitStackProgram.wordSubtract_spec line 70
13. lemma OAI.ExactQuantumFactoring.BitStackProgram.wordSubtract_borrow line 86
14. lemma OAI.ExactQuantumFactoring.BitStackProgram.wordSubtract_value line 97
15. lemma OAI.ExactQuantumFactoring.BitStackProgram.subStep_size line 108