OAI/Computability/MinUncut/Machines/RuntimeSpace.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeSpace.configurationLength line 14
2. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeSpace.initial_configurationLength line 17
3. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeSpace.step_configurationLength line 27
4. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeSpace.execution_configurationLength line 36
5. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeSpace.prefix_configurationLength line 44
6. def OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeSpace.spacePolynomial line 51
7. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeSpace.spacePolynomial_eval line 54
8. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeSpace.prefix_length_polynomial line 59
9. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeSpace.totalLength_eq_configurationLength line 67
10. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeSpace.finishCost_le_of_prefix line 73
11. def OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeSpace.completedTime line 89
12. theorem OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeSpace.completedTime_eval line 93
13. def OAI.MinUncutGames.Foundations.Hastad.SourceRuntimeSpace.prefixAndFinishInTime line 100