OAI/Computability/DepthThree/TapeUnaryCompare.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.DepthThreeLowerBound.TapeUnaryCompare.State line 15
  2. def OAI.DepthThreeLowerBound.TapeUnaryCompare.scanState line 22
  3. def OAI.DepthThreeLowerBound.TapeUnaryCompare.rewindRState line 26
  4. def OAI.DepthThreeLowerBound.TapeUnaryCompare.rewindSState line 30
  5. def OAI.DepthThreeLowerBound.TapeUnaryCompare.mapInstruction line 34
  6. def OAI.DepthThreeLowerBound.TapeUnaryCompare.program line 39
  7. theorem OAI.DepthThreeLowerBound.TapeUnaryCompare.scan_code line 45
  8. theorem OAI.DepthThreeLowerBound.TapeUnaryCompare.rewindR_code line 61
  9. theorem OAI.DepthThreeLowerBound.TapeUnaryCompare.rewindS_code line 70
  10. theorem OAI.DepthThreeLowerBound.TapeUnaryCompare.runs_rewindR line 79
  11. theorem OAI.DepthThreeLowerBound.TapeUnaryCompare.runs_rewindS line 89
  12. theorem OAI.DepthThreeLowerBound.TapeUnaryCompare.runs_compare line 99
  13. theorem OAI.DepthThreeLowerBound.TapeUnaryCompare.runs_compare_linear line 146