OAI/Computability/DepthThree/TapeHashInner.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.DepthThreeLowerBound.TapeHashInner.Stateline 12 - def
OAI.DepthThreeLowerBound.TapeHashInner.programline 14 - def
OAI.DepthThreeLowerBound.TapeHashInner.startline 17 - def
OAI.DepthThreeLowerBound.TapeHashInner.doneline 18 - def
OAI.DepthThreeLowerBound.TapeHashInner.progressStoreline 20 - theorem
OAI.DepthThreeLowerBound.TapeHashInner.progress_zeroline 25 - theorem
OAI.DepthThreeLowerBound.TapeHashInner.progress_stepline 31 - theorem
OAI.DepthThreeLowerBound.TapeHashInner.runs_innerline 47 - theorem
OAI.DepthThreeLowerBound.TapeHashInner.program_doneline 89