OAI/Computability/PerfectCompleteness/Machines/StoppedOwnInputGeometry.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.StoppedOwnInputGeometry.exists_relativePath line 19
  2. def OAI.PerfectCompleteness.StoppedOwnInputGeometry.cutOfBelow line 29
  3. theorem OAI.PerfectCompleteness.StoppedOwnInputGeometry.fullPath_cutOfBelow line 37
  4. theorem OAI.PerfectCompleteness.StoppedOwnInputGeometry.nodeAtLevel_endpoint line 43
  5. theorem OAI.PerfectCompleteness.StoppedOwnInputGeometry.nodeAtLevel_endpoint_spec line 59
  6. def OAI.PerfectCompleteness.StoppedOwnInputGeometry.pathTapeEquiv line 69
  7. theorem OAI.PerfectCompleteness.StoppedOwnInputGeometry.pathTapeEquiv_law line 78
  8. theorem OAI.PerfectCompleteness.StoppedOwnInputGeometry.evaluate_pathTapeEquiv line 87
  9. def OAI.PerfectCompleteness.StoppedOwnInputGeometry.lowerLevel line 99
  10. def OAI.PerfectCompleteness.StoppedOwnInputGeometry.upperNode line 102
  11. def OAI.PerfectCompleteness.StoppedOwnInputGeometry.lowerNode line 107
  12. theorem OAI.PerfectCompleteness.StoppedOwnInputGeometry.upperNode_height line 112
  13. theorem OAI.PerfectCompleteness.StoppedOwnInputGeometry.lowerNode_height line 118
  14. def OAI.PerfectCompleteness.StoppedOwnInputGeometry.ownCut line 124
  15. theorem OAI.PerfectCompleteness.StoppedOwnInputGeometry.lowerNode_path_spec line 133
  16. theorem OAI.PerfectCompleteness.StoppedOwnInputGeometry.fullPath_spec line 142
  17. theorem OAI.PerfectCompleteness.StoppedOwnInputGeometry.arrayLaw_eq line 162
  18. def OAI.PerfectCompleteness.StoppedOwnInputGeometry.tapeEquiv line 175
  19. theorem OAI.PerfectCompleteness.StoppedOwnInputGeometry.tapeEquiv_law line 186
  20. theorem OAI.PerfectCompleteness.StoppedOwnInputGeometry.evaluate_tapeEquiv line 199
  21. theorem OAI.PerfectCompleteness.StoppedOwnInputGeometry.exposedRead_law line 215