OAI/Computability/DepthThree/MachineLanguage.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DepthThreeLowerBound.MachineLanguage.decoded_prepared line 12
  2. abbrev OAI.DepthThreeLowerBound.MachineLanguage.BodyState line 28
  3. def OAI.DepthThreeLowerBound.MachineLanguage.bodyProgram line 30
  4. def OAI.DepthThreeLowerBound.MachineLanguage.bodyStart line 33
  5. def OAI.DepthThreeLowerBound.MachineLanguage.bodyDone line 34
  6. theorem OAI.DepthThreeLowerBound.MachineLanguage.bodyProgram_done line 36
  7. theorem OAI.DepthThreeLowerBound.MachineLanguage.runs_body line 39
  8. abbrev OAI.DepthThreeLowerBound.MachineLanguage.State line 55
  9. def OAI.DepthThreeLowerBound.MachineLanguage.program line 57
  10. def OAI.DepthThreeLowerBound.MachineLanguage.start line 60
  11. def OAI.DepthThreeLowerBound.MachineLanguage.acceptFlag line 62
  12. instance OAI.DepthThreeLowerBound.MachineLanguage.stateFintype line 66
  13. def OAI.DepthThreeLowerBound.MachineLanguage.machine line 73
  14. theorem OAI.DepthThreeLowerBound.MachineLanguage.machine_init line 75
  15. theorem OAI.DepthThreeLowerBound.MachineLanguage.halts line 78
  16. theorem OAI.DepthThreeLowerBound.MachineLanguage.cost_le_standard line 112
  17. theorem OAI.DepthThreeLowerBound.MachineLanguage.polynomial_time line 119
  18. theorem OAI.DepthThreeLowerBound.language_polynomial_time line 126