OAI/Computability/MinUncut/Games/PoweringInitializeFrame.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra line 12
2. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra_table line 17
3. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra_other line 21
4. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra_scratch line 26
5. def OAI.MinUncutGames.Foundations.Complexity.PoweringInitializeFrame.preparedTapes line 31
6. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringInitializeFrame.prepared_commonRole line 37
7. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringInitializeFrame.prepared_ready line 45
8. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringInitializeFrame.prepared_start line 55
9. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringInitializeFrame.prepared_counter line 62
10. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringInitializeFrame.prepared_output line 69
11. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringInitializeFrame.prepared_vertices line 74
12. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringInitializeFrame.prepared_darts line 77
13. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringInitializeFrame.prepared_source line 81
14. def OAI.MinUncutGames.Foundations.Complexity.PoweringInitializeFrame.preparedCfg line 84
15. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringInitializeFrame.initialGlobalTapes_eq line 89
16. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringInitializeFrame.machine_initialStacks line 104
17. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringInitializeFrame.initList_eq line 110
18. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringInitializeFrame.tableBits_head line 119
19. def OAI.MinUncutGames.Foundations.Complexity.PoweringInitializeFrame.initializeInTime line 123
20. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalConfiguration.placement_injective line 143
21. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalConfiguration.placement_ne_output line 146
22. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalConfiguration.output_ne_placement line 152
23. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_placement line 156
24. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalConfiguration.headerDarts_ne_placement line 162
25. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalConfiguration.placement_ne_headerVertices line 168
26. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalConfiguration.placement_ne_headerDarts line 172
27. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_headerDarts line 176
28. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_output line 179
29. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalConfiguration.headerDarts_ne_output line 182
30. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_scratch line 185
31. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalConfiguration.headerDarts_ne_scratch line 190
32. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalConfiguration.scratch_ne_output line 195
33. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalConfiguration.boolList_mpr_eq line 200
34. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalConfiguration.haltList_tapes line 203
35. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalConfiguration.haltList_eq line 210