OAI/Computability/DepthThree/TapeHornerBody.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.TapeHornerBody.ProductState line 13
  2. abbrev OAI.DepthThreeLowerBound.TapeHornerBody.WorkState line 14
  3. abbrev OAI.DepthThreeLowerBound.TapeHornerBody.State line 15
  4. def OAI.DepthThreeLowerBound.TapeHornerBody.product line 17
  5. def OAI.DepthThreeLowerBound.TapeHornerBody.work line 21
  6. def OAI.DepthThreeLowerBound.TapeHornerBody.program line 24
  7. def OAI.DepthThreeLowerBound.TapeHornerBody.start line 27
  8. def OAI.DepthThreeLowerBound.TapeHornerBody.done line 28
  9. def OAI.DepthThreeLowerBound.TapeHornerBody.cost line 30
  10. theorem OAI.DepthThreeLowerBound.TapeHornerBody.program_done line 33
  11. theorem OAI.DepthThreeLowerBound.TapeHornerBody.runs_body line 35