OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumBitTransfer.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Transfer a bit-coded word between the verifier machine and the Boolean prefix tapes. Only the bit register is added to the finite control.

  1. def OAI.ContinuumCoulomb.QuantumBitTransfer.loop line 14
  2. theorem OAI.ContinuumCoulomb.QuantumBitTransfer.update_src line 21
  3. theorem OAI.ContinuumCoulomb.QuantumBitTransfer.update_dst line 33
  4. theorem OAI.ContinuumCoulomb.QuantumBitTransfer.step_empty line 42
  5. theorem OAI.ContinuumCoulomb.QuantumBitTransfer.step_cons line 53
  6. theorem OAI.ContinuumCoulomb.QuantumBitTransfer.transfer_steps line 66
  7. def OAI.ContinuumCoulomb.QuantumBitTransfer.transfer line 89