OAI/Computability/PerfectCompleteness/Foundations/StoppedProjectedExperiment.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.StoppedProjectedExperiment.below_append line 22
  2. abbrev OAI.PerfectCompleteness.StoppedProjectedExperiment.Outer line 32
  3. abbrev OAI.PerfectCompleteness.StoppedProjectedExperiment.Inner line 35
  4. def OAI.PerfectCompleteness.StoppedProjectedExperiment.outerLaw line 40
  5. def OAI.PerfectCompleteness.StoppedProjectedExperiment.innerLaw line 45
  6. abbrev OAI.PerfectCompleteness.StoppedProjectedExperiment.nativeSlots line 56
  7. def OAI.PerfectCompleteness.StoppedProjectedExperiment.upperPath line 59
  8. def OAI.PerfectCompleteness.StoppedProjectedExperiment.lowerPath line 62
  9. def OAI.PerfectCompleteness.StoppedProjectedExperiment.stoppedPath line 65
  10. def OAI.PerfectCompleteness.StoppedProjectedExperiment.upper line 69
  11. def OAI.PerfectCompleteness.StoppedProjectedExperiment.lower line 72
  12. theorem OAI.PerfectCompleteness.StoppedProjectedExperiment.upper_height line 76
  13. theorem OAI.PerfectCompleteness.StoppedProjectedExperiment.lower_height line 80
  14. def OAI.PerfectCompleteness.StoppedProjectedExperiment.cut line 85
  15. theorem OAI.PerfectCompleteness.StoppedProjectedExperiment.fullPath_spec line 90
  16. def OAI.PerfectCompleteness.StoppedProjectedExperiment.cutQuestions line 106
  17. def OAI.PerfectCompleteness.StoppedProjectedExperiment.projectedSlots line 111
  18. theorem OAI.PerfectCompleteness.StoppedProjectedExperiment.fill_native line 118
  19. def OAI.PerfectCompleteness.StoppedProjectedExperiment.projection line 125
  20. def OAI.PerfectCompleteness.StoppedProjectedExperiment.direction line 138
  21. abbrev OAI.PerfectCompleteness.StoppedProjectedExperiment.experiment line 149
  22. abbrev OAI.PerfectCompleteness.StoppedProjectedExperiment.TapeSample line 156
  23. def OAI.PerfectCompleteness.StoppedProjectedExperiment.tapeLaw line 161
  24. def OAI.PerfectCompleteness.StoppedProjectedExperiment.tapeRead line 167
  25. theorem OAI.PerfectCompleteness.StoppedProjectedExperiment.tapeRead_law line 176
  26. theorem OAI.PerfectCompleteness.StoppedProjectedExperiment.arrays_tapeRead line 205
  27. abbrev OAI.PerfectCompleteness.StoppedProjectedExperiment.PhysicalBase line 223
  28. def OAI.PerfectCompleteness.StoppedProjectedExperiment.withFlags line 228
  29. def OAI.PerfectCompleteness.StoppedProjectedExperiment.physicalBaseLaw line 233
  30. abbrev OAI.PerfectCompleteness.StoppedProjectedExperiment.baseTag line 239
  31. def OAI.PerfectCompleteness.StoppedProjectedExperiment.physicalSources line 242
  32. abbrev OAI.PerfectCompleteness.StoppedProjectedExperiment.PhysicalRaw line 247
  33. abbrev OAI.PerfectCompleteness.StoppedProjectedExperiment.PhysicalSample line 254
  34. def OAI.PerfectCompleteness.StoppedProjectedExperiment.physicalFiberLaw line 258
  35. def OAI.PerfectCompleteness.StoppedProjectedExperiment.physicalLaw line 266
  36. def OAI.PerfectCompleteness.StoppedProjectedExperiment.physicalRead line 271
  37. theorem OAI.PerfectCompleteness.StoppedProjectedExperiment.physicalFiber_probability line 281
  38. theorem OAI.PerfectCompleteness.StoppedProjectedExperiment.physicalRead_law line 324
  39. def OAI.PerfectCompleteness.StoppedProjectedExperiment.physicalExperimentRead line 353
  40. theorem OAI.PerfectCompleteness.StoppedProjectedExperiment.physicalExperimentRead_law line 360