OAI/Computability/DirectedFeedback/Machines/MachineProductProgram.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Explicit.MachineProductProgram.Extra line 16
  2. abbrev OAI.DFVSGames.Explicit.MachineProductProgram.Tape line 17
  3. abbrev OAI.DFVSGames.Explicit.MachineProductProgram.State line 18
  4. def OAI.DFVSGames.Explicit.MachineProductProgram.auxiliary line 20
  5. def OAI.DFVSGames.Explicit.MachineProductProgram.constantDigit line 21
  6. def OAI.DFVSGames.Explicit.MachineProductProgram.accumulator line 22
  7. def OAI.DFVSGames.Explicit.MachineProductProgram.output line 23
  8. def OAI.DFVSGames.Explicit.MachineProductProgram.rowRole line 25
  9. def OAI.DFVSGames.Explicit.MachineProductProgram.decodeRow_inline_MachineProductProgram line 35
  10. theorem OAI.DFVSGames.Explicit.MachineProductProgram.decodeRow_role_inline_MachineProductProgram line 46
  11. def OAI.DFVSGames.Explicit.MachineProductProgram.rowSlots line 55
  12. def OAI.DFVSGames.Explicit.MachineProductProgram.powerRole line 62
  13. theorem OAI.DFVSGames.Explicit.MachineProductProgram.powerRole_injective line 71
  14. def OAI.DFVSGames.Explicit.MachineProductProgram.powerSlots line 83
  15. def OAI.DFVSGames.Explicit.MachineProductProgram.initRole line 86
  16. theorem OAI.DFVSGames.Explicit.MachineProductProgram.initRole_injective line 92
  17. def OAI.DFVSGames.Explicit.MachineProductProgram.seedCommands line 96
  18. def OAI.DFVSGames.Explicit.MachineProductProgram.clearKeys line 99
  19. theorem OAI.DFVSGames.Explicit.MachineProductProgram.mem_clearKeys line 102
  20. inductive OAI.DFVSGames.Explicit.MachineProductProgram.Label line 108
  21. def OAI.DFVSGames.Explicit.MachineProductProgram.headerDestination line 123
  22. def OAI.DFVSGames.Explicit.MachineProductProgram.rowMain line 128
  23. def OAI.DFVSGames.Explicit.MachineProductProgram.nextCheck line 131
  24. def OAI.DFVSGames.Explicit.MachineProductProgram.resetAt line 133
  25. def OAI.DFVSGames.Explicit.MachineProductProgram.headerNext line 135
  26. def OAI.DFVSGames.Explicit.MachineProductProgram.program line 138
  27. def OAI.DFVSGames.Explicit.MachineProductProgram.machine line 164
  28. def OAI.DFVSGames.Explicit.MachineProductHeaders.frame line 186
  29. def OAI.DFVSGames.Explicit.MachineProductHeaders.headerBits line 196
  30. def OAI.DFVSGames.Explicit.MachineProductHeaders.baseTapes line 199
  31. theorem OAI.DFVSGames.Explicit.MachineProductHeaders.frame_accumulator line 202
  32. theorem OAI.DFVSGames.Explicit.MachineProductHeaders.frame_output line 205
  33. theorem OAI.DFVSGames.Explicit.MachineProductHeaders.frame_radix line 208
  34. theorem OAI.DFVSGames.Explicit.MachineProductHeaders.frame_digit line 214
  35. theorem OAI.DFVSGames.Explicit.MachineProductHeaders.power_outside line 219
  36. theorem OAI.DFVSGames.Explicit.MachineProductHeaders.frame_power_clean line 225
  37. theorem OAI.DFVSGames.Explicit.MachineProductHeaders.frame_power_output line 229
  38. theorem OAI.DFVSGames.Explicit.MachineProductHeaders.frame_append line 233
  39. theorem OAI.DFVSGames.Explicit.MachineProductHeaders.initialized_eq line 244
  40. def OAI.DFVSGames.Explicit.MachineProductHeadersRead.inputTapes line 274
  41. def OAI.DFVSGames.Explicit.MachineProductHeadersRead.afterVertices line 278
  42. def OAI.DFVSGames.Explicit.MachineProductHeadersRead.afterAlphabet line 283
  43. def OAI.DFVSGames.Explicit.MachineProductHeadersRead.rawResultTapes line 288
  44. def OAI.DFVSGames.Explicit.MachineProductHeadersRead.resultTapes line 294
  45. theorem OAI.DFVSGames.Explicit.MachineProductHeadersRead.initList_eq line 300
  46. theorem OAI.DFVSGames.Explicit.MachineProductHeadersRead.first_result line 309
  47. theorem OAI.DFVSGames.Explicit.MachineProductHeadersRead.second_result line 322
  48. theorem OAI.DFVSGames.Explicit.MachineProductHeadersRead.third_result line 335
  49. def OAI.DFVSGames.Explicit.MachineProductHeadersRead.rawHeadersInTime line 348
  50. def OAI.DFVSGames.Explicit.MachineProductHeadersRead.headersInTime line 387
  51. theorem OAI.DFVSGames.Explicit.MachineProductHeadersRead.headers_budget line 401
  52. theorem OAI.DFVSGames.Explicit.MachineProductHeaders.seedCommands_nodup line 418
  53. theorem OAI.DFVSGames.Explicit.MachineProductHeaders.seed_result line 424
  54. def OAI.DFVSGames.Explicit.MachineProductHeaders.seedBridge line 452
  55. def OAI.DFVSGames.Explicit.MachineProductHeaders.seedInTime line 469
  56. def OAI.DFVSGames.Explicit.MachineProductHeaders.powerExit line 504
  57. def OAI.DFVSGames.Explicit.MachineProductHeaders.powerInTime line 507
  58. def OAI.DFVSGames.Explicit.MachineProductHeaders.alphabetInTime line 523
  59. def OAI.DFVSGames.Explicit.MachineProductHeaders.powersInTime line 534
  60. def OAI.DFVSGames.Explicit.MachineProductHeaders.initializeInTime line 567
  61. def OAI.DFVSGames.Explicit.MachineProductHeaders.steps line 581
  62. def OAI.DFVSGames.Explicit.MachineProductHeaders.prepareInTime line 586
  63. def OAI.DFVSGames.Explicit.MachineProductHeaders.timePolynomial line 602
  64. theorem OAI.DFVSGames.Explicit.MachineProductHeaders.steps_le line 607
  65. def OAI.DFVSGames.Explicit.MachineProductHeaders.inPolynomialTime line 622
  66. def OAI.DFVSGames.Explicit.MachineProductBounds.fieldPolynomial line 641
  67. theorem OAI.DFVSGames.Explicit.MachineProductBounds.fieldPolynomial_eval line 646
  68. theorem OAI.DFVSGames.Explicit.MachineProductBounds.field_steps_le line 652
  69. def OAI.DFVSGames.Explicit.MachineProductBounds.rowCost line 675
  70. theorem OAI.DFVSGames.Explicit.MachineProductBounds.row_steps_le line 683
  71. structure OAI.DFVSGames.Explicit.MachineProductLoop.BaseReady line 727
  72. def OAI.DFVSGames.Explicit.MachineProductLoop.tupleTapes line 733
  73. theorem OAI.DFVSGames.Explicit.MachineProductLoop.tupleTapes_frame line 738
  74. theorem OAI.DFVSGames.Explicit.MachineProductLoop.tupleTapes_current line 750
  75. theorem OAI.DFVSGames.Explicit.MachineProductLoop.tupleTapes_accumulator line 755
  76. theorem OAI.DFVSGames.Explicit.MachineProductLoop.tupleTapes_ready line 760
  77. def OAI.DFVSGames.Explicit.MachineProductLoop.rowBits line 811
  78. theorem OAI.DFVSGames.Explicit.MachineProductLoop.input_length line 815
  79. def OAI.DFVSGames.Explicit.MachineProductLoop.bodyBound line 821
  80. theorem OAI.DFVSGames.Explicit.MachineProductLoop.bodyTrace line 824
  81. theorem OAI.DFVSGames.Explicit.MachineProductLoop.traversalInTime line 877