OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumTermTime.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Assign every actual history term to its clock time and enumerate by time.

  1. def OAI.ContinuumCoulomb.qmaBoundedClockTime line 11
  2. theorem OAI.ContinuumCoulomb.qmaBoundedClockTime_eq line 14
  3. def OAI.ContinuumCoulomb.qmaHistoryTermTime line 20
  4. def OAI.ContinuumCoulomb.qmaHistoryTermList line 28
  5. theorem OAI.ContinuumCoulomb.qmaHistoryTermList_mem line 31
  6. theorem OAI.ContinuumCoulomb.qmaHistoryTermList_nodup line 36
  7. def OAI.ContinuumCoulomb.qmaOrderedHistoryTerms line 39
  8. theorem OAI.ContinuumCoulomb.qmaOrderedHistoryTerms_mem line 43
  9. theorem OAI.ContinuumCoulomb.qmaOrderedHistoryTerms_nodup line 48
  10. theorem OAI.ContinuumCoulomb.qmaOrderedHistoryTerms_length line 53
  11. theorem OAI.ContinuumCoulomb.qmaOrderedHistoryTerms_sorted line 59