OAI/Computability/DepthThree/TapeHornerBody.lean
11 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.DepthThreeLowerBound.TapeHornerBody.ProductStateline 13 - abbrev
OAI.DepthThreeLowerBound.TapeHornerBody.WorkStateline 14 - abbrev
OAI.DepthThreeLowerBound.TapeHornerBody.Stateline 15 - def
OAI.DepthThreeLowerBound.TapeHornerBody.productline 17 - def
OAI.DepthThreeLowerBound.TapeHornerBody.workline 21 - def
OAI.DepthThreeLowerBound.TapeHornerBody.programline 24 - def
OAI.DepthThreeLowerBound.TapeHornerBody.startline 27 - def
OAI.DepthThreeLowerBound.TapeHornerBody.doneline 28 - def
OAI.DepthThreeLowerBound.TapeHornerBody.costline 30 - theorem
OAI.DepthThreeLowerBound.TapeHornerBody.program_doneline 33 - theorem
OAI.DepthThreeLowerBound.TapeHornerBody.runs_bodyline 35