OAI/Computability/DepthThree/TapeMultiProgram.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.TapeHeads line 13
  2. abbrev OAI.DepthThreeLowerBound.TapeMoves line 14
  3. abbrev OAI.DepthThreeLowerBound.TapeTapes line 15
  4. abbrev OAI.DepthThreeLowerBound.TapeMultiCfg line 16
  5. abbrev OAI.DepthThreeLowerBound.TapeMultiProgram line 17
  6. def OAI.DepthThreeLowerBound.wordTape line 20
  7. def OAI.DepthThreeLowerBound.cursorTape line 23
  8. theorem OAI.DepthThreeLowerBound.wordTape_head line 27
  9. theorem OAI.DepthThreeLowerBound.cursorTape_head_cons line 30
  10. theorem OAI.DepthThreeLowerBound.cursorTape_head_nil line 33
  11. theorem OAI.DepthThreeLowerBound.wordTape_right line 36
  12. theorem OAI.DepthThreeLowerBound.cursorTape_right line 39
  13. def OAI.DepthThreeLowerBound.TapeMultiProgram.step line 48
  14. def OAI.DepthThreeLowerBound.TapeMultiProgram.cfg line 51
  15. def OAI.DepthThreeLowerBound.TapeMultiProgram.heads line 53
  16. def OAI.DepthThreeLowerBound.TapeMultiProgram.stayMoves line 55
  17. def OAI.DepthThreeLowerBound.TapeMultiProgram.moveOnly line 57
  18. def OAI.DepthThreeLowerBound.TapeMultiProgram.writeOnly line 60
  19. def OAI.DepthThreeLowerBound.TapeMultiProgram.jump line 63
  20. def OAI.DepthThreeLowerBound.TapeMultiProgram.move line 66
  21. def OAI.DepthThreeLowerBound.TapeMultiProgram.writeMove line 69
  22. def OAI.DepthThreeLowerBound.TapeMultiProgram.isAtom line 74
  23. def OAI.DepthThreeLowerBound.TapeMultiProgram.machine line 77