OAI/Computability/DepthThree/TapePowerSearch.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.TapePowerSearch.Registers line 11
  2. def OAI.DepthThreeLowerBound.TapePowerSearch.candidateStore line 13
  3. def OAI.DepthThreeLowerBound.TapePowerSearch.flag line 16
  4. abbrev OAI.DepthThreeLowerBound.TapePowerSearch.State line 20
  5. def OAI.DepthThreeLowerBound.TapePowerSearch.program line 22
  6. def OAI.DepthThreeLowerBound.TapePowerSearch.start line 28
  7. def OAI.DepthThreeLowerBound.TapePowerSearch.done line 29
  8. def OAI.DepthThreeLowerBound.TapePowerSearch.cost line 31
  9. theorem OAI.DepthThreeLowerBound.TapePowerSearch.runs_test line 36
  10. theorem OAI.DepthThreeLowerBound.TapePowerSearch.runs_search line 57
  11. theorem OAI.DepthThreeLowerBound.TapePowerSearch.program_done line 110
  12. def OAI.DepthThreeLowerBound.TapePowerSearch.continueLt line 113
  13. def OAI.DepthThreeLowerBound.TapePowerSearch.continueLe line 114
  14. theorem OAI.DepthThreeLowerBound.TapePowerSearch.continueLt_result line 116
  15. theorem OAI.DepthThreeLowerBound.TapePowerSearch.continueLe_result line 120
  16. theorem OAI.DepthThreeLowerBound.TapePowerSearch.runs_cube line 128
  17. theorem OAI.DepthThreeLowerBound.TapePowerSearch.runs_sixth_boundary line 147