OAI/Computability/QuantumFactoring/BitStackAdder.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BitStackProgram.sumBit line 14

    Source documentation

    Literal full-adder truth tables, not an arithmetic oracle.

    def sumBit (a b c : Bool) : Bool := xor a (xor b c)
  2. def OAI.ExactQuantumFactoring.BitStackProgram.carryBit line 15
  3. lemma OAI.ExactQuantumFactoring.BitStackProgram.sum_carry line 17
  4. abbrev OAI.ExactQuantumFactoring.BitStackProgram.AddState line 21
  5. abbrev OAI.ExactQuantumFactoring.BitStackProgram.addStateCode line 22
  6. def OAI.ExactQuantumFactoring.BitStackProgram.addStep line 25
  7. def OAI.ExactQuantumFactoring.BitStackProgram.addMeasure line 30
  8. def OAI.ExactQuantumFactoring.BitStackProgram.residual line 32
  9. def OAI.ExactQuantumFactoring.BitStackProgram.addInvariant line 34
  10. lemma OAI.ExactQuantumFactoring.BitStackProgram.binaryValue_head_tail line 37
  11. lemma OAI.ExactQuantumFactoring.BitStackProgram.addInvariant_step line 41
  12. lemma OAI.ExactQuantumFactoring.BitStackProgram.addMeasure_step line 50
  13. lemma OAI.ExactQuantumFactoring.BitStackProgram.addMeasure_iterate line 61
  14. lemma OAI.ExactQuantumFactoring.BitStackProgram.addInvariant_iterate line 69
  15. lemma OAI.ExactQuantumFactoring.BitStackProgram.residual_zero line 75
  16. def OAI.ExactQuantumFactoring.BitStackProgram.wordAdd line 81
  17. lemma OAI.ExactQuantumFactoring.BitStackProgram.wordAdd_value line 84
  18. lemma OAI.ExactQuantumFactoring.BitStackProgram.addStep_size line 97
  19. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.iterateLinear line 106
  20. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.addStepP line 123
  21. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.wordAddP line 136
  22. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.binaryAdd line 148