OAI/Computability/QuantumFactoring/BitStackIncrement.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BitStackProgram.binaryValue line 13

    Source documentation

    Little-endian evaluation; leading zeroes at the high end are allowed.

    def binaryValue : List Bool → ℕ
  | [] => 0
  | b::xs => b.toNat+2*binaryValue xs
  2. def OAI.ExactQuantumFactoring.BitStackProgram.incrementWord line 17
  3. def OAI.ExactQuantumFactoring.BitStackProgram.carryTail line 22
  4. def OAI.ExactQuantumFactoring.BitStackProgram.carryCount line 27
  5. lemma OAI.ExactQuantumFactoring.BitStackProgram.incrementWord_value line 32
  6. lemma OAI.ExactQuantumFactoring.BitStackProgram.carryCount_le_length line 36
  7. lemma OAI.ExactQuantumFactoring.BitStackProgram.incrementWord_eq line 40
  8. lemma OAI.ExactQuantumFactoring.BitStackProgram.incrementWord_length line 45
  9. def OAI.ExactQuantumFactoring.BitStackProgram.rippleBody line 51
  10. def OAI.ExactQuantumFactoring.BitStackProgram.ripple line 53
  11. def OAI.ExactQuantumFactoring.BitStackProgram.increment line 54
  12. lemma OAI.ExactQuantumFactoring.BitStackProgram.ripple_runs line 57
  13. lemma OAI.ExactQuantumFactoring.BitStackProgram.increment_runs line 114