OAI/Computability/MinUncut/Machines/MachineExpanderFamilyAffine.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.affine_source_ne_scratch line 11
2. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.affine_source_ne_destination line 14
3. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.affine_scratch_ne_destination line 17
4. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes line 20
5. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_other line 27
6. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_source line 33
7. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_scratch line 38
8. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_destination line 43
9. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.affinePhaseBoolTrace line 51
10. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.affinePhaseTrace line 96
11. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.affinePhaseInTime line 111
12. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.copyCountInTime line 124
13. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.multiplySizeInTime line 141
14. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.emitSteps line 165
15. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.affinePlan_bits line 167
16. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.affinePlan_steps line 178
17. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.emittedWord line 185
18. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.emittedWord_target line 189
19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.emittedWord_other line 194
20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.program_firstEmit line 202
21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.program_secondEmit line 208
22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.program_outputEmit line 214
23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.firstEmitTraceAt line 224
24. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.secondEmitTraceAt line 255
25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.outputEmitTraceAt line 286
26. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.firstEmitInTimeAt line 317
27. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.secondEmitInTimeAt line 335
28. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.outputEmitInTimeAt line 353
29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.firstEmitTrace line 373
30. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.secondEmitTrace line 385
31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.outputEmitTrace line 397
32. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.firstEmitInTime line 409
33. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.secondEmitInTime line 421
34. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.outputEmitInTime line 433
35. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseLabel line 449
36. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.scanPhaseLabel line 453
37. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.reversePhaseLabel line 456
38. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.lookupPhasePort line 459
39. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseAddress line 462
40. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseAddress_eq_rowIndex line 465
41. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.lookupTape_injective line 473
42. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes line 477
43. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_index line 482
44. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_work line 490
45. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_output line 496
46. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_other line 502
47. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_table line 509
48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_restore line 515
49. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseTrace line 540
50. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseInTime line 562
51. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.reversePhaseTrace line 590
52. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.reversePhaseInTime line 606
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.reversePhaseTrace_unary line 618
54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_zero line 636
55. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_one line 637
56. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_two line 638
57. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_three line 639
58. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_four line 640
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_five line 641
60. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes line 645
61. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.cleanupSteps line 658
62. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.cleanupSteps_eq_sum line 667
63. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes_dirty line 671
64. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes_other line 677
65. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes_table line 694
66. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes_inputVertex line 699
67. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes_output line 704
68. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.join_trace line 709
69. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.cleanupOneTraceAt line 715
70. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.cleanupTraceAt line 732
71. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.doneStepAt line 757
72. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.cleanupExitTraceAt line 767
73. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.initializedTapes line 784
74. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.initializeStepAt line 793
75. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.clearedQueryTapes line 806
76. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.clearQueryStepAt line 811