OAI/Computability/DepthThree/TapeReadPush.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.DepthThreeLowerBound.TapeReadPush.Stateline 10 - def
OAI.DepthThreeLowerBound.TapeReadPush.programline 12 - def
OAI.DepthThreeLowerBound.TapeReadPush.startline 17 - def
OAI.DepthThreeLowerBound.TapeReadPush.doneline 19 - theorem
OAI.DepthThreeLowerBound.TapeReadPush.runs_read_pushline 21 - theorem
OAI.DepthThreeLowerBound.TapeReadPush.program_doneline 40 - theorem
OAI.DepthThreeLowerBound.TapeReadPush.runs_storeline 44