OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryComparison.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Unary-bounded equality checks for the clock/work registers. A single specified bit may be flipped, as required by the propagation delta.

  1. abbrev OAI.ContinuumCoulomb.QuantumHistoryComparison.Input line 12
  2. def OAI.ContinuumCoulomb.QuantumHistoryComparison.inputCode line 13
  3. def OAI.ContinuumCoulomb.QuantumHistoryComparison.point line 16
  4. def OAI.ContinuumCoulomb.QuantumHistoryComparison.value line 22
  5. theorem OAI.ContinuumCoulomb.QuantumHistoryComparison.value_iff line 24
  6. theorem OAI.ContinuumCoulomb.QuantumHistoryComparison.no_flip_iff line 33
  7. theorem OAI.ContinuumCoulomb.QuantumHistoryComparison.value_equiv_iff line 39
  8. theorem OAI.ContinuumCoulomb.QuantumHistoryComparison.value_flip_iff line 51
  9. abbrev OAI.ContinuumCoulomb.QuantumHistoryComparison.PointInput line 72
  10. def OAI.ContinuumCoulomb.QuantumHistoryComparison.pointCode line 73
  11. opaque OAI.ContinuumCoulomb.QuantumHistoryComparison.countProgram line 75
  12. opaque OAI.ContinuumCoulomb.QuantumHistoryComparison.baseProgram line 76
  13. opaque OAI.ContinuumCoulomb.QuantumHistoryComparison.flipProgram line 78
  14. opaque OAI.ContinuumCoulomb.QuantumHistoryComparison.targetProgram line 80
  15. opaque OAI.ContinuumCoulomb.QuantumHistoryComparison.dataProgram line 83
  16. theorem OAI.ContinuumCoulomb.QuantumHistoryComparison.swap_val line 87
  17. opaque OAI.ContinuumCoulomb.QuantumHistoryComparison.pointProgram line 90
  18. opaque OAI.ContinuumCoulomb.QuantumHistoryComparison.unaryPointProgram line 108
  19. opaque OAI.ContinuumCoulomb.QuantumHistoryComparison.program line 114