OAI/Computability/QuantumFactoring/BitStackDivision.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.conditional line 15
  2. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.binaryZero line 20
  3. abbrev OAI.ExactQuantumFactoring.BitStackProgram.DivState line 33
  4. abbrev OAI.ExactQuantumFactoring.BitStackProgram.divStateCode line 34
  5. def OAI.ExactQuantumFactoring.BitStackProgram.divStep line 36
  6. lemma OAI.ExactQuantumFactoring.BitStackProgram.divStep_fst line 40
  7. lemma OAI.ExactQuantumFactoring.BitStackProgram.divStep_size line 43
  8. lemma OAI.ExactQuantumFactoring.BitStackProgram.divStep_spec line 56
  9. lemma OAI.ExactQuantumFactoring.BitStackProgram.div_fold_spec line 71
  10. def OAI.ExactQuantumFactoring.BitStackProgram.divideRaw line 89
  11. lemma OAI.ExactQuantumFactoring.BitStackProgram.divideRaw_spec line 92
  12. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.divStepP line 105
  13. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.divideRawP line 120
  14. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.binaryDivMod line 129
  15. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.binaryDiv line 142
  16. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.binaryMod line 144