OAI/Computability/DirectedFeedback/Machines/MachineExpanderRowDivision.lean

GitHub source file

133 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.controlStatement_inverse_inline_MachineExpanderRowDivision line 56
  2. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.transportedDivision_inline_MachineExpanderRowDivision line 63
  3. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.divisionStates_apply line 122
  4. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.divisionState line 126
  5. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.divisionOutput line 131
  6. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.firstDivisionTrace line 137
  7. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.secondDivisionTrace line 178
  8. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.divisionOutput_source line 222
  9. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.divisionOutput_quotient line 234
  10. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.divisionOutput_remainder line 243
  11. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.divisionOutput_other line 250
  12. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.firstDivisionInTime line 260
  13. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderRow.secondDivisionInTime line 284
  14. inductive OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.ExtraTape line 320
  15. instance OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.(instance at line 324) line 324
  16. abbrev OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.Tape line 326
  17. abbrev OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.Alphabet line 328
  18. instance OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.alphabetFintype line 332
  19. inductive OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.OuterLabel line 335
  20. instance OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.(instance at line 339) line 339
  21. abbrev OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.Label line 341
  22. abbrev OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.Position line 342
  23. abbrev OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.State line 343
  24. abbrev OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.RowStatePrefix line 344
  25. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.guardStates line 347
  26. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.guardStates_apply line 354
  27. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.guardStates_symm_apply line 358
  28. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.rowFactor_pos line 361
  29. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.zeroPosition line 365
  30. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.nextPosition line 368
  31. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.positionPair line 371
  32. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.caller line 374
  33. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.boundaryState line 376
  34. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.initialState line 381
  35. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.prepareState line 385
  36. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.resetState line 389
  37. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.clearRegister line 393
  38. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.advancePositionState line 396
  39. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.resetPositionState line 399
  40. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.vertexGuardCore line 402
  41. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.outerStatement line 412
  42. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.rowReturn line 432
  43. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.program line 434
  44. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.program_row line 439
  45. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.program_outer line 445
  46. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.rowExecution line 449
  47. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.rowExecution_steps line 461
  48. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.rowTapes line 469
  49. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.extraTapes line 475
  50. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes line 479
  51. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.initialTapes line 483
  52. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderTable.finalTapes line 489
  53. def OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.tapes line 504
  54. def OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.statement line 506
  55. def OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.configuration line 508
  56. def OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.program line 510
  57. abbrev OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.castStatement line 513
  58. abbrev OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.castConfiguration line 514
  59. abbrev OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.castProgram line 515
  60. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.tapes_rfl line 517
  61. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.statement_rfl line 518
  62. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.configuration_rfl line 519
  63. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.program_rfl line 520
  64. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.program_apply line 522
  65. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.statement_roundtrip line 525
  66. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.statement_symm_roundtrip line 528
  67. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.configuration_roundtrip line 531
  68. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.configuration_symm_roundtrip line 534
  69. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.program_roundtrip line 537
  70. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.program_symm_roundtrip line 540
  71. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.tapes_roundtrip line 543
  72. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.tapes_symm_roundtrip line 546
  73. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.configuration_label line 549
  74. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.configuration_state line 552
  75. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.configuration_tapes line 555
  76. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.configuration_mk line 558
  77. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.map_configuration_rfl line 562
  78. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.stepAux_simulation line 567
  79. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.step_simulation line 572
  80. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.trace_transport line 578
  81. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.successfulTrace line 586
  82. def OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.executionInTime line 594
  83. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.executionInTime_steps line 606
  84. def OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.successfulExecutionInTime line 611
  85. theorem OAI.DFVSGames.Foundations.Complexity.MachineAlphabetTransport.successfulExecutionInTime_steps line 617
  86. inductive OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.ExtraTape line 633
  87. instance OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.(instance at line 637) line 637
  88. abbrev OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.Tape line 639
  89. abbrev OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.Alphabet line 640
  90. abbrev OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.BoolAlphabet line 642
  91. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.alphabet_eq line 644
  92. instance OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.alphabetFintype line 650
  93. inductive OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.AffinePhase line 654
  94. instance OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.(instance at line 658) line 658
  95. inductive OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.AffineLabel line 660
  96. instance OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.(instance at line 664) line 664
  97. inductive OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.OuterLabel line 666
  98. abbrev OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.Label line 674
  99. abbrev OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.State line 675
  100. abbrev OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.RegisterAmbient line 676
  101. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.registerStates line 679
  102. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.registerStates_apply line 686
  103. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.registerStates_symm_apply line 690
  104. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.caller line 693
  105. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.initialState line 696
  106. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.normalizeState line 700
  107. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.initialEncoding line 704
  108. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.initialEncoding_eq_family line 706
  109. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.tableTape line 709
  110. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.inputVertexTape line 710
  111. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.vertexCountTape line 711
  112. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.resultTape line 712
  113. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.affineSource line 714
  114. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.affineDestination line 718
  115. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.affineCoefficient line 722
  116. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.affineExit line 726
  117. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.affineStatement line 730
  118. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.drainStatement line 748
  119. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.boolOuterStatement line 756
  120. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.outerStatement line 785
  121. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.tableReturn line 789
  122. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.program line 791
  123. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.program_table line 796
  124. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.program_outer line 803
  125. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.boolView line 807
  126. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.boolView_outer line 811
  127. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.tableExecution line 820
  128. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.tableExecution_steps line 832
  129. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.tableFrame line 841
  130. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.extraFrame line 847
  131. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.boundaryTapes line 852
  132. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.initialTapes line 856
  133. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.familyTapes line 863