OAI/Computability/QuantumFactoring/BitArithmetic.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitArithmetic.binaryInputs line 19

   Source documentation

   The two actual little-endian input words of the bitblaster.

   def binaryInputs (w : ℕ) : AIG.BinaryRefVec (inputs (w+w)).1 w :=
   …

2. def OAI.ExactQuantumFactoring.BitArithmetic.leftWord line 23
3. def OAI.ExactQuantumFactoring.BitArithmetic.rightWord line 25
4. lemma OAI.ExactQuantumFactoring.BitArithmetic.binaryInputs_left line 28
5. lemma OAI.ExactQuantumFactoring.BitArithmetic.binaryInputs_right line 34
6. def OAI.ExactQuantumFactoring.BitArithmetic.add line 40
7. lemma OAI.ExactQuantumFactoring.BitArithmetic.add_correct line 44
8. def OAI.ExactQuantumFactoring.BitArithmetic.mul line 49
9. lemma OAI.ExactQuantumFactoring.BitArithmetic.mul_correct line 53
10. lemma OAI.ExactQuantumFactoring.BitArithmetic.add_count line 58
11. lemma OAI.ExactQuantumFactoring.BitArithmetic.mul_count line 66