OAI/Computability/QuantumFactoring/WordNetworks.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.BitArithmetic.leftWord_append line 15
2. lemma OAI.ExactQuantumFactoring.BitArithmetic.rightWord_append line 17
3. lemma OAI.ExactQuantumFactoring.BitArithmetic.mul_word line 20
4. lemma OAI.ExactQuantumFactoring.BitArithmetic.mod_word line 28
5. lemma OAI.ExactQuantumFactoring.BitArithmetic.add_word line 36
6. lemma OAI.ExactQuantumFactoring.BitArithmetic.bitsValue_append_zero line 44
7. lemma OAI.ExactQuantumFactoring.BitArithmetic.padRight_word line 62
8. lemma OAI.ExactQuantumFactoring.BitArithmetic.bitsValue_take line 66
9. lemma OAI.ExactQuantumFactoring.BitArithmetic.setWidth_toNat_of_le line 75
10. def OAI.ExactQuantumFactoring.BitArithmetic.wordConstant line 81

    Source documentation

    A word of constants uses at most one Boolean node per output bit.

    def wordConstant {n : ℕ} {w : ℕ} (v : BitVec w) : BooleanNetwork n w :=
    …

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

11. lemma OAI.ExactQuantumFactoring.BitArithmetic.wordConstant_eval line 84
12. lemma OAI.ExactQuantumFactoring.BitArithmetic.wordConstant_count line 91