OAI/Combinatorics/IndependentSets/Machines/MachineCloudCount.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.Tape line 13
2. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.(instance at line 17) line 17
3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.Alphabet line 21
4. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.State line 22
5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.memory line 24
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.memory_original line 32
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.memory_work line 34
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.memory_target line 36
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.memory_scratch line 38
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.memory_count line 40
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.memory_spare line 42
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.update_memory_work line 45
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.update_memory_target line 49
14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.update_memory_scratch line 53
15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.update_memory_count line 57
16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.finishField line 64
17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.fieldLoop line 67
18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.hit line 80
19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.fieldStep_zero line 82
20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.fieldStep_succ_zero line 99
21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.fieldStep_succ_succ line 115
22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.fieldTrace line 131
23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.replicate_encodeWord line 165
24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.preservingFieldTrace line 169
25. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.preservingFieldInTime line 201
26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.discardFieldsTrace line 221
27. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.Label line 256
28. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.skipLabel line 261
29. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.rowEntry line 264
30. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.program line 270
31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.program_skip line 283
32. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.rowStep_nonempty line 288
33. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.rowStep_empty line 298
34. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.Row line 304
35. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.rowWords line 306
36. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.rowTime line 308
37. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.rowTrace line 311
38. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.rowsHits line 346
39. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.rowsTime line 350
40. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.rowsTrace line 354
41. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.rowTime_le line 378
42. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.rowsTime_le line 387
43. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.inputWord line 397
44. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.inputWord_eq line 400
45. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.inputWord_length line 404
46. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.totalSteps line 411
47. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.countTrace line 414
48. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.totalSteps_le line 449
49. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.tableRows line 458
50. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.tableRows_width line 462
51. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.tableRows_words line 468
52. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.tableRows_input line 475
53. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.rowsHits_eq_filter line 480
54. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.rowList_eq_finRange_map line 487
55. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.rowList_cloud_count line 494
56. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.tableRows_hits line 500
57. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.cloudCountTrace line 506
58. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudCount.cloudCountInTime line 520