OAI/Computability/DepthThree/TapeHornerTake.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.TapeHornerTake.registers line 10
  2. abbrev OAI.DepthThreeLowerBound.TapeHornerTake.PrepareState line 19
  3. abbrev OAI.DepthThreeLowerBound.TapeHornerTake.WorkState line 20
  4. abbrev OAI.DepthThreeLowerBound.TapeHornerTake.State line 21
  5. def OAI.DepthThreeLowerBound.TapeHornerTake.prepare line 23
  6. def OAI.DepthThreeLowerBound.TapeHornerTake.work line 27
  7. def OAI.DepthThreeLowerBound.TapeHornerTake.program line 30
  8. def OAI.DepthThreeLowerBound.TapeHornerTake.start line 33
  9. def OAI.DepthThreeLowerBound.TapeHornerTake.done line 34
  10. theorem OAI.DepthThreeLowerBound.TapeHornerTake.program_done line 36
  11. theorem OAI.DepthThreeLowerBound.TapeHornerTake.runs_take line 38