OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumUnaryPrefix.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Preserve the unary size bound while calling the given verifier generator. The extra tapes hold only Boolean words; the original machine is embedded without changing any of its instructions.

  1. abbrev OAI.ContinuumCoulomb.QuantumUnaryPrefix.Tape line 17
  2. abbrev OAI.ContinuumCoulomb.QuantumUnaryPrefix.Alphabet line 18
  3. abbrev OAI.ContinuumCoulomb.QuantumUnaryPrefix.Label line 20
  4. abbrev OAI.ContinuumCoulomb.QuantumUnaryPrefix.State line 21
  5. def OAI.ContinuumCoulomb.QuantumUnaryPrefix.program line 23
  6. def OAI.ContinuumCoulomb.QuantumUnaryPrefix.machine line 53
  7. def OAI.ContinuumCoulomb.QuantumUnaryPrefix.extraTapes line 68
  8. def OAI.ContinuumCoulomb.QuantumUnaryPrefix.tapes line 71
  9. def OAI.ContinuumCoulomb.QuantumUnaryPrefix.configuration line 75
  10. def OAI.ContinuumCoulomb.QuantumUnaryPrefix.next line 80
  11. theorem OAI.ContinuumCoulomb.QuantumUnaryPrefix.embedded_program line 83
  12. def OAI.ContinuumCoulomb.QuantumUnaryPrefix.source_execution line 89