OAI/Computability/DirectedFeedback/Machines/MachineAddressHeaders.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Reduction.CloneMachineAffine.output_eq_flatMap line 56
  2. theorem OAI.DFVSGames.Reduction.CloneMachineAffine.output_append line 65
  3. theorem OAI.DFVSGames.Reduction.CloneMachineAffine.affineEmit_replicate_true line 72
  4. theorem OAI.DFVSGames.Reduction.CloneMachineAffine.affineEmit_word line 79
  5. theorem OAI.DFVSGames.Reduction.CloneMachineAffine.affineEmit_word_append line 86
  6. theorem OAI.DFVSGames.Reduction.CloneMachineAffine.affineEmit_words line 91
  7. theorem OAI.DFVSGames.Reduction.CloneMachineAffine.output_word line 99
  8. theorem OAI.DFVSGames.Reduction.CloneMachineAffine.output_word_append line 106
  9. theorem OAI.DFVSGames.Reduction.CloneMachineAffine.output_words line 113
  10. theorem OAI.DFVSGames.Reduction.CloneMachineAffine.output_header_variables line 120
  11. theorem OAI.DFVSGames.Reduction.CloneMachineAffine.output_header_count line 125
  12. theorem OAI.DFVSGames.Reduction.CloneMachineAffine.output_field line 130
  13. theorem OAI.DFVSGames.Reduction.CloneMachineAffine.output_first_field line 136
  14. theorem OAI.DFVSGames.Reduction.CloneMachineAffine.output_second_field line 142
  15. theorem OAI.DFVSGames.Reduction.CloneMachineAffine.output_third_field line 148
  16. theorem OAI.DFVSGames.Reduction.CloneMachineAffine.output_rhs_field line 154
  17. inductive OAI.DFVSGames.Reduction.MachineAddressHeaders.Prefix.Label line 174
  18. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Prefix.readStart line 178
  19. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Prefix.readLoop line 179
  20. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Prefix.destination line 183
  21. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Prefix.statement line 185
  22. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Prefix.atReadStart line 199
  23. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Prefix.atReadLoop line 206
  24. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Prefix.atReadDone line 214
  25. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Prefix.copied line 219
  26. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Prefix.readTapes line 222
  27. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Prefix.resultTapes line 227
  28. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Prefix.clear_readTapes line 231
  29. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Prefix.readTapes_work line 251
  30. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Prefix.resultTapes_other line 256
  31. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Prefix.resultTapes_source line 260
  32. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Prefix.resultTapes_work line 264
  33. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Prefix.resultTapes_n line 267
  34. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Prefix.resultTapes_m line 271
  35. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Prefix.inTime line 275
  36. def OAI.DFVSGames.Reduction.MachineAddressHeaders.baseConstant line 325
  37. def OAI.DFVSGames.Reduction.MachineAddressHeaders.radix line 326
  38. def OAI.DFVSGames.Reduction.MachineAddressHeaders.capacity line 327
  39. def OAI.DFVSGames.Reduction.MachineAddressHeaders.edgeFactor line 328
  40. def OAI.DFVSGames.Reduction.MachineAddressHeaders.edgeCount line 330
  41. inductive OAI.DFVSGames.Reduction.MachineAddressHeaders.Kind line 334
  42. instance OAI.DFVSGames.Reduction.MachineAddressHeaders.(instance at line 337) line 337
  43. def OAI.DFVSGames.Reduction.MachineAddressHeaders.polynomial line 341
  44. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.polynomial_capacity_eval line 345
  45. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.polynomial_edges_eval line 349
  46. inductive OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.Control line 355
  47. instance OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.(instance at line 360) line 360
  48. abbrev OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.Coefficients line 365
  49. abbrev OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.Layout line 369
  50. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.inputControl line 371
  51. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.outputControl line 374
  52. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.controlSlots line 377
  53. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.coefficientBlock line 385
  54. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.localSlots line 392
  55. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.control line 413
  56. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.evalSlots line 415
  57. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.control_eq_iff line 419
  58. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_radix line 422
  59. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_accA line 424
  60. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_accB line 426
  61. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_destination line 428
  62. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_counter line 430
  63. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_scratch line 432
  64. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.evalSlots_digit line 434
  65. inductive OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.Label line 438
  66. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.evalStart line 444
  67. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.afterEval line 447
  68. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.statement line 452
  69. structure OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.WorkClean line 483
  70. structure OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.Clean line 490
  71. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.WorkClean.update_control line 496
  72. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.evalPhaseTrace line 508
  73. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.headerBits line 531
  74. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.resultTapes line 534
  75. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.steps line 541
  76. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.trace_trans_inline_MachineAddressHeaders line 547
  77. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.preparedBase line 551
  78. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.prepareBaseTrace line 555
  79. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.doubleTrace line 627
  80. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.trace line 652
  81. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.inTime line 734
  82. def OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.timePolynomial line 750
  83. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Arithmetic.steps_le_timePolynomial line 757
  84. abbrev OAI.DFVSGames.Reduction.MachineAddressHeaders.Layout line 780
  85. def OAI.DFVSGames.Reduction.MachineAddressHeaders.arithmeticSlots line 784
  86. def OAI.DFVSGames.Reduction.MachineAddressHeaders.prefixLocal line 789
  87. def OAI.DFVSGames.Reduction.MachineAddressHeaders.prefixSlots line 797
  88. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.prefixSlots_apply line 801
  89. abbrev OAI.DFVSGames.Reduction.MachineAddressHeaders.Label line 808
  90. def OAI.DFVSGames.Reduction.MachineAddressHeaders.statement line 810
  91. structure OAI.DFVSGames.Reduction.MachineAddressHeaders.Clean line 817
  92. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.prefixResult_control line 823
  93. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.prefixResult_coefficient line 833
  94. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.Clean.afterPrefix line 840
  95. def OAI.DFVSGames.Reduction.MachineAddressHeaders.resultTapes line 854
  96. def OAI.DFVSGames.Reduction.MachineAddressHeaders.inTime line 859
  97. def OAI.DFVSGames.Reduction.MachineAddressHeaders.timePolynomial line 905
  98. def OAI.DFVSGames.Reduction.MachineAddressHeaders.inPolynomialTime line 908
  99. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.resultTapes_source line 929
  100. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.resultTapes_n line 935
  101. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.resultTapes_m line 942
  102. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.resultTapes_base line 949
  103. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.resultTapes_capacity line 954
  104. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.resultTapes_reversed line 959
  105. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.resultTapes_other line 967
  106. theorem OAI.DFVSGames.Reduction.MachineAddressHeaders.resultTapes_readCopy line 980