OAI/Computability/DirectedFeedback/Games/AddressTupleBody.lean

GitHub source file

145 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Integration.AddressTupleBody.Arena line 58
  2. abbrev OAI.DFVSGames.Integration.AddressTupleBody.Rows line 59
  3. abbrev OAI.DFVSGames.Integration.AddressTupleBody.Slots line 60
  4. abbrev OAI.DFVSGames.Integration.AddressTupleBody.BodyState line 61
  5. abbrev OAI.DFVSGames.Integration.AddressTupleBody.CleanupLabel line 62
  6. abbrev OAI.DFVSGames.Integration.AddressTupleBody.RowLabel line 64
  7. abbrev OAI.DFVSGames.Integration.AddressTupleBody.Label line 66
  8. instance OAI.DFVSGames.Integration.AddressTupleBody.labelFintype line 70
  9. def OAI.DFVSGames.Integration.AddressTupleBody.sourceLabels line 76
  10. def OAI.DFVSGames.Integration.AddressTupleBody.rhsLabel line 78
  11. def OAI.DFVSGames.Integration.AddressTupleBody.rowLabels line 79
  12. def OAI.DFVSGames.Integration.AddressTupleBody.cleanupLabels line 81
  13. def OAI.DFVSGames.Integration.AddressTupleBody.resetLabel line 83
  14. def OAI.DFVSGames.Integration.AddressTupleBody.main line 86
  15. def OAI.DFVSGames.Integration.AddressTupleBody.reset line 88
  16. def OAI.DFVSGames.Integration.AddressTupleBody.instruction line 91
  17. def OAI.DFVSGames.Integration.AddressTupleBody.program line 105
  18. def OAI.DFVSGames.Integration.AddressTupleBody.rhs line 109
  19. def OAI.DFVSGames.Integration.AddressTupleBody.loaded line 112
  20. def OAI.DFVSGames.Integration.AddressTupleBody.tupleBits line 116
  21. def OAI.DFVSGames.Integration.AddressTupleBody.emitted line 121
  22. def OAI.DFVSGames.Integration.AddressTupleBody.finalTapes line 128
  23. structure OAI.DFVSGames.Integration.AddressTupleBody.Ready line 134
  24. def OAI.DFVSGames.Integration.AddressTupleBody.budget line 144
  25. def OAI.DFVSGames.Integration.AddressTupleBody.run line 153
  26. def OAI.DFVSGames.Integration.AddressTupleBody.source line 207
  27. theorem OAI.DFVSGames.Integration.AddressTupleBody.rhs_eq_actual line 210
  28. theorem OAI.DFVSGames.Integration.AddressTupleBody.canonicalValues_eq_actual line 213
  29. theorem OAI.DFVSGames.Integration.AddressTupleBody.tupleBits_actual line 222
  30. theorem OAI.DFVSGames.Integration.AddressTupleBody.actualInvariant line 233
  31. def OAI.DFVSGames.Integration.AddressTupleBody.run_fixed_rows line 255
  32. theorem OAI.DFVSGames.Integration.AddressTupleBody.finalTapes_eq line 276
  33. def OAI.DFVSGames.Integration.AddressTupleBody.run_actual line 284
  34. theorem OAI.DFVSGames.Integration.AddressTupleBody.saved_of_current line 310
  35. abbrev OAI.DFVSGames.Reduction.AddressMachineProgram.Tape line 329
  36. abbrev OAI.DFVSGames.Reduction.AddressMachineProgram.State line 331
  37. def OAI.DFVSGames.Reduction.AddressMachineProgram.accumulator line 335
  38. def OAI.DFVSGames.Reduction.AddressMachineProgram.output line 336
  39. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.accumulator_ne_output line 338
  40. def OAI.DFVSGames.Reduction.AddressMachineProgram.clearKeys line 341
  41. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.mem_clearKeys line 346
  42. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.accumulator_not_mem_clearKeys line 351
  43. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.output_not_mem_clearKeys line 352
  44. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.clearKeys_covers line 354
  45. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.clearKeys_nodup line 357
  46. abbrev OAI.DFVSGames.Reduction.AddressMachineProgram.HeaderLabel line 361
  47. abbrev OAI.DFVSGames.Reduction.AddressMachineProgram.BodyLabel line 362
  48. abbrev OAI.DFVSGames.Reduction.AddressMachineProgram.FinishLabel line 364
  49. inductive OAI.DFVSGames.Reduction.AddressMachineProgram.Label line 366
  50. def OAI.DFVSGames.Reduction.AddressMachineProgram.headerLabels line 376
  51. def OAI.DFVSGames.Reduction.AddressMachineProgram.initializeLabels line 377
  52. def OAI.DFVSGames.Reduction.AddressMachineProgram.bodyLabels line 378
  53. def OAI.DFVSGames.Reduction.AddressMachineProgram.finishLabels line 379
  54. def OAI.DFVSGames.Reduction.AddressMachineProgram.start line 381
  55. def OAI.DFVSGames.Reduction.AddressMachineProgram.initializeStart line 382
  56. def OAI.DFVSGames.Reduction.AddressMachineProgram.bodyStart line 383
  57. def OAI.DFVSGames.Reduction.AddressMachineProgram.checkLabel line 384
  58. def OAI.DFVSGames.Reduction.AddressMachineProgram.resetLabel line 385
  59. def OAI.DFVSGames.Reduction.AddressMachineProgram.finishStart line 386
  60. def OAI.DFVSGames.Reduction.AddressMachineProgram.next line 388
  61. def OAI.DFVSGames.Reduction.AddressMachineProgram.resetAt line 391
  62. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.next_lt line 394
  63. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.next_ge line 396
  64. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.resetAt_lt line 398
  65. def OAI.DFVSGames.Reduction.AddressMachineProgram.program line 401
  66. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.atHeader line 423
  67. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.atInitialize line 427
  68. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.atBody line 432
  69. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.atCheck line 436
  70. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.atReset line 441
  71. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.atFinish line 446
  72. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.finishStartStep line 450
  73. def OAI.DFVSGames.Reduction.AddressMachineProgram.finishStartInTime line 457
  74. def OAI.DFVSGames.Reduction.AddressMachineProgram.machine line 465
  75. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.machine_main line 476
  76. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.machine_program line 477
  77. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.machine_initialState line 478
  78. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.machine_input line 479
  79. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.machine_output line 480
  80. def OAI.DFVSGames.Reduction.AddressMachineProgram.inputAlphabet line 482
  81. def OAI.DFVSGames.Reduction.AddressMachineProgram.outputAlphabet line 483
  82. def OAI.DFVSGames.Reduction.AddressMachineProgram.inputTapes line 485
  83. def OAI.DFVSGames.Reduction.AddressMachineProgram.outputTapes line 488
  84. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.inputTapes_source line 491
  85. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.inputTapes_other line 494
  86. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.outputTapes_output line 497
  87. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.outputTapes_other line 500
  88. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.initList_eq line 503
  89. theorem OAI.DFVSGames.Reduction.AddressMachineProgram.haltList_eq line 515
  90. abbrev OAI.DFVSGames.Reduction.AddressOdometerSchedule.Tape line 542
  91. def OAI.DFVSGames.Reduction.AddressOdometerSchedule.current line 546
  92. def OAI.DFVSGames.Reduction.AddressOdometerSchedule.remaining line 549
  93. def OAI.DFVSGames.Reduction.AddressOdometerSchedule.accumulator line 552
  94. def OAI.DFVSGames.Reduction.AddressOdometerSchedule.currentAt line 555
  95. def OAI.DFVSGames.Reduction.AddressOdometerSchedule.remainingAt line 558
  96. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.current_eq_iff line 561
  97. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.remaining_eq_iff line 564
  98. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.current_ne_remaining line 567
  99. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.remaining_ne_current line 570
  100. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.accumulator_ne_current line 573
  101. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.accumulator_ne_remaining line 576
  102. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.current_ne_accumulator line 579
  103. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.remaining_ne_accumulator line 581
  104. def OAI.DFVSGames.Reduction.AddressOdometerSchedule.setDigits line 584
  105. def OAI.DFVSGames.Reduction.AddressOdometerSchedule.setAcc line 592
  106. def OAI.DFVSGames.Reduction.AddressOdometerSchedule.putDigit line 595
  107. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.setDigits_current line 599
  108. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.setDigits_remaining line 604
  109. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.setDigits_other line 610
  110. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.digitCases_inline_AddressOdometerSchedule line 626
  111. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.setDigits_zero line 638
  112. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.setDigits_accumulator line 646
  113. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.setAcc_self line 650
  114. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.setAcc_setAcc line 652
  115. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.setAcc_apply line 654
  116. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.setDigits_setAcc line 657
  117. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.putDigit_current line 669
  118. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.putDigit_remaining line 674
  119. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.putDigit_other line 680
  120. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.putDigit_accumulator line 686
  121. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.putDigit_setAcc line 691
  122. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.setDigits_putDigit line 703
  123. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.setDigits_snoc line 722
  124. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.setDigits_snoc_base line 755
  125. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.setDigits_savedIndex line 761
  126. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.setAcc_other line 767
  127. def OAI.DFVSGames.Reduction.AddressOdometerSchedule.allBits line 772
  128. def OAI.DFVSGames.Reduction.AddressOdometerSchedule.blockPrefix line 775
  129. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.blockPrefix_eq_ofFn line 779
  130. def OAI.DFVSGames.Reduction.AddressOdometerSchedule.blocks line 788
  131. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.blockPrefix_all line 791
  132. def OAI.DFVSGames.Reduction.AddressOdometerSchedule.configuration line 798
  133. def OAI.DFVSGames.Reduction.AddressOdometerSchedule.BodyTrace line 801
  134. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.val_snoc line 812
  135. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.zeros_snoc line 818
  136. def OAI.DFVSGames.Reduction.AddressOdometerSchedule.initialConfiguration line 823
  137. def OAI.DFVSGames.Reduction.AddressOdometerSchedule.finalConfiguration line 827
  138. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.exists_schedule line 833
  139. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.traversalInTime line 964
  140. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.initial_current line 985
  141. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.initial_remaining line 990
  142. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.final_current line 995
  143. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.final_remaining line 1001
  144. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.final_accumulator line 1007
  145. theorem OAI.DFVSGames.Reduction.AddressOdometerSchedule.final_other line 1014