OAI/Combinatorics/IndependentSets/Machines/MachineCeilingPower.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.Tape line 16
2. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.(instance at line 20) line 20
3. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.Label line 24
4. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.(instance at line 29) line 29
5. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.Alphabet line 34
6. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.State line 35
7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.memory line 37
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.update_work line 47
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.update_power line 50
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.update_saved line 53
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.update_level line 56
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.update_fuel line 59
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.update_product line 62
14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.compareLoop line 68
15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.scaleLoop line 78
16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.program line 87
17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.overflow line 110
18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.compareStep_zero line 112
19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.compareStep_succ_zero line 122
20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.compareStep_succ_succ line 132
21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.compareTrace line 142
22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.replicate_encodeWord line 167
23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.compareRestoredTrace line 171
24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.appendTrace line 192
25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.scaleStep_succ line 196
26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.scaleStep_zero line 207
27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.scaleScanTrace line 217
28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.scaleTrace line 235
29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.cleanupTrace line 257
30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.guardStep_succ line 268
31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.guardStep_zero line 279
32. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.decideStep line 290
33. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.prefixTime line 302
34. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.prefixTrace line 304
35. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.coreTime line 331
36. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.coreTrace line 336
37. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.roundBudget line 364
38. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.prefixTime_le line 366
39. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.prefixTime_le_roundBudget line 371
40. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.continuingTime_le line 377
41. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.coreTime_le line 385
42. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.initStep line 410
43. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.totalTime line 418
44. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.searchTrace line 420
45. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.timeBound line 440
46. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.totalTime_le line 442
47. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.timePolynomial line 449
48. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.timePolynomial_encoding line 452
49. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.paddingTrace line 456
50. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.paddingInTime line 464
51. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCeilingPower.paddingOutput_bounds line 475