OAI/Computability/DepthThree/TapeInputGuard.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.TapeInputGuard.positiveResult line 14
  2. def OAI.DepthThreeLowerBound.TapeInputGuard.atLeastResult line 18
  3. def OAI.DepthThreeLowerBound.TapeInputGuard.atMostResult line 22
  4. theorem OAI.DepthThreeLowerBound.TapeInputGuard.positiveResult_result line 26
  5. theorem OAI.DepthThreeLowerBound.TapeInputGuard.atLeastResult_result line 30
  6. theorem OAI.DepthThreeLowerBound.TapeInputGuard.atMostResult_result line 35
  7. inductive OAI.DepthThreeLowerBound.TapeInputGuard.CheckState line 39
  8. def OAI.DepthThreeLowerBound.TapeInputGuard.checkProgram line 47
  9. def OAI.DepthThreeLowerBound.TapeInputGuard.checkStart line 66
  10. theorem OAI.DepthThreeLowerBound.TapeInputGuard.runs_checks line 68
  11. abbrev OAI.DepthThreeLowerBound.TapeInputGuard.TwoState line 122
  12. def OAI.DepthThreeLowerBound.TapeInputGuard.twoProgram line 123
  13. def OAI.DepthThreeLowerBound.TapeInputGuard.twoStart line 125
  14. def OAI.DepthThreeLowerBound.TapeInputGuard.twoDone line 126
  15. theorem OAI.DepthThreeLowerBound.TapeInputGuard.runs_two line 128
  16. abbrev OAI.DepthThreeLowerBound.TapeInputGuard.TestState line 142
  17. def OAI.DepthThreeLowerBound.TapeInputGuard.testProgram line 143
  18. def OAI.DepthThreeLowerBound.TapeInputGuard.testStart line 145
  19. def OAI.DepthThreeLowerBound.TapeInputGuard.testDone line 146
  20. theorem OAI.DepthThreeLowerBound.TapeInputGuard.runs_test line 148
  21. abbrev OAI.DepthThreeLowerBound.TapeInputGuard.State line 166
  22. def OAI.DepthThreeLowerBound.TapeInputGuard.program line 167
  23. def OAI.DepthThreeLowerBound.TapeInputGuard.start line 169
  24. def OAI.DepthThreeLowerBound.TapeInputGuard.done line 170
  25. def OAI.DepthThreeLowerBound.TapeInputGuard.cost line 172
  26. theorem OAI.DepthThreeLowerBound.TapeInputGuard.cost_eq line 174
  27. theorem OAI.DepthThreeLowerBound.TapeInputGuard.cost_le_square line 179
  28. theorem OAI.DepthThreeLowerBound.TapeInputGuard.cost_parameters_le line 185
  29. theorem OAI.DepthThreeLowerBound.TapeInputGuard.runs_guard line 192
  30. theorem OAI.DepthThreeLowerBound.TapeInputGuard.runs_inputFits line 210
  31. theorem OAI.DepthThreeLowerBound.TapeInputGuard.runs_inputFits_quadratic line 233
  32. theorem OAI.DepthThreeLowerBound.TapeInputGuard.program_done line 246