OAI/Computability/DirectedFeedback/Machines/MachineSubdivisionRows.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Explicit.MachineSubdivisionRows.identityTable line 15
  2. def OAI.DFVSGames.Explicit.MachineSubdivisionRows.inverseTable line 21
  3. def OAI.DFVSGames.Explicit.MachineSubdivisionRows.rows line 27
  4. theorem OAI.DFVSGames.Explicit.MachineSubdivisionRows.rows_length line 34
  5. def OAI.DFVSGames.Explicit.MachineSubdivisionRows.tokens line 38
  6. theorem OAI.DFVSGames.Explicit.MachineSubdivisionRows.tokens_length line 44
  7. def OAI.DFVSGames.Explicit.MachineSubdivisionRows.fields line 47
  8. def OAI.DFVSGames.Explicit.MachineSubdivisionRows.rowBits line 50
  9. theorem OAI.DFVSGames.Explicit.MachineSubdivisionRows.templateOutput_rows line 53
  10. def OAI.DFVSGames.Explicit.MachineSubdivisionRows.field line 62
  11. def OAI.DFVSGames.Explicit.MachineSubdivisionRows.scratch line 64
  12. def OAI.DFVSGames.Explicit.MachineSubdivisionRows.output line 65
  13. theorem OAI.DFVSGames.Explicit.MachineSubdivisionRows.field_ne_scratch line 67
  14. theorem OAI.DFVSGames.Explicit.MachineSubdivisionRows.field_ne_output line 73
  15. theorem OAI.DFVSGames.Explicit.MachineSubdivisionRows.scratch_ne_output line 79
  16. def OAI.DFVSGames.Explicit.MachineSubdivisionRows.machine line 81
  17. theorem OAI.DFVSGames.Explicit.MachineSubdivisionRows.machine_finiteAlphabet line 92
  18. def OAI.DFVSGames.Explicit.MachineSubdivisionRows.phaseInTime line 98
  19. theorem OAI.DFVSGames.Explicit.MachineSubdivisionRows.phase_budget line 113
  20. def OAI.DFVSGames.Explicit.MachineSubdivisionRows.subdivisionVertexWords line 122
  21. theorem OAI.DFVSGames.Explicit.MachineSubdivisionRows.subdivisionVertexWords_bounded line 129
  22. def OAI.DFVSGames.Reduction.Encoding.sideEquiv line 142
  23. theorem OAI.DFVSGames.Reduction.Encoding.sideEquiv_false_val line 145
  24. theorem OAI.DFVSGames.Reduction.Encoding.sideEquiv_true_val line 148
  25. def OAI.DFVSGames.Reduction.Encoding.alphabetEquiv line 151
  26. theorem OAI.DFVSGames.Reduction.Encoding.alphabetEquiv_symm_apply_apply line 158
  27. theorem OAI.DFVSGames.Reduction.Encoding.alphabetEquiv_apply_symm_apply line 163
  28. def OAI.DFVSGames.Reduction.Encoding.translate line 167
  29. theorem OAI.DFVSGames.Reduction.Encoding.translate_involutive line 171
  30. def OAI.DFVSGames.Reduction.Encoding.translationTable line 183
  31. theorem OAI.DFVSGames.Reduction.Encoding.translationTable_images line 190
  32. theorem OAI.DFVSGames.Reduction.Encoding.translationTable_inverseImages line 195
  33. theorem OAI.DFVSGames.Reduction.Encoding.translationTable_satisfied_iff line 201
  34. def OAI.DFVSGames.Reduction.Encoding.imageVertices line 211
  35. theorem OAI.DFVSGames.Reduction.Encoding.mem_imageVertices line 214
  36. theorem OAI.DFVSGames.Reduction.Encoding.imageVertices_nodup line 218
  37. theorem OAI.DFVSGames.Reduction.Encoding.imageVertices_length_le line 221
  38. abbrev OAI.DFVSGames.Reduction.Encoding.ImageVertex line 226
  39. def OAI.DFVSGames.Reduction.Encoding.imageEquiv line 229
  40. def OAI.DFVSGames.Reduction.Encoding.imageVertex line 233
  41. def OAI.DFVSGames.Reduction.Encoding.imageIndex line 236
  42. theorem OAI.DFVSGames.Reduction.Encoding.imageIndex_eq_iff line 239
  43. theorem OAI.DFVSGames.Reduction.Encoding.imageVertices_range line 245
  44. def OAI.DFVSGames.Explicit.MachineSubdivisionDynamicRows.rows line 262
  45. def OAI.DFVSGames.Explicit.MachineSubdivisionDynamicRows.tokens line 269
  46. theorem OAI.DFVSGames.Explicit.MachineSubdivisionDynamicRows.tokens_length line 275
  47. def OAI.DFVSGames.Explicit.MachineSubdivisionDynamicRows.fields line 278
  48. def OAI.DFVSGames.Explicit.MachineSubdivisionDynamicRows.rowBits line 284
  49. theorem OAI.DFVSGames.Explicit.MachineSubdivisionDynamicRows.templateOutput_rows line 287
  50. def OAI.DFVSGames.Explicit.MachineSubdivisionDynamicRows.field line 295
  51. def OAI.DFVSGames.Explicit.MachineSubdivisionDynamicRows.scratch line 297
  52. def OAI.DFVSGames.Explicit.MachineSubdivisionDynamicRows.output line 298
  53. theorem OAI.DFVSGames.Explicit.MachineSubdivisionDynamicRows.field_ne_scratch line 300
  54. theorem OAI.DFVSGames.Explicit.MachineSubdivisionDynamicRows.field_ne_output line 306
  55. theorem OAI.DFVSGames.Explicit.MachineSubdivisionDynamicRows.scratch_ne_output line 312
  56. def OAI.DFVSGames.Explicit.MachineSubdivisionDynamicRows.machine line 314
  57. theorem OAI.DFVSGames.Explicit.MachineSubdivisionDynamicRows.machine_finiteAlphabet line 325
  58. def OAI.DFVSGames.Explicit.MachineSubdivisionDynamicRows.phaseInTime line 331
  59. theorem OAI.DFVSGames.Explicit.MachineSubdivisionDynamicRows.phase_budget line 346
  60. theorem OAI.DFVSGames.Explicit.MachineSubdivisionDynamicRows.translation_inverse line 355
  61. theorem OAI.DFVSGames.Explicit.MachineSubdivisionDynamicRows.translation_rows line 359
  62. abbrev OAI.DFVSGames.Foundations.Complexity.MachineUnaryCounter.Alphabet line 374
  63. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryCounter.guard line 376
  64. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryCounter.counterTapes line 383
  65. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryCounter.counterTapes_counter line 387
  66. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryCounter.counterTapes_other line 392
  67. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryCounter.guardPushBound line 398
  68. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryCounter.stepAux_succ line 402
  69. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryCounter.stepAux_zero line 410
  70. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryCounter.guardStep_succ line 418
  71. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryCounter.guardStep_zero line 430
  72. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryCounter.guardTrace_succ line 442
  73. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryCounter.guardTrace_zero line 455
  74. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryCounter.guardInTime_succ line 467
  75. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryCounter.guardInTime_zero line 482
  76. inductive OAI.DFVSGames.Explicit.MachineSubdivisionProgram.Tape line 507
  77. instance OAI.DFVSGames.Explicit.MachineSubdivisionProgram.(instance at line 514) line 514
  78. abbrev OAI.DFVSGames.Explicit.MachineSubdivisionProgram.State line 516
  79. def OAI.DFVSGames.Explicit.MachineSubdivisionProgram.initialState line 518
  80. def OAI.DFVSGames.Explicit.MachineSubdivisionProgram.headerField line 520
  81. def OAI.DFVSGames.Explicit.MachineSubdivisionProgram.rowField line 525
  82. def OAI.DFVSGames.Explicit.MachineSubdivisionProgram.rowTokens line 533
  83. def OAI.DFVSGames.Explicit.MachineSubdivisionProgram.headerTokens line 536
  84. def OAI.DFVSGames.Explicit.MachineSubdivisionProgram.newHeaderField line 539
  85. structure OAI.DFVSGames.Explicit.MachineSubdivisionProgram.InitOp line 543
  86. def OAI.DFVSGames.Explicit.MachineSubdivisionProgram.initOp line 549
  87. def OAI.DFVSGames.Explicit.MachineSubdivisionProgram.clearKeys line 560
  88. inductive OAI.DFVSGames.Explicit.MachineSubdivisionProgram.Label line 565
  89. def OAI.DFVSGames.Explicit.MachineSubdivisionProgram.headerNext line 581
  90. def OAI.DFVSGames.Explicit.MachineSubdivisionProgram.initNext line 584
  91. def OAI.DFVSGames.Explicit.MachineSubdivisionProgram.rowEntry line 588
  92. def OAI.DFVSGames.Explicit.MachineSubdivisionProgram.program line 591
  93. def OAI.DFVSGames.Explicit.MachineSubdivisionProgram.machine line 635
  94. theorem OAI.DFVSGames.Explicit.MachineSubdivisionProgram.machine_finiteAlphabet line 646
  95. theorem OAI.DFVSGames.Explicit.MachineSubdivisionProgram.rowField_injective line 652
  96. theorem OAI.DFVSGames.Explicit.MachineSubdivisionProgram.clearKeys_covers line 656
  97. theorem OAI.DFVSGames.Explicit.MachineSubdivisionProgram.accumulator_not_mem_clearKeys line 660
  98. theorem OAI.DFVSGames.Explicit.MachineSubdivisionProgram.output_not_mem_clearKeys line 661
  99. def OAI.DFVSGames.Explicit.MachineSubdivisionHeaders.inputTapes line 673
  100. def OAI.DFVSGames.Explicit.MachineSubdivisionHeaders.afterVertices line 676
  101. def OAI.DFVSGames.Explicit.MachineSubdivisionHeaders.afterAlphabet line 679
  102. def OAI.DFVSGames.Explicit.MachineSubdivisionHeaders.resultTapes line 683
  103. theorem OAI.DFVSGames.Explicit.MachineSubdivisionHeaders.initList_eq line 688
  104. theorem OAI.DFVSGames.Explicit.MachineSubdivisionHeaders.first_result line 694
  105. theorem OAI.DFVSGames.Explicit.MachineSubdivisionHeaders.second_result line 702
  106. theorem OAI.DFVSGames.Explicit.MachineSubdivisionHeaders.third_result line 710
  107. def OAI.DFVSGames.Explicit.MachineSubdivisionHeaders.headersInTime line 718
  108. theorem OAI.DFVSGames.Explicit.MachineSubdivisionHeaders.headers_budget line 756