OAI/Computability/DepthThree/TapeEvaluation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.DepthThreeLowerBound.TapeEvaluation.Prepared line 13
  2. abbrev OAI.DepthThreeLowerBound.TapeEvaluation.WorkState line 24
  3. abbrev OAI.DepthThreeLowerBound.TapeEvaluation.State line 25
  4. def OAI.DepthThreeLowerBound.TapeEvaluation.work line 27
  5. def OAI.DepthThreeLowerBound.TapeEvaluation.program line 30
  6. def OAI.DepthThreeLowerBound.TapeEvaluation.start line 33
  7. def OAI.DepthThreeLowerBound.TapeEvaluation.done line 34
  8. def OAI.DepthThreeLowerBound.TapeEvaluation.acceptFlag line 36
  9. theorem OAI.DepthThreeLowerBound.TapeEvaluation.acceptFlag_done line 40
  10. theorem OAI.DepthThreeLowerBound.TapeEvaluation.program_done line 41
  11. def OAI.DepthThreeLowerBound.TapeEvaluation.hashWord line 43
  12. def OAI.DepthThreeLowerBound.TapeEvaluation.evaluationWord line 46
  13. def OAI.DepthThreeLowerBound.TapeEvaluation.outputStore line 48
  14. def OAI.DepthThreeLowerBound.TapeEvaluation.cost line 51
  15. theorem OAI.DepthThreeLowerBound.TapeEvaluation.cost_le line 55
  16. theorem OAI.DepthThreeLowerBound.TapeEvaluation.runs_evaluate_cost line 77
  17. theorem OAI.DepthThreeLowerBound.TapeEvaluation.runs_evaluate line 150