OAI/Computability/QuantumFactoring/BitStackNaturals.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.BitStackProgram.binaryValue_bits line 14
2. lemma OAI.ExactQuantumFactoring.BitStackProgram.incrementWord_bits line 21
3. abbrev OAI.ExactQuantumFactoring.BitStackProgram.unaryCode line 31
4. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.successor line 33
5. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.unarySuccessor line 50
6. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.unaryToBits line 64

   Source documentation

   Unary-to-binary conversion charges every carry and all word moves.

   noncomputable def unaryToBits : Procedure unaryCode Nat.bits id := by
   …

   Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Procedure, OAI.ExactQuantumFactoring.BitStackProgram.unaryCode