OAI/Computability/DepthThree/TapeDivideFive.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.DepthThreeLowerBound.TapeDivideFive.State line 11
  2. def OAI.DepthThreeLowerBound.TapeDivideFive.nextPhase line 17
  3. def OAI.DepthThreeLowerBound.TapeDivideFive.residue line 20
  4. def OAI.DepthThreeLowerBound.TapeDivideFive.program line 22
  5. theorem OAI.DepthThreeLowerBound.TapeDivideFive.dec_runs line 39
  6. theorem OAI.DepthThreeLowerBound.TapeDivideFive.inc_runs line 50
  7. theorem OAI.DepthThreeLowerBound.TapeDivideFive.runs_phase line 61
  8. theorem OAI.DepthThreeLowerBound.TapeDivideFive.runs_divide line 126
  9. theorem OAI.DepthThreeLowerBound.TapeDivideFive.done_halts line 136