OAI/Computability/DepthThree/TapeHash.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.TapeHash.State line 11
  2. def OAI.DepthThreeLowerBound.TapeHash.program line 13
  3. def OAI.DepthThreeLowerBound.TapeHash.start line 16
  4. def OAI.DepthThreeLowerBound.TapeHash.done line 17
  5. def OAI.DepthThreeLowerBound.TapeHash.resultStore line 19
  6. theorem OAI.DepthThreeLowerBound.TapeHash.cost_le line 23
  7. theorem OAI.DepthThreeLowerBound.TapeHash.runs_hash line 46
  8. theorem OAI.DepthThreeLowerBound.TapeHash.runs_wordHash line 80
  9. theorem OAI.DepthThreeLowerBound.TapeHash.program_done line 95