OAI/Computability/QuantumFactoring/PhysicalListSlots.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactQuantumFactoring.PhysicalListSlots.ordinaryWidth line 21
  2. abbrev OAI.ExactQuantumFactoring.PhysicalListSlots.Result line 22
  3. instance OAI.ExactQuantumFactoring.PhysicalListSlots.resultFintype line 24
  4. def OAI.ExactQuantumFactoring.PhysicalListSlots.sampleRead line 26
  5. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.sampleRead_word line 28
  6. def OAI.ExactQuantumFactoring.PhysicalListSlots.ordinary line 32
  7. def OAI.ExactQuantumFactoring.PhysicalListSlots.ordinaryProgram line 35
  8. def OAI.ExactQuantumFactoring.PhysicalListSlots.ordinaryZero line 38
  9. def OAI.ExactQuantumFactoring.PhysicalListSlots.ordinaryState line 41
  10. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.single_normalized line 44
  11. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.ordinary_normalized line 51
  12. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.ordinary_good_mass line 58
  13. def OAI.ExactQuantumFactoring.PhysicalListSlots.fresh line 82
  14. def OAI.ExactQuantumFactoring.PhysicalListSlots.passed line 84
  15. def OAI.ExactQuantumFactoring.PhysicalListSlots.output line 89
  16. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.fresh_normalized line 91
  17. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.passed_mass line 94
  18. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.passed_good line 112
  19. abbrev OAI.ExactQuantumFactoring.PhysicalListSlots.width line 118
  20. def OAI.ExactQuantumFactoring.PhysicalListSlots.layout line 120
  21. def OAI.ExactQuantumFactoring.PhysicalListSlots.program line 121
  22. def OAI.ExactQuantumFactoring.PhysicalListSlots.zero line 123
  23. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.program_entry line 126
  24. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.program_state line 129
  25. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.program_length line 135