OAI/Computability/DirectedFeedback/Machines/MachineSubdivisionInit.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Explicit.MachineSubdivisionInit.source_ne_scratch line 14
  2. theorem OAI.DFVSGames.Explicit.MachineSubdivisionInit.source_ne_destination line 17
  3. theorem OAI.DFVSGames.Explicit.MachineSubdivisionInit.scratch_ne_destination line 20
  4. def OAI.DFVSGames.Explicit.MachineSubdivisionInit.priorWord line 23
  5. theorem OAI.DFVSGames.Explicit.MachineSubdivisionInit.operationTrace line 28
  6. def OAI.DFVSGames.Explicit.MachineSubdivisionInit.sourceValue line 76
  7. def OAI.DFVSGames.Explicit.MachineSubdivisionInit.beforeValue line 87
  8. def OAI.DFVSGames.Explicit.MachineSubdivisionInit.afterValue line 98
  9. def OAI.DFVSGames.Explicit.MachineSubdivisionInit.frame line 101
  10. theorem OAI.DFVSGames.Explicit.MachineSubdivisionInit.frame_source line 108
  11. theorem OAI.DFVSGames.Explicit.MachineSubdivisionInit.frame_scratch line 113
  12. theorem OAI.DFVSGames.Explicit.MachineSubdivisionInit.frame_destination line 117
  13. def OAI.DFVSGames.Explicit.MachineSubdivisionInit.atStage line 123
  14. theorem OAI.DFVSGames.Explicit.MachineSubdivisionInit.initNext_eq_atStage line 127
  15. def OAI.DFVSGames.Explicit.MachineSubdivisionInit.stageCost line 131
  16. theorem OAI.DFVSGames.Explicit.MachineSubdivisionInit.sourceValue_le line 133
  17. def OAI.DFVSGames.Explicit.MachineSubdivisionInit.prefixInTime line 136
  18. def OAI.DFVSGames.Explicit.MachineSubdivisionInit.resultTapes line 179
  19. theorem OAI.DFVSGames.Explicit.MachineSubdivisionInit.final_frame line 193
  20. def OAI.DFVSGames.Explicit.MachineSubdivisionInit.initializeInTime line 201
  21. def OAI.DFVSGames.Explicit.MachineSubdivisionEmission.headerBits line 220
  22. def OAI.DFVSGames.Explicit.MachineSubdivisionEmission.resultTapes line 222
  23. theorem OAI.DFVSGames.Explicit.MachineSubdivisionEmission.header_template line 226
  24. theorem OAI.DFVSGames.Explicit.MachineSubdivisionEmission.header_copiedLength line 234
  25. theorem OAI.DFVSGames.Explicit.MachineSubdivisionEmission.header_result line 242
  26. def OAI.DFVSGames.Explicit.MachineSubdivisionEmission.headerInTime line 248
  27. def OAI.DFVSGames.Explicit.MachineSubdivisionEmission.prepareInTime line 266
  28. theorem OAI.DFVSGames.Reduction.GameEncodingSize.tableBits_length_le line 290
  29. theorem OAI.DFVSGames.Reduction.GameEncodingSize.constraintBits_length_le line 299
  30. theorem OAI.DFVSGames.Reduction.GameEncodingSize.constraintsBits_length_le line 308
  31. theorem OAI.DFVSGames.Reduction.GameEncodingSize.gameBits_length_le line 319
  32. def OAI.DFVSGames.Explicit.MachineSubdivisionTableRead.tapes line 338
  33. theorem OAI.DFVSGames.Explicit.MachineSubdivisionTableRead.tapes_input line 341
  34. theorem OAI.DFVSGames.Explicit.MachineSubdivisionTableRead.tapes_reverse line 344
  35. theorem OAI.DFVSGames.Explicit.MachineSubdivisionTableRead.update_input_inline_MachineSubdivisionTableRead line 347
  36. theorem OAI.DFVSGames.Explicit.MachineSubdivisionTableRead.update_reverse_inline_MachineSubdivisionTableRead line 353
  37. theorem OAI.DFVSGames.Explicit.MachineSubdivisionTableRead.step_true line 359
  38. theorem OAI.DFVSGames.Explicit.MachineSubdivisionTableRead.step_false line 369
  39. theorem OAI.DFVSGames.Explicit.MachineSubdivisionTableRead.readWordTrace line 379
  40. theorem OAI.DFVSGames.Explicit.MachineSubdivisionTableRead.readWordsTrace line 400
  41. def OAI.DFVSGames.Explicit.MachineSubdivisionTableRead.finalTapes line 430
  42. theorem OAI.DFVSGames.Explicit.MachineSubdivisionTableRead.finalTapes_other line 433
  43. theorem OAI.DFVSGames.Explicit.MachineSubdivisionTableRead.finalTapes_input line 438
  44. theorem OAI.DFVSGames.Explicit.MachineSubdivisionTableRead.finalTapes_reverse line 441
  45. theorem OAI.DFVSGames.Explicit.MachineSubdivisionTableRead.finalTapes_permutation line 444
  46. theorem OAI.DFVSGames.Explicit.MachineSubdivisionTableRead.tableTrace line 447
  47. def OAI.DFVSGames.Explicit.MachineSubdivisionTableRead.tableInTime line 474
  48. def OAI.DFVSGames.Explicit.MachineSubdivisionBody.tableBits line 501
  49. structure OAI.DFVSGames.Explicit.MachineSubdivisionBody.Ready line 504
  50. def OAI.DFVSGames.Explicit.MachineSubdivisionBody.afterU line 513
  51. def OAI.DFVSGames.Explicit.MachineSubdivisionBody.afterV line 517
  52. def OAI.DFVSGames.Explicit.MachineSubdivisionBody.afterTable line 521
  53. def OAI.DFVSGames.Explicit.MachineSubdivisionBody.rowPayload line 525
  54. def OAI.DFVSGames.Explicit.MachineSubdivisionBody.afterRows line 530
  55. def OAI.DFVSGames.Explicit.MachineSubdivisionBody.afterDrainU line 535
  56. def OAI.DFVSGames.Explicit.MachineSubdivisionBody.afterDrainV line 539
  57. def OAI.DFVSGames.Explicit.MachineSubdivisionBody.afterDrainTable line 543
  58. def OAI.DFVSGames.Explicit.MachineSubdivisionBody.incrementTapes line 547
  59. def OAI.DFVSGames.Explicit.MachineSubdivisionBody.bodyResult line 553
  60. def OAI.DFVSGames.Explicit.MachineSubdivisionBody.bodyBudget line 557
  61. theorem OAI.DFVSGames.Explicit.MachineSubdivisionBody.rowField_ne_scratch_inline_MachineSubdivisionBody line 566
  62. theorem OAI.DFVSGames.Explicit.MachineSubdivisionBody.rowField_ne_accumulator_inline_MachineSubdivisionBody line 569
  63. def OAI.DFVSGames.Explicit.MachineSubdivisionBody.incrementInTime line 572
  64. def OAI.DFVSGames.Explicit.MachineSubdivisionBody.bodyInTime line 582
  65. def OAI.DFVSGames.Explicit.MachineSubdivisionLoopFrame.bodyBits line 657
  66. theorem OAI.DFVSGames.Explicit.MachineSubdivisionLoopFrame.bodyBits_nil line 660
  67. theorem OAI.DFVSGames.Explicit.MachineSubdivisionLoopFrame.bodyBits_cons line 662
  68. def OAI.DFVSGames.Explicit.MachineSubdivisionLoopFrame.identityBits line 669
  69. def OAI.DFVSGames.Explicit.MachineSubdivisionLoopFrame.rowBits line 672
  70. def OAI.DFVSGames.Explicit.MachineSubdivisionLoopFrame.outputRows line 679
  71. def OAI.DFVSGames.Explicit.MachineSubdivisionLoopFrame.frame line 683
  72. def OAI.DFVSGames.Explicit.MachineSubdivisionLoopFrame.afterGuard line 694
  73. theorem OAI.DFVSGames.Explicit.MachineSubdivisionLoopFrame.frame_prepared line 698
  74. theorem OAI.DFVSGames.Explicit.MachineSubdivisionLoopFrame.guard_cons line 705
  75. theorem OAI.DFVSGames.Explicit.MachineSubdivisionLoopFrame.guard_nil line 726
  76. theorem OAI.DFVSGames.Explicit.MachineSubdivisionLoopFrame.ready line 743
  77. def OAI.DFVSGames.Explicit.MachineSubdivisionBodySpec.resultTapes line 767
  78. theorem OAI.DFVSGames.Explicit.MachineSubdivisionBodySpec.bodyResult_eq line 777
  79. theorem OAI.DFVSGames.Explicit.MachineSubdivisionBodySpec.result_input line 787
  80. theorem OAI.DFVSGames.Explicit.MachineSubdivisionBodySpec.result_locals line 794
  81. theorem OAI.DFVSGames.Explicit.MachineSubdivisionBodySpec.result_accumulator line 805
  82. theorem OAI.DFVSGames.Explicit.MachineSubdivisionBodySpec.encodeWord_succ line 813
  83. theorem OAI.DFVSGames.Explicit.MachineSubdivisionBodySpec.result_indices line 816
  84. def OAI.DFVSGames.Explicit.MachineSubdivisionBodySpec.rowBits line 831
  85. theorem OAI.DFVSGames.Explicit.MachineSubdivisionBodySpec.rowPayload_eq line 839
  86. theorem OAI.DFVSGames.Explicit.MachineSubdivisionBodySpec.rowBits_eq_dynamic line 852
  87. theorem OAI.DFVSGames.Explicit.MachineSubdivisionBodySpec.bodyBudget_le line 859