OAI/Computability/DirectedFeedback/Machines/MachineTemplateAddress.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.DFVSGames.Reduction.MachineTemplateAddress.Tape line 57
  2. abbrev OAI.DFVSGames.Reduction.MachineTemplateAddress.State line 64
  3. abbrev OAI.DFVSGames.Reduction.MachineTemplateAddress.Alphabet line 65
  4. def OAI.DFVSGames.Reduction.MachineTemplateAddress.hornerLayout line 69
  5. def OAI.DFVSGames.Reduction.MachineTemplateAddress.hornerSlots line 85
  6. def OAI.DFVSGames.Reduction.MachineTemplateAddress.chosen line 88
  7. theorem OAI.DFVSGames.Reduction.MachineTemplateAddress.mem_chosen line 91
  8. abbrev OAI.DFVSGames.Reduction.MachineTemplateAddress.Label line 95
  9. def OAI.DFVSGames.Reduction.MachineTemplateAddress.emitLabel line 99
  10. def OAI.DFVSGames.Reduction.MachineTemplateAddress.reverseLabel line 101
  11. def OAI.DFVSGames.Reduction.MachineTemplateAddress.parseLabel line 102
  12. def OAI.DFVSGames.Reduction.MachineTemplateAddress.hornerLabel line 104
  13. def OAI.DFVSGames.Reduction.MachineTemplateAddress.cleanupLabel line 106
  14. def OAI.DFVSGames.Reduction.MachineTemplateAddress.parseDestination line 109
  15. theorem OAI.DFVSGames.Reduction.MachineTemplateAddress.parseDestination_below line 113
  16. def OAI.DFVSGames.Reduction.MachineTemplateAddress.instruction line 116
  17. def OAI.DFVSGames.Reduction.MachineTemplateAddress.program line 139
  18. structure OAI.DFVSGames.Reduction.MachineTemplateAddress.Clean line 145
  19. def OAI.DFVSGames.Reduction.MachineTemplateAddress.digits line 155
  20. def OAI.DFVSGames.Reduction.MachineTemplateAddress.forwardTapes line 157
  21. def OAI.DFVSGames.Reduction.MachineTemplateAddress.parsedTapes line 160
  22. def OAI.DFVSGames.Reduction.MachineTemplateAddress.resultTapes line 165
  23. def OAI.DFVSGames.Reduction.MachineTemplateAddress.afterHorner line 168
  24. def OAI.DFVSGames.Reduction.MachineTemplateAddress.phaseSteps line 173
  25. theorem OAI.DFVSGames.Reduction.MachineTemplateAddress.resultTapes_output line 180
  26. theorem OAI.DFVSGames.Reduction.MachineTemplateAddress.resultTapes_other line 184
  27. theorem OAI.DFVSGames.Reduction.MachineTemplateAddress.hornerValue_eq_radix line 188
  28. theorem OAI.DFVSGames.Reduction.MachineTemplateAddress.parsedTapes_other line 198
  29. theorem OAI.DFVSGames.Reduction.MachineTemplateAddress.parsedTapes_source line 209
  30. theorem OAI.DFVSGames.Reduction.MachineTemplateAddress.parsedTapes_digit line 218
  31. theorem OAI.DFVSGames.Reduction.MachineTemplateAddress.parsedTapes_clean line 237
  32. theorem OAI.DFVSGames.Reduction.MachineTemplateAddress.cleanup_result line 258
  33. theorem OAI.DFVSGames.Reduction.MachineTemplateAddress.parse_atStart line 298
  34. theorem OAI.DFVSGames.Reduction.MachineTemplateAddress.parse_atLoop line 307
  35. theorem OAI.DFVSGames.Reduction.MachineTemplateAddress.parse_atDone line 317
  36. theorem OAI.DFVSGames.Reduction.MachineTemplateAddress.phaseTrace line 323
  37. theorem OAI.DFVSGames.Reduction.MachineTemplateAddress.programTrace line 416
  38. def OAI.DFVSGames.Reduction.MachineTemplateAddress.phaseInTime line 429
  39. theorem OAI.DFVSGames.Reduction.MachineTemplateAddress.copiedLength_le_inline_MachineTemplateAddress line 448
  40. theorem OAI.DFVSGames.Reduction.MachineTemplateAddress.lengthSum_le_inline_MachineTemplateAddress line 466
  41. def OAI.DFVSGames.Reduction.MachineTemplateAddress.timePolynomial line 478
  42. theorem OAI.DFVSGames.Reduction.MachineTemplateAddress.timePolynomial_eval line 484
  43. theorem OAI.DFVSGames.Reduction.MachineTemplateAddress.phaseSteps_le_timePolynomial line 490
  44. def OAI.DFVSGames.Reduction.MachineTemplateAddress.phaseInPolynomialTime line 523
  45. abbrev OAI.DFVSGames.Reduction.MachineAddressEdge.Tape line 556
  46. abbrev OAI.DFVSGames.Reduction.MachineAddressEdge.State line 557
  47. abbrev OAI.DFVSGames.Reduction.MachineAddressEdge.Alphabet line 558
  48. def OAI.DFVSGames.Reduction.MachineAddressEdge.addressSlots line 562
  49. def OAI.DFVSGames.Reduction.MachineAddressEdge.capacityTape line 566
  50. def OAI.DFVSGames.Reduction.MachineAddressEdge.outputTape line 567
  51. def OAI.DFVSGames.Reduction.MachineAddressEdge.workTape line 568
  52. def OAI.DFVSGames.Reduction.MachineAddressEdge.tempTape line 569
  53. def OAI.DFVSGames.Reduction.MachineAddressEdge.scratchTape line 570
  54. theorem OAI.DFVSGames.Reduction.MachineAddressEdge.address_ne_output line 573
  55. theorem OAI.DFVSGames.Reduction.MachineAddressEdge.capacity_ne_output line 577
  56. theorem OAI.DFVSGames.Reduction.MachineAddressEdge.work_ne_output line 581
  57. theorem OAI.DFVSGames.Reduction.MachineAddressEdge.temp_ne_work line 585
  58. abbrev OAI.DFVSGames.Reduction.MachineAddressEdge.Label line 588
  59. def OAI.DFVSGames.Reduction.MachineAddressEdge.leftLabel line 591
  60. def OAI.DFVSGames.Reduction.MachineAddressEdge.rightLabel line 593
  61. def OAI.DFVSGames.Reduction.MachineAddressEdge.plumbing line 595
  62. def OAI.DFVSGames.Reduction.MachineAddressEdge.instruction line 598
  63. def OAI.DFVSGames.Reduction.MachineAddressEdge.program line 624
  64. structure OAI.DFVSGames.Reduction.MachineAddressEdge.Clean line 629
  65. def OAI.DFVSGames.Reduction.MachineAddressEdge.appended line 633
  66. theorem OAI.DFVSGames.Reduction.MachineAddressEdge.appended_address line 636
  67. theorem OAI.DFVSGames.Reduction.MachineAddressEdge.appended_capacity line 642
  68. theorem OAI.DFVSGames.Reduction.MachineAddressEdge.appended_output line 646
  69. theorem OAI.DFVSGames.Reduction.MachineAddressEdge.appended_other line 651
  70. theorem OAI.DFVSGames.Reduction.MachineAddressEdge.appended_append line 656
  71. theorem OAI.DFVSGames.Reduction.MachineAddressEdge.Clean.appended line 661
  72. def OAI.DFVSGames.Reduction.MachineAddressEdge.edgeBits line 675
  73. def OAI.DFVSGames.Reduction.MachineAddressEdge.phaseSteps line 680
  74. theorem OAI.DFVSGames.Reduction.MachineAddressEdge.addressResult_eq line 688
  75. theorem OAI.DFVSGames.Reduction.MachineAddressEdge.transfer_result line 692
  76. theorem OAI.DFVSGames.Reduction.MachineAddressEdge.literalStep line 723
  77. theorem OAI.DFVSGames.Reduction.MachineAddressEdge.phaseTrace line 732
  78. theorem OAI.DFVSGames.Reduction.MachineAddressEdge.programTrace line 865
  79. def OAI.DFVSGames.Reduction.MachineAddressEdge.phaseInTime line 888
  80. def OAI.DFVSGames.Reduction.MachineAddressEdge.timePolynomial line 917
  81. theorem OAI.DFVSGames.Reduction.MachineAddressEdge.timePolynomial_eval line 923
  82. theorem OAI.DFVSGames.Reduction.MachineAddressEdge.radix_le_magnitude line 931
  83. theorem OAI.DFVSGames.Reduction.MachineAddressEdge.phaseSteps_le_timePolynomial line 940