OAI/Computability/DepthThree/TapeHorner.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.TapeHorner.State line 10
  2. def OAI.DepthThreeLowerBound.TapeHorner.program line 12
  3. def OAI.DepthThreeLowerBound.TapeHorner.start line 15
  4. def OAI.DepthThreeLowerBound.TapeHorner.done line 16
  5. def OAI.DepthThreeLowerBound.TapeHorner.cost line 18
  6. theorem OAI.DepthThreeLowerBound.TapeHorner.program_done line 21
  7. theorem OAI.DepthThreeLowerBound.TapeHorner.cost_le line 23
  8. theorem OAI.DepthThreeLowerBound.TapeHorner.runs_horner line 29