OAI/Computability/DirectedFeedback/Machines/MachineExpanderRowLookup.lean

GitHub source file

145 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseLabel line 57
  2. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.scanPhaseLabel line 61
  3. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.reversePhaseLabel line 64
  4. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.lookupPhasePort line 67
  5. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseAddress line 70
  6. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseAddress_eq_rowIndex line 73
  7. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.lookupTape_injective line 81
  8. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes line 85
  9. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_index line 90
  10. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_work line 98
  11. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_output line 104
  12. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_other line 110
  13. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_table line 117
  14. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_restore line 123
  15. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseTrace line 148
  16. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseInTime line 170
  17. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.reversePhaseTrace line 198
  18. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.reversePhaseInTime line 214
  19. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.reversePhaseTrace_unary line 226
  20. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_zero line 251
  21. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_one line 252
  22. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_two line 253
  23. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_three line 254
  24. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_four line 255
  25. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_five line 256
  26. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes line 260
  27. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.cleanupSteps line 273
  28. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.cleanupSteps_eq_sum line 282
  29. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes_dirty line 286
  30. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes_other line 292
  31. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes_table line 309
  32. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes_inputVertex line 314
  33. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes_output line 319
  34. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.join_trace_inline_MachineExpanderRowCleanup line 324
  35. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.cleanupOneTraceAt line 330
  36. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.cleanupTraceAt line 347
  37. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.doneStepAt line 372
  38. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.cleanupExitTraceAt line 382
  39. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.initializedTapes line 399
  40. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.initializeStepAt line 408
  41. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.clearedQueryTapes line 421
  42. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.clearQueryStepAt line 426
  43. structure OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData line 448
  44. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.rowData line 455
  45. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.control0 line 463
  46. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.firstRow line 464
  47. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.firstValue line 465
  48. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.firstPair line 466
  49. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.firstVertex line 467
  50. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.firstReturn line 468
  51. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.control1 line 469
  52. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.secondRow line 470
  53. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.secondValue line 471
  54. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.secondPair line 472
  55. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.secondVertex line 473
  56. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.secondReturn line 474
  57. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.control2 line 475
  58. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.query1 line 476
  59. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.query2 line 477
  60. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.finalValue line 478
  61. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.tableLength line 479
  62. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.query1_eq_firstRow line 481
  63. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.query2_eq_secondRow line 484
  64. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.firstValue_div_degree line 487
  65. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.firstValue_mod_degree line 488
  66. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.secondValue_div_degree line 489
  67. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.secondValue_mod_degree line 490
  68. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.firstReturn_eq_residue line 492
  69. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.secondReturn_eq_residue line 496
  70. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.receiveFirst_residue_eq_control1 line 500
  71. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.receiveSecond_residue_eq_control2 line 506
  72. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.firstSelected line 512
  73. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.secondSelected line 516
  74. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.evaluateRow_eq line 520
  75. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.finalValue_eq_step_reverseIndex line 523
  76. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.rows_le_tableLength line 530
  77. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.query1_le_tableLength line 534
  78. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.query2_le_tableLength line 538
  79. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.firstValue_le_tableLength line 542
  80. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.secondValue_le_tableLength line 545
  81. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.inputVertex_le_tableLength line 548
  82. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.firstVertex_le_tableLength line 553
  83. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.secondVertex_le_tableLength line 557
  84. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.firstReturn_le_tableLength line 561
  85. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.RowData.secondReturn_le_tableLength line 565
  86. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frameContents line 573
  87. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame0 line 587
  88. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame1 line 589
  89. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame2 line 591
  90. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame3 line 593
  91. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame4 line 596
  92. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame5 line 598
  93. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame6 line 600
  94. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame7 line 602
  95. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame8 line 604
  96. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame9 line 607
  97. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame10 line 609
  98. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame11 line 611
  99. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame12 line 613
  100. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_id_eq_inline_MachineExpanderRowFrames line 616
  101. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame1_eq line 624
  102. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame2_eq line 630
  103. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame3_eq line 636
  104. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame4_eq line 642
  105. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame5_eq line 648
  106. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame6_eq line 656
  107. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame7_eq line 662
  108. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame8_eq line 669
  109. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame9_eq line 676
  110. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame10_eq line 683
  111. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame11_eq line 691
  112. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame12_eq line 699
  113. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.final_frame_eq line 705
  114. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame0_inputVertex line 710
  115. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame0_table line 713
  116. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame0_output line 716
  117. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame1_inputVertex line 719
  118. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame1_emitScratch line 722
  119. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame2_queryReverse line 725
  120. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame2_queryIndex line 728
  121. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame3_table line 731
  122. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame3_lookupRestore line 734
  123. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame3_lookupWork line 737
  124. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame3_lookupOutput line 740
  125. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame3_queryIndex line 743
  126. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame4_lookupOutput line 746
  127. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame4_quotientFirst line 749
  128. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame4_remainderFirst line 752
  129. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame6_quotientFirst line 755
  130. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame6_emitScratch line 758
  131. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame7_queryReverse line 761
  132. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame7_queryIndex line 764
  133. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame8_table line 767
  134. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame8_lookupRestore line 770
  135. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame8_lookupWork line 773
  136. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame8_lookupOutput line 776
  137. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame8_queryIndex line 779
  138. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame9_lookupOutput line 782
  139. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame9_quotientSecond line 785
  140. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame9_remainderSecond line 788
  141. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame10_quotientSecond line 791
  142. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame10_emitScratch line 794
  143. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.frame10_output line 797
  144. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.final_dirty_word_length_le line 800
  145. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.cleanupSteps_le_tableLength line 808