OAI/Computability/DirectedFeedback/Machines/MachineSingleOrbitCodec.lean

GitHub source file

107 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitHeader.halfStep_first line 56
  2. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitHeader.halfStep_second line 62
  3. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitHeader.halfStep_false line 68
  4. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitHeader.halfTrace line 74
  5. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitHeader.countStep_true line 95
  6. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitHeader.countStep_false line 101
  7. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitHeader.countTrace line 107
  8. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitHeader.initial_configuration line 124
  9. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitHeader.initialStep line 132
  10. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitHeader.headerTrace line 139
  11. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitSubtract.subtractStep_zero line 185
  12. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitSubtract.subtractStep_succ line 193
  13. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitSubtract.subtractTrace line 203
  14. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitSubtract.restore_tapes line 218
  15. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitSubtract.restoreTrace line 224
  16. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitSubtract.removeOffsetTrace line 241
  17. def OAI.DFVSGames.Explicit.MachineSingleOrbitCodec.doubleConstraint line 265
  18. def OAI.DFVSGames.Explicit.MachineSingleOrbitCodec.doubleInstance line 270
  19. def OAI.DFVSGames.Explicit.MachineSingleOrbitCodec.rowBits line 275
  20. def OAI.DFVSGames.Explicit.MachineSingleOrbitCodec.doubledRowBits line 278
  21. def OAI.DFVSGames.Explicit.MachineSingleOrbitCodec.rowsBits line 281
  22. def OAI.DFVSGames.Explicit.MachineSingleOrbitCodec.doubledRowsBits line 284
  23. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitCodec.rowBits_eq line 287
  24. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitCodec.doubledRowBits_eq line 292
  25. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitCodec.rowsBits_nil line 297
  26. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitCodec.doubledRowsBits_nil line 298
  27. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitCodec.rowsBits_cons line 301
  28. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitCodec.doubledRowsBits_cons line 305
  29. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitCodec.gameBits_eq line 310
  30. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitCodec.doubled_gameBits_eq line 315
  31. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitCodec.input_length_eq line 321
  32. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitCodec.vertices_le_input_length line 329
  33. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitCodec.rows_le_input_length line 334
  34. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitRows.joinTrace line 350
  35. def OAI.DFVSGames.Explicit.MachineSingleOrbitRows.rowCost line 354
  36. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitRows.rowTrace line 357
  37. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitRows.guardStep_succ line 393
  38. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitRows.guardStep_zero line 401
  39. def OAI.DFVSGames.Explicit.MachineSingleOrbitRows.rowsCost line 409
  40. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitRows.rowsCost_cons line 412
  41. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitRows.rowsTrace line 418
  42. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitFinish.haltList_eq line 460
  43. def OAI.DFVSGames.Explicit.MachineSingleOrbitFinish.finishStartInTime line 468
  44. def OAI.DFVSGames.Explicit.MachineSingleOrbitFinish.timePolynomial line 476
  45. def OAI.DFVSGames.Explicit.MachineSingleOrbitFinish.completePrefix line 479
  46. def OAI.DFVSGames.Explicit.MachineSingleOrbitRuntime.finalTapes line 524
  47. def OAI.DFVSGames.Explicit.MachineSingleOrbitRuntime.prefixCost line 527
  48. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitRuntime.prefixTrace line 530
  49. def OAI.DFVSGames.Explicit.MachineSingleOrbitRuntime.prefixPolynomial line 558
  50. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitRuntime.prefixCost_le line 561
  51. def OAI.DFVSGames.Explicit.MachineSingleOrbitRuntime.prefixInTime line 570
  52. def OAI.DFVSGames.Explicit.MachineSingleOrbitRuntime.timePolynomial line 579
  53. def OAI.DFVSGames.Explicit.MachineSingleOrbitRuntime.fullRunInTime line 582
  54. def OAI.DFVSGames.Explicit.MachineSingleOrbitRuntime.computableInPolyTime line 589
  55. theorem OAI.DFVSGames.Explicit.MachineSingleOrbitRuntime.workAlphabetFinite line 603
  56. inductive OAI.DFVSGames.Reduction.SourceEquationLookup.Tape line 623
  57. inductive OAI.DFVSGames.Reduction.SourceEquationLookup.Label line 627
  58. def OAI.DFVSGames.Reduction.SourceEquationLookup.fieldDestination line 633
  59. def OAI.DFVSGames.Reduction.SourceEquationLookup.readStart line 634
  60. def OAI.DFVSGames.Reduction.SourceEquationLookup.readLoop line 635
  61. def OAI.DFVSGames.Reduction.SourceEquationLookup.skipLabel line 636
  62. def OAI.DFVSGames.Reduction.SourceEquationLookup.headerLabel line 637
  63. def OAI.DFVSGames.Reduction.SourceEquationLookup.program line 642
  64. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.atSkip line 659
  65. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.atReadStart line 663
  66. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.atReadLoop line 667
  67. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.atReadDone line 672
  68. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.discardHeadersTrace line 675
  69. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.discardFourTrace line 687
  70. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.readFourTrace line 697
  71. def OAI.DFVSGames.Reduction.SourceEquationLookup.scanTapes line 713
  72. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.scanTapes_work line 717
  73. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.scanTapes_index line 721
  74. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.scanTapes_other line 726
  75. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.update_scanTapes_work line 731
  76. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.skipEquationsTrace line 738
  77. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.fieldDestination_eq line 786
  78. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.fieldDestination_injective_below line 792
  79. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.readFour_output_field line 798
  80. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.readFour_output_work line 810
  81. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.readFour_output_frame line 818
  82. def OAI.DFVSGames.Reduction.SourceEquationLookup.outputTapes line 826
  83. def OAI.DFVSGames.Reduction.SourceEquationLookup.scanSteps line 832
  84. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.scanReadTrace line 838
  85. def OAI.DFVSGames.Reduction.SourceEquationLookup.lookupSteps line 866
  86. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.lookupWithSplitTrace line 870
  87. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.output_source line 900
  88. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.output_index line 906
  89. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.output_work line 912
  90. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.output_field line 918
  91. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.output_first line 925
  92. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.output_second line 931
  93. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.output_third line 937
  94. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.output_rhs line 943
  95. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.output_frame line 949
  96. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.equationWords_four line 956
  97. def OAI.DFVSGames.Reduction.SourceEquationLookup.fieldWords line 961
  98. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.output_fieldWords line 964
  99. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.lookupSteps_le_input line 970
  100. def OAI.DFVSGames.Reduction.SourceEquationLookup.timePolynomial line 989
  101. theorem OAI.DFVSGames.Reduction.SourceEquationLookup.timePolynomial_eval line 991
  102. def OAI.DFVSGames.Reduction.SourceEquationLookup.lookupWithSplitInTime line 994
  103. def OAI.DFVSGames.Reduction.SourceEquationLookup.lookupInTime line 1014
  104. def OAI.DFVSGames.Reduction.SourceEquationLookup.machine line 1033
  105. def OAI.DFVSGames.Reduction.SourceEquationLookup.machineInTime line 1044
  106. def OAI.DFVSGames.Reduction.SourceEquationLookup.placedLookupInTime line 1057
  107. def OAI.DFVSGames.Reduction.SourceEquationLookup.embeddedLookupInTime line 1076