OAI/Computability/DepthThree/TapeHashStep.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.TapeHashStep.State line 10
  2. def OAI.DepthThreeLowerBound.TapeHashStep.program line 12
  3. def OAI.DepthThreeLowerBound.TapeHashStep.start line 16
  4. def OAI.DepthThreeLowerBound.TapeHashStep.done line 17
  5. def OAI.DepthThreeLowerBound.TapeHashStep.resultStore line 19
  6. theorem OAI.DepthThreeLowerBound.TapeHashStep.runs_step line 24
  7. theorem OAI.DepthThreeLowerBound.TapeHashStep.program_done line 47