OAI/Computability/DepthThree/TapeInitialization.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.DepthThreeLowerBound.InitState line 13
  2. instance OAI.DepthThreeLowerBound.(instance at line 22) line 22
  3. def OAI.DepthThreeLowerBound.initActive line 28
  4. instance OAI.DepthThreeLowerBound.(instance at line 31) line 31
  5. def OAI.DepthThreeLowerBound.initializationCode line 34
  6. def OAI.DepthThreeLowerBound.rawInputTapes line 55
  7. def OAI.DepthThreeLowerBound.initializedTapes line 58
  8. theorem OAI.DepthThreeLowerBound.initializedTapes_input line 63
  9. theorem OAI.DepthThreeLowerBound.initializedTapes_length line 67
  10. theorem OAI.DepthThreeLowerBound.initializedTapes_other line 72
  11. theorem OAI.DepthThreeLowerBound.initializedTapes_head line 77
  12. theorem OAI.DepthThreeLowerBound.init_step line 82
  13. theorem OAI.DepthThreeLowerBound.init_raw_left line 95
  14. theorem OAI.DepthThreeLowerBound.init_write_nil line 99
  15. def OAI.DepthThreeLowerBound.initHomeTapes line 102
  16. def OAI.DepthThreeLowerBound.initScanTapes line 105
  17. def OAI.DepthThreeLowerBound.initRewindTapes line 112
  18. theorem OAI.DepthThreeLowerBound.initialization_start line 121
  19. theorem OAI.DepthThreeLowerBound.initialization_home line 128
  20. theorem OAI.DepthThreeLowerBound.initialization_prepare line 138
  21. theorem OAI.DepthThreeLowerBound.initialization_scan_bit line 152
  22. theorem OAI.DepthThreeLowerBound.initialization_scan_end line 168
  23. theorem OAI.DepthThreeLowerBound.initRewind_head_ne_home line 183
  24. theorem OAI.DepthThreeLowerBound.initialization_rewind_bit line 187
  25. theorem OAI.DepthThreeLowerBound.initialization_rewind_home line 204
  26. theorem OAI.DepthThreeLowerBound.initialization_finish line 223
  27. theorem OAI.DepthThreeLowerBound.initialization_scan_runs line 231
  28. theorem OAI.DepthThreeLowerBound.initialization_rewind_runs line 244
  29. theorem OAI.DepthThreeLowerBound.initialization_runs line 255
  30. theorem OAI.DepthThreeLowerBound.initialization_done line 270
  31. def OAI.DepthThreeLowerBound.initializationMachine line 273
  32. theorem OAI.DepthThreeLowerBound.initializationMachine_init line 276
  33. theorem OAI.DepthThreeLowerBound.initializationMachine_halts line 279