OAI/Computability/PerfectCompleteness/Machines/FixedStoppedNativeTape.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.FixedStoppedNativeTape.cast_trans_toFun_heq line 19
  2. theorem OAI.PerfectCompleteness.FixedStoppedNativeTape.observeFiber_tape_heq line 34
  3. theorem OAI.PerfectCompleteness.FixedStoppedNativeTape.collapsedRightTape_heq line 52
  4. theorem OAI.PerfectCompleteness.FixedStoppedNativeTape.joinedExterior_heq line 80
  5. abbrev OAI.PerfectCompleteness.FixedStoppedNativeTape.physicalRead line 114
  6. abbrev OAI.PerfectCompleteness.FixedStoppedNativeTape.experimentRead line 117
  7. abbrev OAI.PerfectCompleteness.FixedStoppedNativeTape.rawRead line 120
  8. theorem OAI.PerfectCompleteness.FixedStoppedNativeTape.exterior_heq line 123
  9. theorem OAI.PerfectCompleteness.FixedStoppedNativeTape.physicalRead_tape_heq line 138
  10. theorem OAI.PerfectCompleteness.FixedStoppedNativeTape.experimentTape_heq line 166
  11. theorem OAI.PerfectCompleteness.FixedStoppedNativeTape.rawSample_heq line 189
  12. theorem OAI.PerfectCompleteness.FixedStoppedNativeTape.visible_heq line 207