OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumBufferedProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Literal binary TM2 programs for every buffered endpoint path point.

  1. opaque OAI.ContinuumCoulomb.QuantumBufferedCode.uProgram line 12
  2. opaque OAI.ContinuumCoulomb.QuantumBufferedCode.vProgram line 13
  3. opaque OAI.ContinuumCoulomb.QuantumBufferedCode.kProgram line 14
  4. def OAI.ContinuumCoulomb.QuantumBufferedCode.constProgram line 15
  5. opaque OAI.ContinuumCoulomb.QuantumBufferedCode.horizontalProgram line 18
  6. opaque OAI.ContinuumCoulomb.QuantumBufferedCode.verticalProgram line 20
  7. opaque OAI.ContinuumCoulomb.QuantumBufferedCode.doglegCutProgram line 22
  8. opaque OAI.ContinuumCoulomb.QuantumBufferedCode.doglegProgram line 25
  9. opaque OAI.ContinuumCoulomb.QuantumBufferedCode.totalProgram line 35
  10. opaque OAI.ContinuumCoulomb.QuantumBufferedCode.detourCutProgram line 37
  11. opaque OAI.ContinuumCoulomb.QuantumBufferedCode.twiceUProgram line 39
  12. opaque OAI.ContinuumCoulomb.QuantumBufferedCode.detourProgram line 42
  13. def OAI.ContinuumCoulomb.QuantumBufferedCode.doglegCertificate line 57
  14. def OAI.ContinuumCoulomb.QuantumBufferedCode.detourCertificate line 59