OAI/Computability/DepthThree/TapeUnary.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.TapeUnary.counterTape line 11
  2. theorem OAI.DepthThreeLowerBound.TapeUnary.blank_singleton line 13
  3. theorem OAI.DepthThreeLowerBound.TapeUnary.prepend_home line 17
  4. theorem OAI.DepthThreeLowerBound.TapeUnary.remove_home line 21
  5. inductive OAI.DepthThreeLowerBound.TapeUnary.IncState line 29
  6. instance OAI.DepthThreeLowerBound.TapeUnary.(instance at line 35) line 35
  7. def OAI.DepthThreeLowerBound.TapeUnary.incProgram line 41
  8. theorem OAI.DepthThreeLowerBound.TapeUnary.increment_word line 46
  9. theorem OAI.DepthThreeLowerBound.TapeUnary.increment line 67
  10. inductive OAI.DepthThreeLowerBound.TapeUnary.DecState line 74
  11. def OAI.DepthThreeLowerBound.TapeUnary.decProgram line 82
  12. theorem OAI.DepthThreeLowerBound.TapeUnary.decrement_empty line 91
  13. theorem OAI.DepthThreeLowerBound.TapeUnary.decrement_cons line 109
  14. theorem OAI.DepthThreeLowerBound.TapeUnary.decrement line 143