OAI/Computability/QuantumFactoring/BitStackIntegers.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BitStackProgram.intData line 12
  2. def OAI.ExactQuantumFactoring.BitStackProgram.intCode line 13
  3. def OAI.ExactQuantumFactoring.BitStackProgram.intOfSign line 14
  4. lemma OAI.ExactQuantumFactoring.BitStackProgram.intOfSign_data line 16
  5. lemma OAI.ExactQuantumFactoring.BitStackProgram.intData_ofSign line 23
  6. def OAI.ExactQuantumFactoring.BitStackProgram.signedAdd line 28
  7. lemma OAI.ExactQuantumFactoring.BitStackProgram.signedAdd_value line 32
  8. lemma OAI.ExactQuantumFactoring.BitStackProgram.signedMul_value line 39
  9. lemma OAI.ExactQuantumFactoring.BitStackProgram.intOfSign_not line 44
  10. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.intSign line 49
  11. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.intAbs line 51
  12. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.signedInt line 54
  13. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.natToInt line 64
  14. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.intNeg line 67
  15. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.signedAddP line 73
  16. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.intAdd line 91
  17. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.intSub line 96
  18. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.intMul line 100