OAI/Computability/DepthThree/MachineBasic.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DepthThreeLowerBound.runSteps_zero line 9
  2. theorem OAI.DepthThreeLowerBound.runSteps_succ line 12
  3. theorem OAI.DepthThreeLowerBound.runSteps_succ_left line 16
  4. theorem OAI.DepthThreeLowerBound.runSteps_none line 21
  5. theorem OAI.DepthThreeLowerBound.runSteps_add line 27
  6. theorem OAI.DepthThreeLowerBound.runSteps_succ_eq_of_step_eq line 31
  7. theorem OAI.DepthThreeLowerBound.runSteps_eq_of_step_eq line 37
  8. def OAI.DepthThreeLowerBound.RunsIn line 44
  9. theorem OAI.DepthThreeLowerBound.RunsIn.refl line 47
  10. theorem OAI.DepthThreeLowerBound.RunsIn.single line 51
  11. theorem OAI.DepthThreeLowerBound.RunsIn.mono line 55
  12. theorem OAI.DepthThreeLowerBound.RunsIn.trans line 60
  13. structure OAI.DepthThreeLowerBound.FiniteMachine line 70
  14. def OAI.DepthThreeLowerBound.HaltsIn line 86
  15. def OAI.DepthThreeLowerBound.PolynomialTimeDecider line 92