OAI/Computability/DepthThree/TapeMultiRoutines.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.DepthThreeLowerBound.runSteps_map_of_someline 9 - theorem
OAI.DepthThreeLowerBound.RunsIn.mapline 31 - def
OAI.DepthThreeLowerBound.TapeMultiProgram.mapCfgline 41 - theorem
OAI.DepthThreeLowerBound.TapeMultiProgram.step_jumpline 44 - theorem
OAI.DepthThreeLowerBound.TapeMultiProgram.step_moveline 51 - theorem
OAI.DepthThreeLowerBound.TapeMultiProgram.step_writeMoveline 67 - theorem
OAI.DepthThreeLowerBound.TapeMultiProgram.step_mapline 84 - theorem
OAI.DepthThreeLowerBound.TapeMultiProgram.runs_mapline 105