OAI/Computability/DepthThree/MultiTapeMachine.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.DepthThreeLowerBound.(instance at line 12) line 12
  2. theorem OAI.DepthThreeLowerBound.HeadMove.apply_left line 18
  3. theorem OAI.DepthThreeLowerBound.HeadMove.apply_stay line 21
  4. theorem OAI.DepthThreeLowerBound.HeadMove.apply_right line 24
  5. theorem OAI.DepthThreeLowerBound.multiTapeStep_eq_some line 27
  6. theorem OAI.DepthThreeLowerBound.multiTapeStep_eq_none_iff line 34
  7. theorem OAI.DepthThreeLowerBound.FiniteMultiTapeMachine.init_q line 42
  8. theorem OAI.DepthThreeLowerBound.FiniteMultiTapeMachine.init_inputTape line 45
  9. theorem OAI.DepthThreeLowerBound.FiniteMultiTapeMachine.init_otherTape line 49
  10. theorem OAI.DepthThreeLowerBound.multiTapeHaltsIn_iff_runsIn line 56
  11. theorem OAI.DepthThreeLowerBound.MultiTapeHaltsIn.mono line 67
  12. def OAI.DepthThreeLowerBound.MultiTapePolynomialTimeDecider line 73